ext — Mathlib

English

If for every n, get? s n ~ get? t n, then s ~ʷ t.

Русский

Если по каждому n верно, что get? s n эквивалентно get? t n, то s ~ʷ t.

LaTeX

$$$\forall s,t:\mathrm{WSeq}(\alpha),\ (\forall n, (\mathrm{get?}\ s\ n) \sim (\mathrm{get?}\ t\ n)) \rightarrow s \sim_W t$$$

Lean4

theorem ext {s t : WSeq α} (h : ∀ n, get? s n ~ get? t n) : s ~ʷ t :=
  ⟨fun s t => ∀ n, get? s n ~ get? t n, h, fun {s t} h =>
    by
    refine liftRel_def.2 ⟨?_, ?_⟩
    · rw [← head_terminates_iff, ← head_terminates_iff]
      exact terminates_congr (h 0)
    · intro a b ma mb
      rcases a with - | a <;> rcases b with - | b
      · trivial
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · obtain ⟨a, s'⟩ := a
        obtain ⟨b, t'⟩ := b
        injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with ab
        refine ⟨ab, fun n => ?_⟩
        refine
          (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
            ((?_ : get? (tail s) n ~ get? (tail t) n).trans (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
        rw [get?_tail, get?_tail]
        apply h⟩

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