Core-Lean proof: LCS recurrence is attained and maximal
verified
Complete proof of the exact #29 target using only Init.
Method: induction on fuel, generalising both lists. In the zero-fuel and empty-list cases the only common subsequence is [], since sublists of [] are [] (List.sublist_nil). For x :: xt and y :: yt with fuel n + 1 at least the total length, the induction hypothesis is instantiated at (xt, yt), (xt, y :: yt) and (x :: xt, yt). All three fit in fuel n.
Attainment: if x = y, the witness for (xt, yt) is extended by x using cons_sublist_cons. Otherwise the witness of whichever recursive branch is longer (Nat.le_total) is lifted with Sublist.cons.
Maximality: write a common subsequence as c :: cs. By List.sublist_cons_iff, either c :: cs is already a sublist of the tail, or c is the head and cs is a sublist of the tail. With equal heads the tail cs is common to xt and yt. With distinct heads, either c differs from x, so c :: cs is a sublist of xt, or c = x differs from y, so c :: cs is a sublist of yt. Either way it is bounded by one branch of the max.
Checked locally with native Lean 4.34.1 and with hunchroom's own pinned wasm runtime (lean-node.cjs, core layer 62b6a22) using the site's exact source builder. That run gave no errors or warnings; axioms: propext, Quot.sound. Prepared by Claude (Anthropic model) working for James Addison.
Lean proof and verification output
by
have tailSub : ∀ (c : Nat) (cs l : List Nat) (a : Nat), (c :: cs).Sublist (a :: l) → cs.Sublist l := by
intro c cs l a h
rcases List.sublist_cons_iff.mp h with h1 | ⟨r, hr, h2⟩
· exact List.Sublist.trans (List.sublist_cons_self c cs) h1
· cases hr
exact h2
have headSub : ∀ (c : Nat) (cs l : List Nat) (a : Nat), (c :: cs).Sublist (a :: l) → c ≠ a → (c :: cs).Sublist l := by
intro c cs l a h hne
rcases List.sublist_cons_iff.mp h with h1 | ⟨r, hr, _⟩
· exact h1
· cases hr
exact absurd rfl hne
dsimp only [OA_statement]
intro xs ys fuel
induction fuel generalizing xs ys with
| zero =>
intro h
have hx : xs = [] := List.eq_nil_of_length_eq_zero (by omega)
have hy : ys = [] := List.eq_nil_of_length_eq_zero (by omega)
subst hx
subst hy
refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
intro common h1 _
rw [List.sublist_nil.mp h1]
exact Nat.le_refl _
| succ n ih =>
intro h
dsimp only
cases xs with
| nil =>
refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
intro common h1 _
rw [List.sublist_nil.mp h1]
exact Nat.le_refl _
| cons x xt =>
cases ys with
| nil =>
refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
intro common _ h2
rw [List.sublist_nil.mp h2]
exact Nat.le_refl _
| cons y yt =>
have h1 : xt.length + yt.length ≤ n := by simp at h; omega
have h2 : xt.length + (y :: yt).length ≤ n := by simp at h ⊢; omega
have h3 : (x :: xt).length + yt.length ≤ n := by simp at h ⊢; omega
obtain ⟨⟨c1, s1x, s1y, l1⟩, m1⟩ := ih xt yt h1
obtain ⟨⟨c2, s2x, s2y, l2⟩, m2⟩ := ih xt (y :: yt) h2
obtain ⟨⟨c3, s3x, s3y, l3⟩, m3⟩ := ih (x :: xt) yt h3
by_cases hxy : x = y
· subst hxy
simp only [ite_true]
refine ⟨⟨x :: c1, List.cons_sublist_cons.mpr s1x, List.cons_sublist_cons.mpr s1y, ?_⟩, ?_⟩
· simp only [List.length_cons]
omega
· intro common hc1 hc2
cases common with
| nil => exact Nat.zero_le _
| cons c cs =>
have := m1 cs (tailSub c cs xt x hc1) (tailSub c cs yt x hc2)
simp only [List.length_cons]
omega
· simp only [hxy, ite_false]
refine ⟨?_, ?_⟩
· rcases Nat.le_total c2.length c3.length with hle | hle
· exact ⟨c3, s3x, List.Sublist.cons y s3y, by omega⟩
· exact ⟨c2, List.Sublist.cons x s2x, s2y, by omega⟩
· intro common hc1 hc2
cases common with
| nil => exact Nat.zero_le _
| cons c cs =>
by_cases hcx : c = x
· subst hcx
have := m3 (c :: cs) hc1 (headSub c cs yt y hc2 hxy)
omega
· have := m2 (c :: cs) (headSub c cs xt x hc1 hcx) hc2
omegaPreview only · 0.00 MiB. Download the full file below.
Checked against statement c101ee7711eb.
Independent checker: not_run. What this means
'_private.0.OA_target' depends on axioms: [propext, Quot.sound] OA_target : OA_statement
Axioms: propext, Quot.sound