switch to Lean's DecidableLT

cedar-lean/Cedar/Data/LT.lean

@@ -62,15 +62,13 @@ theorem StrictLT.not_eq [LT α] [StrictLT α] (x y : α) :
   have h₃ := StrictLT.irreflexive x
   contradiction
 
-abbrev DecidableLT (α) [LT α] := DecidableRel (α := α) (· < ·)
-
 end Cedar.Data
 
 ----- Theorems and instances -----
 
 open Cedar.Data
 
-theorem List.lt_cons_cases [LT α] [Cedar.Data.DecidableLT α] {x y : α} {xs ys : List α} :
+theorem List.lt_cons_cases [LT α] [DecidableLT α] {x y : α} {xs ys : List α} :
   x :: xs < y :: ys →
   (x < y ∨ (¬ x < y ∧ ¬ y < x ∧ xs < ys))
 := by
@@ -84,7 +82,7 @@ theorem List.cons_lt_cons [LT α] [StrictLT α] (x : α) (xs ys : List α) :
   apply List.Lex.cons
   simp only [lex_lt, h₁]
 
-theorem List.slt_irrefl [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List α) :
+theorem List.slt_irrefl [LT α] [StrictLT α] [DecidableLT α] (xs : List α) :
   ¬ xs < xs
 := by
   induction xs
@@ -114,7 +112,7 @@ theorem List.slt_trans [LT α] [StrictLT α] {xs ys zs : List α} :
       apply List.Lex.cons
       exact List.slt_trans h₃ h₆
 
-theorem List.slt_asymm [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] {xs ys : List α} :
+theorem List.slt_asymm [LT α] [StrictLT α] [DecidableLT α] {xs ys : List α} :
   xs < ys → ¬ ys < xs
 := by
   intro h₁
@@ -170,7 +168,7 @@ theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} :
         apply List.Lex.rel
         exact StrictLT.if_not_lt_eq_then_gt xhd yhd h₄ h₅
 
-instance List.strictLT (α) [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] : StrictLT (List α) where
+instance List.strictLT (α) [LT α] [StrictLT α] [DecidableLT α] : StrictLT (List α) where
   asymmetric _ _   := List.slt_asymm
   transitive _ _ _ := List.slt_trans
   connected  _ _   := List.lt_conn

cedar-lean/Cedar/Data/List.lean

@@ -29,7 +29,7 @@ open Cedar.Data
 
 ----- Definitions -----
 
-def insertCanonical [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α :=
+def insertCanonical [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α :=
   match xs with
   | [] => [x]
   | hd :: tl =>
@@ -46,7 +46,7 @@ If the ordering relation < on β is strict, then `canonicalize` returns a
 canonical representation of the input list, which is sorted and free of
 duplicates.
 -/
-def canonicalize [LT β] [Cedar.Data.DecidableLT β] (f : α → β) : List α → List α
+def canonicalize [LT β] [DecidableLT β] (f : α → β) : List α → List α
   | [] => []
   | hd :: tl => insertCanonical f hd (canonicalize f tl)
 

cedar-lean/Cedar/Data/Map.lean

@@ -104,7 +104,7 @@ def mapMOnKeys {α β γ} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) (
 instance [LT (Prod α β)] : LT (Map α β) where
   lt a b := a.kvs < b.kvs
 
-instance decLt [LT (Prod α β)] [DecidableEq (Prod α β)] [Cedar.Data.DecidableLT (Prod α β)] : (n m : Map α β) → Decidable (n < m)
+instance decLt [LT (Prod α β)] [DecidableEq (Prod α β)] [DecidableLT (Prod α β)] : (n m : Map α β) → Decidable (n < m)
   | .mk nkvs, .mk mkvs => List.decidableLT nkvs mkvs
 
 -- enables ∈ notation for map keys

cedar-lean/Cedar/Data/Set.lean

@@ -124,7 +124,7 @@ def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α :=
 instance [LT α] : LT (Set α) where
   lt a b := a.elts < b.elts
 
-instance decLt [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] : (n m : Set α) → Decidable (n < m)
+instance decLt [LT α] [DecidableEq α] [DecidableLT α] : (n m : Set α) → Decidable (n < m)
   | .mk nelts, .mk melts => List.decidableLT nelts melts
 
 -- enables ∅

cedar-lean/Cedar/Thm/Authorization/Authorizer.lean

@@ -306,7 +306,7 @@ theorem Except.isOk_iff_exists {x : Except ε α} :
 := by
   cases x <;> simp [Except.isOk, Except.toBool]
 
-theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [Cedar.Data.DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} :
+theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} :
   Except.isOk (as.mapM f) →
   Except.isOk ((Set.elts (Set.make as)).mapM f)
 := by

cedar-lean/Cedar/Thm/Data/List/Basic.lean

@@ -294,7 +294,7 @@ theorem sortedBy_cons [LT β] [StrictLT β] {f : α → β} {x : α} {ys : List
     apply h₂
     simp only [mem_cons, true_or]
 
-theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β]
+theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β]
   {f : α → β} {x y : α} {xs : List α} :
   xs.SortedBy f → x ∈ xs → y ∈ xs → f x = f y →
   x = y
