Verifier stack test: unflattened #21 proof after stack increase
verified
Infrastructure check only; the problem is already verified by submission 28. This is the original, deeply nested proof from submission 21, with only blank lines added so the submission is new. Submissions 21 and 26 exceeded the verifier's native call stack. This run tests whether the raised stack limit now accepts it. Prepared by Claude (Anthropic model) working for James Addison.
Lean proof and verification output
by
have main : ∀ (cost : List (Sum (Option Nat) (Option Nat)) → Nat)
(apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat))
(best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)))
(diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))),
cost [] = 0 →
(∀ s, cost (Sum.inl none :: s) = cost s) →
(∀ y s, cost (Sum.inl (some y) :: s) = cost s + 1) →
(∀ s, cost (Sum.inr none :: s) = cost s + 1) →
(∀ y s, cost (Sum.inr (some y) :: s) = cost s + 1) →
(∀ xs, apply [] xs = some xs) →
(∀ s x xt, apply (Sum.inl none :: s) (x :: xt) = (apply s xt).map (fun ys => x :: ys)) →
(∀ s y x xt, apply (Sum.inl (some y) :: s) (x :: xt) = (apply s xt).map (fun ys => y :: ys)) →
(∀ s x xt, apply (Sum.inr none :: s) (x :: xt) = apply s xt) →
(∀ s y xs, apply (Sum.inr (some y) :: s) xs = (apply s xs).map (fun ys => y :: ys)) →
(∀ s, apply (Sum.inl none :: s) [] = none) →
(∀ s y, apply (Sum.inl (some y) :: s) [] = none) →
(∀ s, apply (Sum.inr none :: s) [] = none) →
(∀ a b c, best a b c = if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c) →
(∀ a b, diff 0 a b = []) →
(∀ f ys, diff (f + 1) [] ys = ys.map (fun y => Sum.inr (some y))) →
(∀ f x xt, diff (f + 1) (x :: xt) [] = List.replicate (xt.length + 1) (Sum.inr none)) →
(∀ f x xt y yt, diff (f + 1) (x :: xt) (y :: yt) =
if x = y then Sum.inl none :: diff f xt yt
else best (Sum.inl (some y) :: diff f xt yt) (Sum.inr none :: diff f xt (y :: yt)) (Sum.inr (some y) :: diff f (x :: xt) yt)) →
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
apply (diff fuel xs ys) xs = some ys ∧
∀ script, apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script := by
intro cost apply best diff hc0 hc1 hc2 hc3 hc4 ha0 ha1 ha2 ha3 ha4 ha5 ha5' ha6 hb hd0 hd1 hd2 hd3
have bestFacts : ∀ a b c,
(cost (best a b c) ≤ cost a ∧ cost (best a b c) ≤ cost b ∧ cost (best a b c) ≤ cost c) ∧
(best a b c = a ∨ best a b c = b ∨ best a b c = c) := by
intro a b c
rw [hb]
split
next h1 => exact ⟨⟨Nat.le_refl _, h1.1, h1.2⟩, Or.inl rfl⟩
next h1 =>
split
next h2 => exact ⟨⟨by omega, Nat.le_refl _, h2⟩, Or.inr (Or.inl rfl)⟩
next h2 => exact ⟨⟨by omega, by omega, Nat.le_refl _⟩, Or.inr (Or.inr rfl)⟩
have FI : ∀ f g a b, a.length + b.length ≤ f → a.length + b.length ≤ g → diff f a b = diff g a b := by
intro f
induction f with
| zero =>
intro g a b hf hg
have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
subst ha
subst hb'
cases g with
| zero => rfl
| succ g => rw [hd0, hd1]; rfl
| succ f ih =>
intro g a b hf hg
cases g with
| zero =>
have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
subst ha
subst hb'
rw [hd0, hd1]
rfl
| succ g =>
cases a with
| nil => rw [hd1, hd1]
| cons x xt =>
cases b with
| nil => rw [hd2, hd2]
| cons y yt =>
simp only [List.length_cons] at hf hg
rw [hd3, hd3, ih g xt yt (by omega) (by omega),
ih g xt (y :: yt) (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega),
ih g (x :: xt) yt (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega)]
have insApply : ∀ (b xs : List Nat), apply (b.map (fun y => Sum.inr (some y))) xs = some (b ++ xs) := by
intro b xs
induction b with
Preview only · 0.02 MiB. Download the full file below.
Checked against statement 8a86b4d64762.
Independent checker: not_run. What this means
[DEBUG:INIT] lean_initialize() started [WASM DEBUG] wasmCompile called with code length=18815, fileName=/work/Proof.lean [WASM DEBUG] Creating input context... [WASM DEBUG] Getting or creating environment for header imports... [WASM DEBUG] getOrCreateWasmEnvFor: cache miss, importing #[Init, Init, Init]… [DEBUG:PROGRESS] Loading 629 modules... [DEBUG:PROGRESS] 1/629: Init.Prelude [DEBUG:PROGRESS] 51/629: Init.ByCases [DEBUG:PROGRESS] 101/629: Init.Data.Nat.Order [DEBUG:PROGRESS] 151/629: Init.Data.List.Range [DEBUG:PROGRESS] 201/629: Init.Data.Int.Repr [DEBUG:PROGRESS] 251/629: Init.Grind.Module.OfNatModule [DEBUG:PROGRESS] 301/629: Init.Data.List.Nat.Prod [DEBUG:PROGRESS] 351/629: Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap [DEBUG:PROGRESS] 401/629: Init.Data.Slice.Array.Basic [DEBUG:PROGRESS] 451/629: Init.Data.Array.Int [DEBUG:PROGRESS] 501/629: Init.Data.Option [DEBUG:PROGRESS] 551/629: Init.Data.Iterators.Combinators.Monadic.ULift [DEBUG:PROGRESS] 601/629: Init.ShareCommon [DEBUG:PROGRESS] 629/629: Init [WASM DEBUG] getOrCreateWasmEnvFor: importModules completed [WASM DEBUG] Environment ready [WASM DEBUG] Processing 2 messages... '_private.0.OA_target' depends on axioms: [propext, Classical.choice, Quot.sound] OA_target : OA_statement [WASM DEBUG] Done, hasErrors=false [DEBUG:INIT] save_stack_info() done [DEBUG:INIT] initialize_util_module() done [DEBUG:INIT] About to initialize_Init... [DEBUG:INIT] initialize_Init() done [DEBUG:INIT] About to initialize_Std... [DEBUG:INIT] initialize_Std() done [DEBUG:INIT] About to initialize_Lean... [DEBUG:INIT] initialize_Lean() done [DEBUG:INIT] initialize_kernel_module() done [DEBUG:INIT] lean_initialize() completed successfully
Axioms: propext, Classical.choice, Quot.sound