@@ -7,89 +7,104 @@ Authors: Mac Malone
77namespace Lake
88
99/--
10- Proof that that equality of a compare function corresponds
10+ Proof that the equality of a compare function corresponds
1111to propositional equality.
1212-/
1313class EqOfCmp (α : Type u) (cmp : α → α → Ordering) where
14- eq_of_cmp {a a' : α} : cmp a a' = Ordering .eq → a = a'
14+ eq_of_cmp {a a' : α} : cmp a a' = .eq → a = a'
1515
1616export EqOfCmp (eq_of_cmp)
1717
1818/--
19- Proof that that equality of a compare function corresponds
19+ Proof that the equality of a compare function corresponds
20+ to propositional equality and vice versa.
21+ -/
22+ class LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends EqOfCmp α cmp where
23+ cmp_rfl {a : α} : cmp a a = .eq
24+
25+ export LawfulCmpEq (cmp_rfl)
26+
27+ attribute [simp] cmp_rfl
28+
29+ @[simp] theorem cmp_iff_eq [LawfulCmpEq α cmp] : cmp a a' = .eq ↔ a = a' :=
30+ Iff.intro eq_of_cmp fun a_eq => a_eq ▸ cmp_rfl
31+
32+ /--
33+ Proof that the equality of a compare function corresponds
2034to propositional equality with respect to a given function.
2135-/
2236class EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) where
23- eq_of_cmp_wrt {a a' : α} : cmp a a' = Ordering .eq → f a = f a'
37+ eq_of_cmp_wrt {a a' : α} : cmp a a' = .eq → f a = f a'
2438
2539export EqOfCmpWrt (eq_of_cmp_wrt)
2640
41+ instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩
42+
2743instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
2844 eq_of_cmp_wrt h := by rw [eq_of_cmp h]
2945
30- instance [EqOfCmpWrt α id cmp] : EqOfCmp α cmp where
31- eq_of_cmp h := eq_of_cmp_wrt (f := id) h
32-
3346instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
3447 eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
3548
36- instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩
3749
38- theorem eq_of_compareOfLessAndEq
39- {a a' : α} [LT α] [DecidableEq α] [Decidable (a < a')]
40- (h : compareOfLessAndEq a a' = Ordering.eq) : a = a' := by
50+ -- ## Basic Instances
51+
52+ theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
53+ [Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by
4154 unfold compareOfLessAndEq at h
4255 split at h; case inl => exact False.elim h
4356 split at h; case inr => exact False.elim h
4457 assumption
4558
46- theorem Nat.eq_of_compare
47- {n n' : Nat} : compare n n' = Ordering.eq → n = n' := by
48- simp only [compare]; exact eq_of_compareOfLessAndEq
59+ theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α}
60+ [Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by
61+ simp [compareOfLessAndEq, lt_irrefl]
4962
50- @[simp]
51- theorem Nat.compare_iff_eq
52- {n n' : Nat} : compare n n' = Ordering.eq ↔ n = n' := by
53- refine ⟨eq_of_compare, fun h => ?_⟩
54- simp [h, compare, compareOfLessAndEq]
63+ instance : LawfulCmpEq Nat compare where
64+ eq_of_cmp := eq_of_compareOfLessAndEq
65+ cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
5566
56- instance : EqOfCmp Nat compare where
57- eq_of_cmp h := Nat.eq_of_compare h
67+ theorem Fin.eq_of_compare {n n' : Fin m} (h : compare n n' = .eq) : n = n' := by
68+ dsimp only [compare] at h
69+ have h' := eq_of_compareOfLessAndEq h
70+ exact Fin.eq_of_val_eq h'
5871
59- theorem String.eq_of_compare
60- {s s' : String} : compare s s' = Ordering.eq → s = s' := by
61- simp only [compare]; exact eq_of_compareOfLessAndEq
72+ instance : LawfulCmpEq (Fin n) compare where
73+ eq_of_cmp := Fin.eq_of_compare
74+ cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
75+
76+ instance : LawfulCmpEq UInt64 compare where
77+ eq_of_cmp h := eq_of_compareOfLessAndEq h
78+ cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
6279
6380theorem List.lt_irrefl [LT α] (irrefl_α : ∀ a : α, ¬ a < a)
6481: (a : List α) → ¬ a < a
65- | _, .head _ _ h => irrefl_α _ h
66- | _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3
82+ | _, .head _ _ h => irrefl_α _ h
83+ | _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3
6784
68- @[simp]
69- theorem String.lt_irrefl (s : String) : ¬ s < s :=
85+ @[simp] theorem String.lt_irrefl (s : String) : ¬ s < s :=
7086 List.lt_irrefl (fun c => Nat.lt_irrefl c.1 .1 ) _
7187
72- @[simp]
73- theorem String.compare_iff_eq
74- {n n' : String} : compare n n' = Ordering.eq ↔ n = n' := by
75- refine ⟨eq_of_compare, fun h => ?_⟩
76- simp [h, compare, compareOfLessAndEq]
77-
78- instance : EqOfCmp String compare where
79- eq_of_cmp h := String.eq_of_compare h
88+ instance : LawfulCmpEq String compare where
89+ eq_of_cmp := eq_of_compareOfLessAndEq
90+ cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _
8091
81- @[inline ]
92+ @[macroInline ]
8293def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering
83- | none, none => Ordering .eq
84- | none, some _ => Ordering .lt
85- | some _, none => Ordering .gt
94+ | none, none => .eq
95+ | none, some _ => .lt
96+ | some _, none => .gt
8697| some x, some y => cmp x y
8798
88- theorem Option.eq_of_compareWith [EqOfCmp α cmp]
89- {o o' : Option α} : compareWith cmp o o' = Ordering.eq → o = o' := by
90- unfold compareWith
91- cases o <;> cases o' <;> simp
92- exact eq_of_cmp
93-
9499instance [EqOfCmp α cmp] : EqOfCmp (Option α) (Option.compareWith cmp) where
95- eq_of_cmp h := Option.eq_of_compareWith h
100+ eq_of_cmp := by
101+ intro o o'
102+ unfold Option.compareWith
103+ cases o <;> cases o' <;> simp
104+ exact eq_of_cmp
105+
106+ instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp) where
107+ cmp_rfl := by
108+ intro o
109+ unfold Option.compareWith
110+ cases o <;> simp
0 commit comments