English
If S and T are related by an Equiv lifting, then their joins are weakly equivalent: join S ~ʷ join T.
Русский
Если S и T связаны отношением LiftRel Equiv, то их объединения (join) эквивалентны в слабом смысле: join S ~ʷ join T.
LaTeX
$$$ \forall S,T : \mathrm{WSeq}(\mathrm{WSeq}\,\alpha),\; h : \mathrm{LiftRel} \mathrm{Equiv} S T \Rightarrow \mathrm{join}\, S \sim_W \mathrm{join}\, T$$$
Lean4
theorem liftRel_join (R : α → β → Prop) {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (h : LiftRel (LiftRel R) S T) :
LiftRel R (join S) (join T) :=
⟨fun s1 s2 => ∃ s t S T, s1 = append s (join S) ∧ s2 = append t (join T) ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T,
⟨nil, nil, S, T, by simp, by simp, by simp, h⟩, fun {s1 s2} ⟨s, t, S, T, h1, h2, st, ST⟩ =>
by
rw [h1, h2]; rw [destruct_append, destruct_append]
apply Computation.liftRel_bind _ _ (liftRel_destruct st)
exact fun {o p} h =>
match o, p, h with
| some (a, s), some (b, t), ⟨h1, h2⟩ => by simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
| none, none, _ => by
-- We do not `dsimp` with `LiftRelO` since `liftRel_join.lem` uses `LiftRelO`.
dsimp only [destruct_append.aux, Computation.LiftRel]; constructor
· intro
apply liftRel_join.lem _ ST fun _ _ => id
· intro b mb
rw [← LiftRelO.swap]
apply liftRel_join.lem (swap R)
· rw [← LiftRel.swap R, ← LiftRel.swap]
apply ST
· rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
· exact mb⟩
