Lean4
theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n :=
by
refine ⟨fun h => ?_, fun ⟨k, h⟩ => evaln_sound h⟩
rsuffices ⟨k, h⟩ : ∃ k, x ∈ evaln (k + 1) c n
· exact ⟨k + 1, h⟩
induction c generalizing n x with simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
| pair cf cg hf hg =>
rcases h with ⟨x, hx, y, hy, rfl⟩
rcases hf hx with ⟨k₁, hk₁⟩; rcases hg hy with ⟨k₂, hk₂⟩
refine ⟨max k₁ k₂, ?_⟩
refine
⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂,
rfl⟩
| comp cf cg hf hg =>
rcases h with ⟨y, hy, hx⟩
rcases hg hy with ⟨k₁, hk₁⟩; rcases hf hx with ⟨k₂, hk₂⟩
refine ⟨max k₁ k₂, ?_⟩
exact
⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩
| prec cf cg hf hg =>
revert h
generalize n.unpair.1 = n₁; generalize n.unpair.2 = n₂
induction n₂ generalizing x n with simp [Option.bind_eq_some_iff]
| zero =>
intro h
rcases hf h with ⟨k, hk⟩
exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
| succ m IH =>
intro y hy hx
rcases IH hy with ⟨k₁, nk₁, hk₁⟩
rcases hg hx with ⟨k₂, hk₂⟩
refine
⟨(max k₁ k₂).succ, Nat.le_succ_of_le <| le_max_of_le_left <| le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y,
evaln_mono (Nat.succ_le_succ <| le_max_left _ _) ?_,
evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩
simp only [evaln.eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some_iff,
Option.guard_eq_some', exists_and_left, exists_const]
exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩
| rfind' cf hf =>
rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
suffices ∃ k, y + n.unpair.2 ∈ evaln (k + 1) (rfind' cf) (Nat.pair n.unpair.1 n.unpair.2) by
simpa [evaln, Option.bind_eq_some_iff]
revert hy₁ hy₂
generalize n.unpair.2 = m
intro hy₁ hy₂
induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
| zero =>
simp at hy₁
rcases hf hy₁ with ⟨k, hk⟩
exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
| succ y IH =>
rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
rcases hf ha with ⟨k₁, hk₁⟩
rcases
IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁) fun {i} hi => by
simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₂ (Nat.succ_lt_succ hi) with
⟨k₂, hk₂⟩
use (max k₁ k₂).succ
rw [zero_add] at hk₁
use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
use a
use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
simpa [a0, add_comm, add_left_comm] using evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
| _ => exact ⟨⟨_, le_rfl⟩, h.symm⟩
