Last active
May 15, 2018 20:04
-
-
Save Rotsor/8eeca2df21fed071b1fbdec7eec5168f to your computer and use it in GitHub Desktop.
Fulcrum in lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Solution for the "Fulcrum" problem from "The Great Theorem Prover Showdown" | |
| -- (https://www.hillelwayne.com/post/theorem-prover-showdown/) | |
| -- | |
| -- I am novice with Lean so the verbosity is almost certainly my | |
| -- fault and not that of Lean. | |
| import system.io | |
| universes u v w | |
| ----------------------------------------- | |
| -- Spec | |
| structure Total_order(A : Sort u) := | |
| (leq : A → A → Prop) | |
| (refl : ∀ x, leq x x) | |
| (trans : ∀ {a b c}, leq a b → leq b c → leq a c) | |
| (total : ∀ a b, leq a b ∨ leq b a) | |
| namespace list | |
| def summ : list ℤ → ℤ := list.foldr (+) 0 | |
| end list | |
| def measure1 : list ℤ × list ℤ → ℤ := | |
| λ t, | |
| abs (list.summ t.fst - list.summ t.snd) | |
| def O : Total_order (list ℤ × list ℤ) := | |
| { | |
| leq := (λ a b, measure1 a <= measure1 b), | |
| refl := begin | |
| intro x, | |
| refl | |
| end, | |
| trans := λ _ _ _ le1 le2, int.le_trans le1 le2, | |
| total := (λ a b, int.le_total (measure1 a) (measure1 b)) | |
| } | |
| def is_min {A : Type u} (O : Total_order A) (P : A → Prop) (x : A) := | |
| P x ∧ (∀ y, P y → O.leq x y) | |
| @[simp] def Good (fulcrum : list ℤ → list ℤ × list ℤ) := | |
| ∀ l, is_min O (λ t, t.fst ++ t.snd = l) (fulcrum l) | |
| ------------------------ | |
| -- Implementation | |
| namespace slist | |
| def t := @subtype (list ℤ × ℤ) (λ t, list.summ t.fst = t.snd) | |
| def nil : t := ⟨ ([], 0), refl _ ⟩ | |
| def cons (x : ℤ) (xs : t) : t := | |
| ⟨ (x :: xs.val.fst, x + xs.val.snd), congr_arg (λ q, x + q) xs.property ⟩ | |
| def to_list (t : t) := t.val.fst | |
| def of_list : list ℤ → t := | |
| list.foldr cons nil | |
| def summ (x : t) := x.val.snd | |
| end slist | |
| def mn {A} (O : Total_order A) [decidable_rel O.leq] : A → A → A := | |
| (λ a b, if O.leq a b then a else b) | |
| @[simp] | |
| def minimum_by {A} | |
| (O : Total_order A) | |
| [decidable_rel O.leq] | |
| (l : list A) : option A := | |
| list.foldr (λ (x : A) accum, some (option.rec x (λ y, mn O x y) accum)) none l | |
| def measure1' := λ (l : slist.t × slist.t), abs (slist.summ l.fst - slist.summ l.snd) | |
| def O' : Total_order (slist.t × slist.t) := | |
| { | |
| leq := (λ a b, measure1' a <= measure1' b), | |
| refl := begin | |
| intro, | |
| refl | |
| end, | |
| trans := λ _ _ _ le1 le2, int.le_trans le1 le2, | |
| total := (λ a b, int.le_total (measure1' a) (measure1' b)) | |
| } | |
| instance O'_decidable : decidable_rel O'.leq := | |
| -- the next line seems dumb: there must be an easier way of doing it | |
| λ a b, if prf : measure1' a <= measure1' b then is_true prf else is_false prf | |
| def res := slist.t × list (slist.t × slist.t) | |
| def step (x : ℤ) (next : slist.t → res) (rev_prefix : slist.t) : res := | |
| let next := next (slist.cons x rev_prefix) in | |
| let suffix := next.fst in | |
| let results := next.snd in | |
| let suffix := slist.cons x suffix in | |
| (suffix, ((rev_prefix, suffix) :: results)) | |
| def pre_fulcrum0 (l : list ℤ) : slist.t → res := | |
| list.foldr | |
| step | |
| (λ prefixx, ((slist.nil, (prefixx, slist.nil) :: []) : res)) | |
| l | |
| def pre_fulcrum := λ l, (pre_fulcrum0 l slist.nil).snd | |
| def fulcrum0 : list ℤ → (slist.t × slist.t) := | |
| λ l, match minimum_by O' (pre_fulcrum l) with | |
| | none := (slist.nil, slist.nil) -- unreachable code | |
| | some x := x | |
| end | |
| def fulcrum := λ l, | |
| let res := fulcrum0 l in | |
| (list.reverse (slist.to_list res.fst), slist.to_list res.snd) | |
| ------------------------ | |
| -- Proof | |
| namespace list | |
| @[simp] theorem summ_nil : summ nil = 0 := refl _ | |
| @[simp] theorem summ_cons : ∀ {x xs}, summ (x :: xs) = x + summ xs := λ _ _, refl _ | |
| theorem summ_rev_append : ∀ a b, summ (list.reverse_core a b) = summ a + summ b := | |
| begin | |
| intro a, | |
| induction a with x xs h, | |
| { | |
| intro b, | |
| simp, | |
| refl, | |
| }, | |
| { | |
| intro b, | |
| simp [summ_cons], | |
| have h' := h (x :: b), | |
| refine (trans h' _), | |
| simp | |
| } | |
| end | |
| @[simp] theorem summ_reverse : ∀ l, summ (list.reverse l) = summ l := | |
| begin | |
| intro l, | |
| have h := summ_rev_append l [], | |
| simp at h, | |
| exact h | |
| end | |
| end list | |
| namespace slist | |
| def of_list_alternative : list ℤ → t := λ l, ⟨ (l, list.summ l), by refl ⟩ | |
| def of_list_semantics : ∀ l, of_list l = of_list_alternative l := | |
| λ l, begin | |
| induction l with x a ih1, | |
| refl, | |
| rw (_ : of_list (x :: a) = cons x (of_list a)), | |
| { | |
| rw ih1, | |
| refl, | |
| }, | |
| refl | |
| end | |
| @[simp] def to_list_of_list : ∀ l, to_list (of_list l) = l := | |
| λ l, begin | |
| rw [of_list_semantics l], | |
| refl | |
| end | |
| def summ_of_list : ∀ l, summ (of_list l) = list.summ l := | |
| begin | |
| intro l, | |
| rw [of_list_semantics l], | |
| refl | |
| end | |
| inductive same {A : Sort u} : A → A → Sort u | |
| | refl : ∀ {x}, same x x | |
| def same_subst : ∀ {A : Sort u} (P : A → Sort v), ∀ {x y}, same x y → P x → P y | |
| := λ A P x y s p, | |
| let motive (x y : A) (s : same x y) : Sort v := P x → P y in | |
| (@same.rec_on _ motive x y s (λ x (p : P x), p) : motive x y s) p | |
| def subtype_eq {A} {P : A → Prop} : ∀ {x y : subtype P}, x.val = y.val → x = y := | |
| begin | |
| intros x y, | |
| intro eq1, | |
| induction x, | |
| induction y, | |
| simp at *, | |
| exact eq1 | |
| end | |
| @[simp] def wf_canonical : ∀ x, of_list (to_list x) = x := | |
| begin | |
| intros x, | |
| have : of_list_alternative (to_list x) = x, | |
| { | |
| induction x with x_val x_prop, simp [to_list, of_list_alternative], | |
| refine (subtype_eq _), | |
| simp, | |
| rw x_prop, | |
| simp, | |
| }, | |
| exact (eq.trans (of_list_semantics _) this), | |
| end | |
| def induction : ∀ {C : t → Prop}, (∀ l, C (of_list l)) → ∀ x, C x := | |
| λ P h x, | |
| let res : P (of_list (to_list x)) := h x.val.fst in | |
| by begin | |
| exact (eq.subst (wf_canonical x) res), | |
| end | |
| end slist | |
| namespace proof | |
| def lift_rel {A B : Type u} (Rel : A → A → Prop) (f : B → A) : B → B → Prop := | |
| λ x y, Rel (f x) (f y) | |
| def lifted_implication {A B₁ B₂ : Type u} (f₁ : B₁ → A) (f₂ : B₂ → A) (Rel : A → A → Prop) | |
| (R : B₁ → B₂ → Prop) (correspond : ∀ {x₁ x₂}, R x₁ x₂ → f₁ x₁ = f₂ x₂) | |
| : (∀ {x₁ y₁ x₂ y₂}, R x₁ x₂ → R y₁ y₂ → lift_rel Rel f₁ x₁ y₁ → lift_rel Rel f₂ x₂ y₂) | |
| := | |
| begin | |
| intros x₁ y₁ x₂ y₂ r₁ r₂ rel, | |
| unfold lift_rel at *, | |
| rw (correspond r₁) at rel, | |
| rw (correspond r₂) at rel, | |
| exact rel | |
| end | |
| @[simp] theorem pre_fulcrum0_step : | |
| ∀ x (l : list ℤ), pre_fulcrum0 (x :: l) = step x (pre_fulcrum0 l) := λ _ _, refl _ | |
| theorem list_rev_core' : ∀ {A} (a : list A), ∀ {q b}, list.reverse_core a (q ++ b) = list.reverse_core a q ++ b := | |
| begin | |
| intro A, | |
| intro a, | |
| induction a with _ _ h, | |
| begin | |
| intros q b, | |
| refl | |
| end, | |
| unfold list.reverse_core, | |
| intros q b, | |
| exact (@h (_ :: q) b) | |
| end | |
| @[simp] theorem rev_nil : ∀ {A}, list.reverse (list.nil) = (list.nil : list A) := | |
| λ A, eq.refl _ | |
| @[simp] theorem rev_core_nil : ∀ {A} l, list.reverse_core list.nil l = (l : list A) := | |
| λ A l, eq.refl _ | |
| @[simp] theorem list_rev_rev_core : ∀ {A} (a b c : list A), list.reverse_core (list.reverse_core a b) c = list.reverse_core b (a ++ c) := | |
| begin | |
| intros A a, | |
| induction a with x _ h, | |
| { intros, refl }, | |
| { | |
| intros b c, | |
| exact (h (x :: b) c) | |
| } | |
| end | |
| @[simp] theorem list_rev_rev : ∀ {A} (l : list A), list.reverse (list.reverse l) = l := | |
| begin | |
| intros, | |
| unfold list.reverse, | |
| simp | |
| end | |
| def pre_fulcrum_correct_result : list ℤ → (slist.t → res) → Prop := | |
| λ suffix f, (∀ (rev_prefix : slist.t), | |
| ( | |
| let r : res := f rev_prefix in | |
| let qq := r in | |
| let suffix' := r.fst in | |
| let results := r.snd in | |
| suffix' = slist.of_list suffix | |
| ∧ ∀ (x : slist.t × slist.t), | |
| (x ∈ results) ↔ | |
| (∃ a b, | |
| slist.to_list x.fst = list.reverse_core a (slist.to_list rev_prefix) | |
| ∧ a ++ b = suffix | |
| ∧ b = slist.to_list x.snd))) | |
| def match1 {A} {R : list A → Type} | |
| (empty : R []) (nonempty : ∀ x xs, R (x :: xs)) : (∀ l, R l) | |
| := λ l, l.rec empty (λ _ _ _, nonempty _ _) | |
| def uncons {A} (l : list A) : (¬ (l = [])) → A × list A := | |
| match l with | |
| | list.nil := λ nonempty, false.elim (nonempty (eq.refl _)) | |
| | x :: xs := λ _, (x, xs) | |
| end | |
| theorem mn_lemma1 {A} (O : Total_order A) [decidable_rel O.leq] : ∀ a b, mn O a b = a ∨ mn O a b = b := | |
| λ a b, | |
| begin | |
| unfold mn, | |
| by_cases h : (O.leq a b), | |
| { simp [h] }, | |
| { simp [h] } | |
| end | |
| theorem mn_lemma2 {A} (O : Total_order A) [decidable_rel O.leq] : ∀ a b, O.leq (mn O a b) a ∧ O.leq (mn O a b) b := | |
| begin | |
| intros a b, | |
| have total := O.total a b, | |
| unfold mn, | |
| by_cases (O.leq a b), | |
| { | |
| simp [h], | |
| exact (O.refl _) | |
| }, | |
| { | |
| refine (or.elim total _ _), | |
| { contradiction }, | |
| { | |
| intro h2, | |
| simp [h], | |
| exact (and.intro h2 (O.refl _)) | |
| } | |
| } | |
| end | |
| theorem list_induction1 : ∀ {A} {P : list A → Prop}, P [] → (∀ x xs, P (x :: xs)) → ∀ x, P x | |
| := λ A P z nz x, | |
| begin | |
| induction x, | |
| exact z, | |
| exact (nz _ _) | |
| end | |
| theorem step_correct : | |
| ∀ x l r, | |
| pre_fulcrum_correct_result l r | |
| → pre_fulcrum_correct_result (x :: l) (step x r) | |
| := | |
| begin | |
| intros x l r0 h, | |
| intro rev_suffix, | |
| let r := r0 (slist.cons x rev_suffix), | |
| have q := h (slist.cons x rev_suffix), | |
| have q1 := and.left q, | |
| have q2 := and.right q, | |
| clear q, | |
| clear h, | |
| simp, | |
| unfold step, | |
| simp, | |
| apply and.intro, | |
| { | |
| clear q2, | |
| exact (congr_arg (λ y, slist.cons x y) q1) | |
| }, | |
| { | |
| intro elem, | |
| induction elem with left_half right_half, | |
| refine (iff.intro _ _), | |
| { | |
| intro in_list, | |
| refine (or.elim in_list _ _), | |
| { | |
| intro at_head, | |
| simp at *, | |
| injection at_head with eq1 eq2, | |
| rw [eq1, eq2] at *, | |
| clear eq1 eq2 at_head left_half right_half, | |
| let right_half := slist.cons x r.fst, | |
| simp at *, | |
| refine (exists.intro [] (exists.intro (slist.to_list right_half) _)), | |
| apply and.intro, | |
| { | |
| refl | |
| }, | |
| simp, | |
| refine (congr_arg (λ q, x :: q) _), | |
| rw [← slist.to_list_of_list l], | |
| have zz := (congr_arg (λ (q : slist.t), slist.to_list q) q1), | |
| simp at *, | |
| exact zz | |
| }, | |
| -- at tail | |
| { | |
| clear in_list, | |
| intro at_tail, | |
| have rec := (q2 (left_half, right_half)).mp at_tail, | |
| refine (exists.elim rec _), | |
| clear rec, | |
| intros a rec, | |
| refine (exists.elim rec _), | |
| clear rec, | |
| intros b rec, | |
| refine (exists.intro (x :: a) _), | |
| refine (exists.intro b _), | |
| apply and.intro, | |
| exact (rec.left), | |
| apply and.intro, | |
| { | |
| have rec := rec.right.left, | |
| exact (congr_arg (λ q, x :: q) rec) | |
| }, | |
| exact rec.right.right | |
| } | |
| }, | |
| { | |
| intro ex, | |
| refine (exists.elim ex _), | |
| clear ex, | |
| intro a, | |
| induction a using proof.list_induction1 with a_hd a_tl, | |
| { -- here | |
| clear q2, | |
| intro ex, | |
| refine (or.intro_left _ _), | |
| have q1 : (r0 (slist.cons x rev_suffix)).fst = slist.of_list l := q1, | |
| rewrite q1, | |
| refine (exists.elim ex _), | |
| clear ex, | |
| intro b, | |
| intro ex, | |
| exact (match ex with | |
| | ⟨ | |
| left_half_is_prefix, | |
| whatever, | |
| right_half_is_suffix ⟩ := by begin | |
| clear _match, | |
| clear ex, | |
| simp at *, | |
| rw whatever at *, | |
| clear whatever, | |
| clear b, | |
| induction right_half using slist.induction, | |
| induction left_half using slist.induction, | |
| simp at *, | |
| rw ←right_half_is_suffix, | |
| rw left_half_is_prefix, | |
| simp at *, | |
| refl | |
| end | |
| end | |
| ) | |
| }, | |
| { -- there | |
| intro ex, | |
| refine (or.intro_right _ _), | |
| refine ((q2 (left_half, right_half)).mpr _), | |
| clear q2, | |
| clear q1, | |
| refine (exists.intro a_tl _), | |
| refine (exists.elim ex _), | |
| clear ex, | |
| intros b ex, | |
| refine (exists.intro b _), | |
| exact ( | |
| match ex with | |
| | ⟨ left_half_eq, ab_is_suffix, right_half_eq ⟩ := begin | |
| clear ex _match, | |
| injection ab_is_suffix with eq1 eq2, | |
| rw eq1 at *, | |
| rw ←eq2 at *, | |
| clear ab_is_suffix, | |
| apply and.intro, | |
| exact left_half_eq, | |
| apply and.intro, | |
| refl, | |
| exact right_half_eq | |
| end | |
| end | |
| ) | |
| } | |
| } | |
| } | |
| end | |
| theorem pre_fulcrum_correct : | |
| ∀ l, pre_fulcrum_correct_result l (pre_fulcrum0 l) | |
| := λ l, by begin | |
| induction l, | |
| begin | |
| unfold pre_fulcrum0, | |
| unfold list.foldr, | |
| exact (λ rev_prefix, begin | |
| apply and.intro, | |
| exact (eq.refl _), | |
| intro elem, | |
| apply iff.intro, | |
| begin | |
| simp, | |
| intro e, | |
| rw e, | |
| simp, | |
| apply exists.intro list.nil, | |
| apply exists.intro list.nil, | |
| simp, | |
| refl, | |
| end, | |
| simp, | |
| intro h, | |
| induction h with a h, | |
| induction h with b h, | |
| induction h with b_def h, | |
| induction h with ab_empty h, | |
| induction a, | |
| case list.cons { contradiction }, | |
| induction b, | |
| case list.cons { contradiction }, | |
| clear ab_empty, | |
| induction elem with x y, | |
| simp at h, | |
| simp at *, | |
| rw (_ : x = rev_prefix), | |
| rw (_ : y = slist.nil), | |
| induction y using slist.induction with q, | |
| { | |
| induction q, | |
| case list.nil { refl }, | |
| case list.cons { contradiction } | |
| }, | |
| induction x using slist.induction with q p r, | |
| { | |
| induction rev_prefix using slist.induction, | |
| simp at *, | |
| rw ← b_def, | |
| } | |
| end) | |
| end, | |
| case list.cons : x rest h { | |
| exact (step_correct _ _ _ h) | |
| } | |
| end | |
| inductive is_correct_minimum_by {A} (O : Total_order A) [decidable_rel O.leq] : list A → option A → Prop | |
| | nil : is_correct_minimum_by [] none | |
| | non_nil : ∀ l min, is_min O (λ x, x ∈ l) min → is_correct_minimum_by l (some min) | |
| theorem correct_minimum_by_inductive_case | |
| {A} (O : Total_order A) [decidable_rel O.leq] : ∀ x l r, | |
| is_correct_minimum_by O l r → | |
| is_correct_minimum_by O (x :: l) ((λ (x : A) accum, some (option.rec x (λ y, mn O x y) accum : A)) x r) | |
| := begin | |
| simp, | |
| intros x l r r_correct, | |
| induction r_correct with _ r_min r_min_correct, | |
| { exact (is_correct_minimum_by.non_nil _ _ begin | |
| dsimp, | |
| unfold is_min, | |
| simp, | |
| intros _ eq1, | |
| rewrite eq1, | |
| exact (O.refl _) | |
| end) }, | |
| { | |
| simp, | |
| exact (is_correct_minimum_by.non_nil _ _ begin | |
| apply and.intro, | |
| { -- minimum is in the list | |
| dsimp, | |
| unfold mn, | |
| exact (if eq1 : O.leq x r_min then begin | |
| simp [eq1], | |
| end else | |
| begin | |
| simp [eq1], | |
| apply or.intro_right, | |
| exact r_min_correct.left | |
| end) | |
| }, | |
| { -- minimum is minimal | |
| intro min_candidate, | |
| intro in_list, | |
| have mn_good := mn_lemma2 O x r_min, | |
| refine (or.elim in_list _ _), | |
| { -- here | |
| intro eq1, | |
| rewrite eq1 at *, | |
| exact mn_good.left | |
| }, | |
| { -- there | |
| intro in_list, | |
| have hh := r_min_correct.right _ in_list, | |
| exact (O.trans mn_good.right hh) | |
| } | |
| } | |
| end) | |
| } | |
| --- exact (is_correct_minimum_by.non_nil l | |
| end | |
| theorem correct_minimum_by | |
| {A} (O : Total_order A) [decidable_rel O.leq] : ∀ l, is_correct_minimum_by O l (minimum_by O l) := | |
| begin | |
| intro l, | |
| induction l with x xs h, | |
| { exact (is_correct_minimum_by.nil _) }, | |
| { exact (correct_minimum_by_inductive_case O _ _ _ h) }, | |
| end | |
| theorem map_is_min {A₁ A₂ : Type u} (O₁ : Total_order A₁) (O₂ : Total_order A₂) (P₁ : A₁ → Prop) (P₂ : A₂ → Prop) | |
| (f : A₁ → A₂) | |
| (f_inverse : A₂ → A₁) | |
| (inverse1 : ∀ y, f (f_inverse y) = y) | |
| (p_preserved_1 : ∀ x, P₁ x → P₂ (f x)) | |
| (p_preserved_2 : ∀ y, P₂ y → P₁ (f_inverse y)) | |
| (Total_order_preserved : ∀ x y, P₁ x → P₁ y → O₁.leq x y → O₂.leq (f x) (f y)) | |
| (x : A₁) | |
| : is_min O₁ P₁ x → is_min O₂ P₂ (f x) := begin | |
| intro x_is_min, | |
| apply and.intro, | |
| { exact ((p_preserved_1 x) (x_is_min.left)) }, | |
| { | |
| intros fy pfy, | |
| let y := f_inverse fy, | |
| have eq1 : fy = f y := eq.symm (inverse1 fy), | |
| have pp : P₁ y := p_preserved_2 _ pfy, | |
| rewrite eq1 at *, | |
| have z := x_is_min.right y pp, | |
| exact (Total_order_preserved _ _ x_is_min.left pp z) | |
| } | |
| end | |
| theorem good : Good fulcrum := ( | |
| begin | |
| intro l, | |
| unfold fulcrum, | |
| dunfold fulcrum0, | |
| dunfold pre_fulcrum, | |
| generalize gen_prefulcrum : pre_fulcrum0 l = pre_fulcrum0_result, | |
| have pre_fulcrum_correct : pre_fulcrum_correct_result l pre_fulcrum0_result := | |
| begin | |
| have hh := pre_fulcrum_correct l, | |
| rewrite gen_prefulcrum at hh, | |
| exact hh, | |
| end, | |
| have fulcrum0_correct := pre_fulcrum_correct slist.nil, | |
| generalize gen_pre_fulcrum : ((pre_fulcrum0_result slist.nil).snd) = pre_fulcrum_result, | |
| generalize gen_min : (minimum_by O' pre_fulcrum_result = min_result), | |
| have correct_minimum : is_correct_minimum_by O' pre_fulcrum_result min_result := | |
| begin | |
| have hh := correct_minimum_by O' pre_fulcrum_result, | |
| rewrite gen_min at hh, | |
| exact hh | |
| end, | |
| induction correct_minimum with pfr min min_proof, | |
| { -- maybe returned [none]: impossible | |
| dsimp at *, | |
| rw ←gen_prefulcrum at *, | |
| simp at *, | |
| induction l, | |
| { | |
| contradiction | |
| }, | |
| { | |
| contradiction | |
| } | |
| }, | |
| { | |
| dsimp, | |
| clear pre_fulcrum_result, | |
| clear min_result, | |
| clear gen_min, | |
| dunfold fulcrum0._match_1, | |
| refine ( | |
| @map_is_min (slist.t × slist.t) (list ℤ × list ℤ) O' O | |
| (λ (x : slist.t × slist.t), x ∈ pfr) | |
| (λ (t : list ℤ × list ℤ), t.fst ++ t.snd = l) | |
| _ | |
| _ | |
| _ | |
| _ | |
| _ | |
| _ | |
| min | |
| min_proof | |
| ), | |
| exact (λ t, (slist.of_list (list.reverse t.fst), slist.of_list (t.snd))), | |
| { -- inverse | |
| intro y, | |
| induction y with fst snd, | |
| simp, | |
| }, | |
| { -- p_preserved_1 | |
| intro t, | |
| induction t with fst snd, | |
| simp, | |
| rw ←gen_pre_fulcrum, | |
| intro in_list, | |
| have ex := (fulcrum0_correct.right (fst, snd)).mp in_list, | |
| refine (exists.elim ex _), | |
| clear ex, | |
| intro a, | |
| intro ex, | |
| refine (exists.elim ex _), | |
| clear ex, | |
| intro b, | |
| intro proof, | |
| rw proof.left, | |
| rw ←proof.right.right, | |
| suffices : list.reverse (list.reverse a) ++ b = l, exact this, | |
| simp, | |
| exact proof.right.left | |
| }, | |
| { -- p_preserved_2 | |
| intro t, | |
| intro is_split, | |
| induction t with fst snd, | |
| have ex := (fulcrum0_correct.right (slist.of_list (list.reverse fst), slist.of_list snd)).mpr _, | |
| { | |
| rw ←gen_pre_fulcrum, | |
| simp at *, | |
| exact ex | |
| }, | |
| { | |
| refine (exists.intro fst (exists.intro snd _)), | |
| simp at *, | |
| refine (and.intro (eq.refl _) _), | |
| exact is_split | |
| } | |
| }, | |
| { -- O' leq implies O leq | |
| intros x y x_good y_good, | |
| refine (lifted_implication measure1' measure1 int.le _ _ _ _), | |
| exact (λ slists lists, | |
| slist.to_list slists.fst = list.reverse lists.fst | |
| ∧ slist.to_list slists.snd = lists.snd | |
| ), | |
| { -- measure1' ~ measure1 | |
| intros slists lists, | |
| intro good, | |
| induction slists with slist1 slist2, | |
| induction lists with list1 list2, | |
| unfold measure1 measure1', | |
| rewrite (_ : slist.summ slist1 = list.summ list1), | |
| rewrite (_ : slist.summ slist2 = list.summ list2), | |
| { | |
| simp at good, | |
| induction slist2 using slist.induction with h1 h2 h3, | |
| rewrite ←good.right, | |
| simp, | |
| rewrite slist.summ_of_list, | |
| }, | |
| { | |
| simp at good, | |
| induction slist1 using slist.induction with h1 h2 h3, | |
| rewrite (_ : list.summ list1 = list.summ (list.reverse list1)), | |
| rewrite ←good.left, | |
| simp, | |
| rewrite slist.summ_of_list, | |
| exact (eq.symm (list.summ_reverse _)), | |
| }, | |
| }, | |
| { -- x good | |
| rw ←gen_pre_fulcrum at *, | |
| have xr := (fulcrum0_correct.right x).mp x_good, | |
| refine (exists.elim xr (λ a ex, exists.elim ex _)), | |
| clear xr, | |
| clear ex, | |
| intro b, | |
| exact (λ rest, begin | |
| simp, | |
| end) | |
| }, | |
| { -- y good (unnecessary duplication with x good) | |
| rw ←gen_pre_fulcrum at *, | |
| have xr := (fulcrum0_correct.right y).mp y_good, | |
| refine (exists.elim xr (λ a ex, exists.elim ex _)), | |
| clear xr, | |
| clear ex, | |
| intro b, | |
| exact (λ rest, begin | |
| simp, | |
| end) | |
| }, | |
| } | |
| } | |
| end) | |
| end proof | |
| --------------------------------- | |
| -- Re-statement of the theorem | |
| theorem good : Good fulcrum := proof.good | |
| --------------------------------- | |
| -- Testing program | |
| def gen : ℕ → list ℕ := | |
| λ n, (nat.rec_on n ([], 0) (λ _ acc, | |
| let x := 1 + acc.snd in ((x :: acc.fst), x)) : list ℕ × ℕ).fst | |
| meta def go : ℕ → io unit := | |
| λ n, | |
| io.print_ln n >>= fun _, | |
| io.print_ln (measure1 (fulcrum (list.map int.of_nat (gen n)))) >>= fun _, | |
| io.stdout >>= fun handle, | |
| io.fs.flush handle >>= fun _, | |
| go (nat.succ n) | |
| meta def main : io unit := | |
| go 800000 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment