destruct_eq_cons — Mathlib

English

If destruct s equals some (a, s'), then s = cons a s'.

Русский

Если destruct s = some (a, s'), тогда s = cons a s'.

LaTeX

$$$\\forall {s:\\mathrm{Seq}\\alpha} {a:\\alpha} {s':\\mathrm{Seq}\\alpha},\\; \\mathrm{destruct}\\ s = \\mathrm{some}\\ (a,s') \\Rightarrow s = \\mathrm{cons}\\ a\\ s'.$$$

Lean4

theorem destruct_eq_cons {s : Seq α} {a s'} : destruct s = some (a, s') → s = cons a s' :=
  by
  dsimp [destruct]
  rcases f0 : get? s 0 with - | a' <;> intro h
  · contradiction
  · obtain ⟨f, al⟩ := s
    injections _ h1 h2
    rw [← h2]
    apply Subtype.eq
    dsimp [tail, cons]
    rw [h1] at f0
    rw [← f0]
    exact (Stream'.eta f).symm

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