Skip to content

Instantly share code, notes, and snippets.

@Rotsor Rotsor/fulcrum.lean
Last active May 15, 2018

Embed
What would you like to do?
Fulcrum in lean
-- 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
You can’t perform that action at this time.