@@ -317,7 +317,7 @@ theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [Cedar.Data.Decidab
       simp only [hf, StrictLT.irreflexive] at hlt
     · exact ih hx hy
 
-theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β]
+theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β]
   {f : α → β} {x : α} {xs : List α} :
   x ∈ xs → xs.SortedBy f →
   xs.find? (fun y => f y == f x) = x
@@ -384,7 +384,7 @@ theorem map_eq_implies_sortedBy [LT β] [StrictLT β] {f : α → β} {g : γ 
           apply sortedBy_implies_head_lt_tail h₂
           simp only [mem_cons, true_or]
 
-theorem filter_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} :
+theorem filter_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} :
   SortedBy f xs → SortedBy f (xs.filter p)
 := by
   intro h₁
@@ -401,7 +401,7 @@ theorem filter_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : 
       exact h₂.left
     · exact ih
 
-theorem filterMap_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} :
+theorem filterMap_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} :
   (∀ x y, g x = some y → f x = f' y) →
   SortedBy f xs →
   SortedBy f' (xs.filterMap g)

cedar-lean/Cedar/Thm/Data/List/Canonical.lean

@@ -30,11 +30,11 @@ open Cedar.Data
 
 /-! ### insertCanonical -/
 
-theorem insertCanonical_singleton [LT β] [Cedar.Data.DecidableLT β] (f : α → β)  (x : α) :
+theorem insertCanonical_singleton [LT β] [DecidableLT β] (f : α → β)  (x : α) :
   insertCanonical f x [] = [x]
 := by unfold insertCanonical; rfl
 
-theorem insertCanonical_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) :
+theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) :
   insertCanonical f x xs ≠ []
 := by
   unfold insertCanonical
@@ -46,7 +46,7 @@ theorem insertCanonical_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT
     split at h <;> try trivial
     split at h <;> trivial
 
-theorem insertCanonical_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {xs : List α} (x : α) :
+theorem insertCanonical_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} (x : α) :
   SortedBy f xs →
   SortedBy f (insertCanonical f x xs)
 := by
@@ -85,7 +85,7 @@ theorem insertCanonical_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT 
         case cons_nil => exact SortedBy.cons_nil
         case cons_cons h₅ h₆ => exact SortedBy.cons_cons (by simp only [h₄, h₆]) h₅
 
-theorem insertCanonical_cases [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x y : α) (ys : List α) :
+theorem insertCanonical_cases [LT β] [DecidableLT β] (f : α → β) (x y : α) (ys : List α) :
   (f x < f y ∧ insertCanonical f x (y :: ys) = x :: y :: ys) ∨
   (¬ f x < f y ∧ f x > f y ∧ insertCanonical f x (y :: ys) = y :: insertCanonical f x ys) ∨
   (¬ f x < f y ∧ ¬ f x > f y ∧ insertCanonical f x (y :: ys) = x :: ys)
@@ -102,7 +102,7 @@ theorem insertCanonical_cases [LT β] [Cedar.Data.DecidableLT β] (f : α → β
     case pos _ _ h₃ => simp [h₃, h₁]
     case neg _ _ h₃ => simp [h₃]
 
-theorem insertCanonical_subset [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) :
+theorem insertCanonical_subset [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) :
   insertCanonical f x xs ⊆ x :: xs
 := by
   induction xs
@@ -117,7 +117,7 @@ theorem insertCanonical_subset [LT β] [Cedar.Data.DecidableLT β] (f : α → 
     · simp only [h₁, cons_subset, mem_cons, true_or, true_and]
       exact Subset.trans (List.subset_cons_self hd tl) (List.subset_cons_self x (hd :: tl))
 
-theorem insertCanonical_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (x : α) (xs : List α) :
+theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (xs : List α) :
   x :: xs ≡ insertCanonical id x xs
 := by
   unfold insertCanonical
@@ -173,7 +173,7 @@ theorem insertCanonical_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α]
               apply cons_equiv_cons
               exact ih
 
-theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] {p : β → γ → Prop}
+theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] {p : β → γ → Prop}
   {kv₁ : α × β} {kv₂ : α × γ} {kvs₁ : List (α × β)} {kvs₂ : List (α × γ)}
   (h₁ : kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd)
   (h₂ : Forallᵥ p kvs₁ kvs₂) :
@@ -202,7 +202,7 @@ theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Ce
       · contradiction
       · exact Forall₂.cons (by exact h₁) (by exact h₄)
 
-theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) :
+theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) :
   insertCanonical Prod.fst (Prod.map id f x) (map (Prod.map id f) xs) =
   map (Prod.map id f) (insertCanonical Prod.fst x xs)
 := by
@@ -218,7 +218,7 @@ theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [Cedar.Data.Dec
         simp [ih, Prod.map]
       · simp [Prod.map]
 
-theorem insertCanonical_map_fst_canonicalize {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) :
+theorem insertCanonical_map_fst_canonicalize {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) :
   insertCanonical Prod.fst (Prod.map id f x) (canonicalize Prod.fst (map (Prod.map id f) xs)) =
   map (Prod.map id f) (insertCanonical Prod.fst x (canonicalize Prod.fst xs))
 := by
@@ -230,11 +230,11 @@ theorem insertCanonical_map_fst_canonicalize {α β γ} [LT α] [StrictLT α] [C
 
 /-! ## canonicalize -/
 
-theorem canonicalize_nil [LT β] [Cedar.Data.DecidableLT β] (f : α → β) :
+theorem canonicalize_nil [LT β] [DecidableLT β] (f : α → β) :
   canonicalize f [] = []
 := by unfold canonicalize; rfl
 
-theorem canonicalize_nil' [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) :
+theorem canonicalize_nil' [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) :
   xs = [] ↔ (canonicalize f xs) = []
 := by
   constructor
@@ -251,7 +251,7 @@ theorem canonicalize_nil' [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (
       apply insertCanonical_not_nil f x (canonicalize f xs)
       exact h₁
 
-theorem canonicalize_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) :
+theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) :
   xs ≠ [] ↔ (canonicalize f xs) ≠ []
 := by
   constructor
@@ -267,14 +267,14 @@ theorem canonicalize_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β
     intro h₀
     cases xs <;> simp only [ne_eq, reduceCtorEq, not_false_eq_true, not_true_eq_false] at *
 
-theorem canonicalize_cons [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) (a : α) :
+theorem canonicalize_cons [LT β] [DecidableLT β] (f : α → β) (xs : List α) (a : α) :
   canonicalize f xs = canonicalize f ys → canonicalize f (a :: xs) = canonicalize f (a :: ys)
 := by
   intro h₁
   unfold canonicalize
   simp [h₁]
 
-theorem canonicalize_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) :
+theorem canonicalize_sortedBy [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) :
   SortedBy f (canonicalize f xs)
 := by
   induction xs
@@ -284,7 +284,7 @@ theorem canonicalize_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β]
     apply insertCanonical_sortedBy
     exact ih
 
-theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {xs : List α} :
+theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} :
   SortedBy f xs → (canonicalize f xs) = xs
 := by
   intro h₁
