eq_thinkN — Mathlib

English

If h : Results s a n, then s = thinkN (pure a) n.

Русский

Если h : Results s a n, то s = thinkN (pure a) n.

LaTeX

$$$$ \operatorname{Results} s a n \Rightarrow s = \mathrm{thinkN}(\mathrm{pure}\ a)\ n. $$$$

Lean4

theorem eq_thinkN {s : Computation α} {a n} (h : Results s a n) : s = thinkN (pure a) n :=
  by
  induction n generalizing s with
    | zero
    | succ n IH <;>
    induction s using recOn with
    | pure a'
    | think s
  · rw [← eq_of_pure_mem h.mem]
    rfl
  · obtain ⟨n, h⟩ := of_results_think h
    cases h
    contradiction
  · have := h.len_unique (results_pure _)
    contradiction
  · rw [IH (results_think_iff.1 h)]
    rfl

Похожие утверждения