-
Notifications
You must be signed in to change notification settings - Fork 403
/
Compare.lean
126 lines (98 loc) · 4.04 KB
/
Compare.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
/-
Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
namespace Lake
/--
Proof that the equality of a compare function corresponds
to propositional equality.
-/
class EqOfCmp (α : Type u) (cmp : α → α → Ordering) where
eq_of_cmp {a a' : α} : cmp a a' = .eq → a = a'
export EqOfCmp (eq_of_cmp)
/--
Proof that the equality of a compare function corresponds
to propositional equality and vice versa.
-/
class LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends EqOfCmp α cmp where
cmp_rfl {a : α} : cmp a a = .eq
export LawfulCmpEq (cmp_rfl)
attribute [simp] cmp_rfl
@[simp] theorem cmp_iff_eq [LawfulCmpEq α cmp] : cmp a a' = .eq ↔ a = a' :=
Iff.intro eq_of_cmp fun a_eq => a_eq ▸ cmp_rfl
/--
Proof that the equality of a compare function corresponds
to propositional equality with respect to a given function.
-/
class EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) where
eq_of_cmp_wrt {a a' : α} : cmp a a' = .eq → f a = f a'
export EqOfCmpWrt (eq_of_cmp_wrt)
instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩
instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
eq_of_cmp_wrt h := by rw [eq_of_cmp h]
instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
-- ## Basic Instances
theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
[Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by
unfold compareOfLessAndEq at h
split at h; case inl => exact False.elim h
split at h; case inr => exact False.elim h
assumption
theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α}
[Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by
simp [compareOfLessAndEq, lt_irrefl]
instance : LawfulCmpEq Nat compare where
eq_of_cmp := eq_of_compareOfLessAndEq
cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
theorem Fin.eq_of_compare {n n' : Fin m} (h : compare n n' = .eq) : n = n' := by
dsimp only [compare] at h
have h' := eq_of_compareOfLessAndEq h
exact Fin.eq_of_val_eq h'
instance : LawfulCmpEq (Fin n) compare where
eq_of_cmp := Fin.eq_of_compare
cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
instance : LawfulCmpEq UInt64 compare where
eq_of_cmp h := eq_of_compareOfLessAndEq h
cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
theorem List.lt_irrefl [LT α] (irrefl_α : ∀ a : α, ¬ a < a)
: (a : List α) → ¬ a < a
| _, .head _ _ h => irrefl_α _ h
| _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3
@[simp] theorem String.lt_irrefl (s : String) : ¬ s < s :=
List.lt_irrefl (fun c => Nat.lt_irrefl c.1.1) _
instance : LawfulCmpEq String compare where
eq_of_cmp := eq_of_compareOfLessAndEq
cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _
@[macro_inline]
def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering
| none, none => .eq
| none, some _ => .lt
| some _, none => .gt
| some x, some y => cmp x y
instance [EqOfCmp α cmp] : EqOfCmp (Option α) (Option.compareWith cmp) where
eq_of_cmp := by
intro o o'
unfold Option.compareWith
cases o <;> cases o' <;> simp
exact eq_of_cmp
instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp) where
cmp_rfl := by
intro o
unfold Option.compareWith
cases o <;> simp
def Prod.compareWith
(cmpA : α → α → Ordering) (cmpB : β → β → Ordering)
: (α × β) → (α × β) → Ordering :=
fun (a, b) (a', b') => match cmpA a a' with | .eq => cmpB b b' | ord => ord
instance [EqOfCmp α cmpA] [EqOfCmp β cmpB]
: EqOfCmp (α × β) (Prod.compareWith cmpA cmpB) where
eq_of_cmp := by
intro (a, b) (a', b')
dsimp only [Prod.compareWith]
split; next ha => intro hb; rw [eq_of_cmp ha, eq_of_cmp hb]
intros; contradiction
instance [LawfulCmpEq α cmpA] [LawfulCmpEq β cmpB]
: LawfulCmpEq (α × β) (Prod.compareWith cmpA cmpB) where
cmp_rfl := by simp [Prod.compareWith]