@@ -296,7 +296,7 @@ theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [Cedar.Data.Decid
       specialize ih h₁
       simp [ih, insertCanonical, h₂]
 
-theorem canonicalize_subseteq [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) :
+theorem canonicalize_subseteq [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) :
   xs.canonicalize f ⊆ xs
 := by
   induction xs <;> simp only [canonicalize, Subset.refl]
@@ -308,7 +308,7 @@ theorem canonicalize_subseteq [LT β] [StrictLT β] [Cedar.Data.DecidableLT β]
     simp only [subset_cons_self]
 
 /-- Corollary of `canonicalize_subseteq` -/
-theorem in_canonicalize_in_list [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {x : α} {xs : List α} :
+theorem in_canonicalize_in_list [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {x : α} {xs : List α} :
   x ∈ xs.canonicalize f → x ∈ xs
 := by
   intro h₁
@@ -321,7 +321,7 @@ Note that `canonicalize_equiv` does not hold for all functions `f`.
 To see why, consider xs = [(1, false), (1, true)], f = Prod.fst.
 Then `canonicalize f xs = [(1, false)] !≡ xs`.
 -/
-theorem canonicalize_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List α) :
+theorem canonicalize_equiv [LT α] [StrictLT α] [DecidableLT α] (xs : List α) :
   xs ≡ canonicalize id xs
 := by
   induction xs
@@ -339,7 +339,7 @@ theorem canonicalize_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs
 Note that `equiv_implies_canonical_eq` does not hold for all functions `f`.
 To see why, consider the `example` immediately below this.
 -/
-theorem equiv_implies_canonical_eq [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs ys : List α) :
+theorem equiv_implies_canonical_eq [LT α] [StrictLT α] [DecidableLT α] (xs ys : List α) :
   xs ≡ ys → (canonicalize id xs) = (canonicalize id ys)
 := by
   intro h₁
@@ -371,7 +371,7 @@ example :
   simp [List.Equiv]
   decide
 
-theorem canonicalize_idempotent {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) :
+theorem canonicalize_idempotent {α β} [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) :
   canonicalize f (canonicalize f xs) = canonicalize f xs
 := sortedBy_implies_canonicalize_eq (canonicalize_sortedBy f xs)
 
@@ -384,7 +384,7 @@ Then `(canonicalize f xs).filter p = []` but `(xs.filter p).canonicalize f = [(1
 #eval (canonicalize Prod.fst [(1, false), (1, true)]).filter Prod.snd
 #eval ([(1, false), (1, true)].filter Prod.snd).canonicalize Prod.fst
 -/
-theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (p : α → Bool) (xs : List α) :
+theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [DecidableLT α] (p : α → Bool) (xs : List α) :
   (canonicalize id xs).filter p = (xs.filter p).canonicalize id
 := by
   have h₁ : (canonicalize id xs).filter p ≡ xs.filter p := by
@@ -397,7 +397,7 @@ theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [Cedar.Data.DecidableL
     (canonicalize_sortedBy id (filter p xs))
     (Equiv.trans h₁ h₂)
 
-theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) :
+theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) :
   List.Forallᵥ p kvs₁ kvs₂ →
   List.Forallᵥ p (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂)
 := by
@@ -410,7 +410,7 @@ theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Cedar
     have h₄ := canonicalize_preserves_forallᵥ p tl₁ tl₂ h₃
     apply insertCanonical_preserves_forallᵥ h₂ h₄
 
-theorem canonicalize_of_map_fst {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) :
+theorem canonicalize_of_map_fst {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) :
   List.canonicalize Prod.fst (List.map (Prod.map id f) xs) =
   List.map (Prod.map id f) (List.canonicalize Prod.fst xs)
 := by

cedar-lean/DiffTest/Parser.lean

@@ -419,11 +419,11 @@ formalization standardizes on ancestor information.
 The definitions and utility functions below are used to convert the descendant
 representation to the ancestor representation.
 -/
-def findInMapValues [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] (m : Map α (Set α)) (k₁ : α) : Set α :=
+def findInMapValues [LT α] [DecidableEq α] [DecidableLT α] (m : Map α (Set α)) (k₁ : α) : Set α :=
   let setOfSets := List.map (λ (k₂,v) => if v.contains k₁ then Set.singleton k₂ else Set.empty) m.toList
   setOfSets.foldl (λ acc v => acc.union v) Set.empty
 
-def descendantsToAncestors [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] (descendants : Map α (Set α)) : Map α (Set α) :=
+def descendantsToAncestors [LT α] [DecidableEq α] [DecidableLT α] (descendants : Map α (Set α)) : Map α (Set α) :=
   Map.make (List.map
     (λ (k,_) => (k, findInMapValues descendants k)) descendants.toList)