Skip to content

Commit 188ae17

Browse files
wkrozowskiwkrozowski
committed
Get the prototype working
1 parent 4681ef7 commit 188ae17

File tree

1 file changed

+157
-72
lines changed

1 file changed

+157
-72
lines changed

‎src/Std/Data/Internal/List/Associative.lean‎

Lines changed: 157 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -8250,89 +8250,174 @@ theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l
82508250
obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm
82518251
exact containsKey_of_mem hm
82528252

8253-
theorem List.minKey?_compare_eq_min?_map_fst [Ord α] [TransOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulEqOrd α]
8253+
theorem le_of_min_eq [Ord α] [TransOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] (a b : α) (h1 : min a b = a) (h2 : a ≠ b) : a ≤ b := by
8254+
apply Classical.byContradiction
8255+
intro hyp
8256+
rw [LawfulOrderLeftLeaningMin.min_eq_right a b hyp] at h1
8257+
rw [eq_comm] at h1
8258+
exact h2 h1
8259+
8260+
theorem le_of_min_eq2 [Ord α] [TransOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] (a b : α) (h1 : min a b = b) (h2 : a ≠ b) : ¬ a ≤ b := by
8261+
intro hyp
8262+
rw [LawfulOrderLeftLeaningMin.min_eq_left a b hyp] at h1
8263+
exact h2 h1
8264+
8265+
theorem trans_lemma [Ord α] [TransOrd α] [LE α] [Std.LawfulOrderOrd α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c := by
8266+
intro h1 h2
8267+
exact (LawfulOrderOrd.isLE_compare a c).1 <| TransOrd.isLE_trans ((LawfulOrderOrd.isLE_compare a b).2 h1) ((LawfulOrderOrd.isLE_compare b c).2 h2)
8268+
8269+
theorem total [Ord α] [OrientedOrd α] [LE α] [Std.LawfulOrderOrd α] (a b : α) : a ≤ b ∨ b ≤ a := by
8270+
rw [← LawfulOrderOrd.isLE_compare a b, ← LawfulOrderOrd.isLE_compare b a]
8271+
rw [OrientedOrd.eq_swap]
8272+
simp
8273+
generalize h : (compare b a) = x
8274+
cases x <;> simp
8275+
8276+
instance [LE α] [Min α] [Std.LawfulOrderMin α] : IdempotentOp (min : α → α → α) where
8277+
idempotent a := by
8278+
apply Or.elim <| MinEqOr.min_eq_or a a <;> (intro; trivial)
8279+
8280+
instance [Ord α] [OrientedOrd α] [TransOrd α] [Std.LawfulEqOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] : Commutative (min : α → α → α) where
8281+
comm a b := by
8282+
by_cases a_le_b : a ≤ b
8283+
case pos =>
8284+
rw [LawfulOrderLeftLeaningMin.min_eq_left a b a_le_b]
8285+
symm
8286+
by_cases a_eq_b : a = b
8287+
case pos =>
8288+
simp [a_eq_b, IdempotentOp.idempotent]
8289+
case neg =>
8290+
apply LawfulOrderLeftLeaningMin.min_eq_right
8291+
intro b_le_a
8292+
have w1 := (LawfulOrderOrd.isLE_compare a b).2 a_le_b
8293+
have w2 := (LawfulOrderOrd.isLE_compare b a).2 b_le_a
8294+
exact a_eq_b <| (LawfulEqOrd.compare_eq_iff_eq).1 <| OrientedCmp.isLE_antisymm w1 w2
8295+
case neg =>
8296+
rw [LawfulOrderLeftLeaningMin.min_eq_right a b a_le_b]
8297+
symm
8298+
by_cases a_eq_b : a = b
8299+
case pos =>
8300+
simp [a_eq_b, IdempotentOp.idempotent]
8301+
case neg =>
8302+
apply LawfulOrderLeftLeaningMin.min_eq_left
8303+
have := total a b
8304+
simp [a_le_b] at this
8305+
exact this
8306+
8307+
instance [Ord α] [TransOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] : Associative (min : α → α → α) where
8308+
assoc := by
8309+
intro a b c
8310+
apply Or.elim <| MinEqOr.min_eq_or a b
8311+
case left =>
8312+
intro h1
8313+
by_cases hab : (a = b)
8314+
case pos =>
8315+
rw [hab]
8316+
have : min b b = b := by
8317+
(apply Or.elim <| MinEqOr.min_eq_or b b) <;> (intro; trivial)
8318+
rw [this]
8319+
apply Or.elim <| MinEqOr.min_eq_or b c
8320+
case left =>
8321+
intro h2
8322+
simp [h2, IdempotentOp.idempotent]
8323+
case right =>
8324+
intro h3
8325+
simp [h3]
8326+
case neg =>
8327+
rw [h1]
8328+
apply Or.elim <| MinEqOr.min_eq_or b c
8329+
case left =>
8330+
intro h2
8331+
rw [h2, h1]
8332+
by_cases hbc : b = c
8333+
case pos =>
8334+
rw [← hbc, h1]
8335+
case neg =>
8336+
have w1 := le_of_min_eq a b h1 hab
8337+
have w2 := le_of_min_eq b c h2 hbc
8338+
exact LawfulOrderLeftLeaningMin.min_eq_left a c (trans_lemma w1 w2)
8339+
case right =>
8340+
intro h2
8341+
rw [h2]
8342+
case right =>
8343+
intro h1
8344+
rw [h1]
8345+
by_cases hab : (a = b)
8346+
case pos =>
8347+
rw [hab]
8348+
apply Or.elim <| MinEqOr.min_eq_or b c
8349+
case left =>
8350+
intro h2
8351+
rw [h2]
8352+
simp [IdempotentOp.idempotent]
8353+
case right =>
8354+
intro h2
8355+
simp [h2]
8356+
case neg =>
8357+
by_cases hbc : (b = c)
8358+
case pos =>
8359+
rw [← hbc]
8360+
simp [IdempotentOp.idempotent, h1]
8361+
case neg =>
8362+
apply Or.elim <| MinEqOr.min_eq_or b c
8363+
case left =>
8364+
intro h2
8365+
rw [h2, h1]
8366+
case right =>
8367+
intro h2
8368+
rw [h2]
8369+
apply Or.elim <| MinEqOr.min_eq_or a c
8370+
case left =>
8371+
intro h3
8372+
rw [h3]
8373+
have w1 := le_of_min_eq2 a b h1 hab
8374+
have w2 := le_of_min_eq2 b c h2 hbc
8375+
have w3 := le_of_min_eq a c h3
8376+
apply Classical.byContradiction
8377+
intro hn
8378+
specialize w3 (Ne.symm hn)
8379+
have v1 := total a b
8380+
have v2 := total b c
8381+
simp [w1] at v1
8382+
simp [w2] at v2
8383+
have a_leq_b := (LawfulOrderOrd.isLE_compare a b).1 <| TransOrd.isLE_trans ((LawfulOrderOrd.isLE_compare a c).2 w3) ((LawfulOrderOrd.isLE_compare c b).2 v2)
8384+
rw [LawfulOrderLeftLeaningMin.min_eq_left a b a_leq_b] at h1
8385+
exact hab h1
8386+
case right =>
8387+
intro h3
8388+
simp [h3]
8389+
8390+
theorem List.minKey?_compare_eq_min?_map_fst [Ord α] [OrientedOrd α] [TransOrd α] [Std.LawfulEqOrd α] [LE α] [Min α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
82548391
(l : List ((a : α) × β a)) :
82558392
List.minKey? l = (l.map Sigma.fst).min? := by
82568393
induction l
82578394
case nil =>
82588395
simp [minKey?_of_isEmpty]
82598396
case cons h t ih =>
8260-
simp [minKey?, minEntry?_cons]
8261-
simp [minEntry?]
8397+
rw [minKey?, minEntry?_cons]
8398+
rw [minEntry?]
8399+
rw [Option.map_some, List.map_cons]
82628400
split
8263-
case h_1 => sorry
8401+
case h_1 _ heq =>
8402+
simp [← ih, minKey?, minEntry?, heq]
82648403
case h_2 _ w heq =>
8265-
have : Associative (min : α → α → α) := by sorry
82668404
simp [List.min?_cons]
8405+
rw [← ih]
8406+
rw [minKey?]
8407+
rw [minEntry?, heq]
82678408
simp [min]
82688409
split
8269-
case isTrue heq2 =>
8270-
rw [← ih]
8271-
simp [Option.elim]
8272-
split
8273-
case h_1 _ _ v heq3 =>
8274-
rw [minKey?, minEntry?] at heq3
8275-
rw [heq] at heq3
8276-
simp at heq3
8277-
rw [← heq3]
8278-
have leq := (@Std.LawfulOrderOrd.isLE_compare α _ _ _ h.fst w.fst).1 heq2
8279-
apply Or.elim <| @MinEqOr.min_eq_or α _ _ h.fst w.fst
8280-
case left =>
8281-
intro hyp
8282-
rw [hyp]
8283-
case right =>
8284-
intro hyp
8285-
rw [hyp]
8286-
have := @LawfulOrderInf.le_min_iff α _ _ _ w.fst h.fst w.fst
8287-
rw [hyp] at this
8288-
have := this.1 (by simp [← Std.LawfulOrderOrd.isLE_compare])
8289-
letI inst : Antisymm (α := α) (· ≤ ·) := by
8290-
constructor
8291-
intro a b
8292-
sorry
8293-
apply @Antisymm.antisymm (α := α) (· ≤ ·) inst
8294-
· exact leq
8295-
· exact this.1
8296-
8297-
8298-
8299-
8300-
case isFalse => sorry
8301-
8302-
8303-
8304-
8305-
8306-
8307-
8308-
8309-
8310-
8311-
8312-
8313-
8314-
8315-
8316-
case isFalse heq =>
8317-
sorry
8318-
8319-
8320-
8321-
8322-
8323-
8324-
8325-
8326-
8327-
8328-
8329-
8330-
8331-
8332-
8333-
8334-
8335-
8410+
case isTrue hyp =>
8411+
have := (LawfulOrderOrd.isLE_compare h.fst w.fst).1 hyp
8412+
have := LawfulOrderLeftLeaningMin.min_eq_left h.fst w.fst this
8413+
rw [this]
8414+
case isFalse hyp =>
8415+
simp only [Bool.not_eq_true, Ordering.isLE_eq_false] at hyp
8416+
have w_le_h := (LawfulOrderOrd.isGE_compare h.fst w.fst).1 (Ordering.isGE_of_eq_gt hyp)
8417+
rw [@Commutative.comm _ min _ h.fst w.fst]
8418+
symm
8419+
apply LawfulOrderLeftLeaningMin.min_eq_left
8420+
exact w_le_h
83368421

83378422
theorem minKey?_eraseKey_eq_iff_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
83388423
{k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :

0 commit comments

Comments
 (0)