English
If R is a relation and s1,t1,s2,t2 are WSeq α,β such that s1 LiftRel s t1 and s2 LiftRel s2 t2, then the concatenations append s1 s2 and append t1 t2 are LiftRel related: LiftRel R (append s1 s2) (append t1 t2).
Русский
Пусть R — отношение и пусть s1,t1, s2,t2 — WSeq α, β такие, что s1 связана с t1 отношением LiftRel R, и s2 связана с t2 LiftRel R. Тогда конкатенации append s1 s2 и append t1 t2 связаны отношением LiftRel R.
LaTeX
$$$ \forall R : \alpha \to \beta \to \mathrm{Prop},\; s_1,s_2 : \mathrm{WSeq}\,\alpha,\; t_1,t_2 : \mathrm{WSeq}\,\beta,\; \mathrm{LiftRel}\ R\ s_1\ t_1 \;\to\; \mathrm{LiftRel}\ R\ s_2\ t_2 \;\Rightarrow\; \mathrm{LiftRel}\ R\ (\mathrm{append}\ s_1 s_2) (\mathrm{append}\ t_1 t_2).$$$
Lean4
theorem liftRel_append (R : α → β → Prop) {s1 s2 : WSeq α} {t1 t2 : WSeq β} (h1 : LiftRel R s1 t1)
(h2 : LiftRel R s2 t2) : LiftRel R (append s1 s2) (append t1 t2) :=
⟨fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1,
Or.inr ⟨s1, t1, rfl, rfl, h1⟩, fun {s t} h =>
match s, t, h with
| s, t, Or.inl h => by
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)
intro a b; apply LiftRelO.imp_right
intro s t; apply Or.inl
| _, _, Or.inr ⟨s1, t1, rfl, rfl, h⟩ =>
by
simp only [exists_and_left, destruct_append]
apply Computation.liftRel_bind _ _ (liftRel_destruct h)
intro o p h
rcases o with - | a <;> rcases p with - | b
· simp only [destruct_append.aux]
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)
intro a b
apply LiftRelO.imp_right
intro s t
apply Or.inl
· cases b; cases h
· cases a; cases h
· obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
obtain ⟨r, h⟩ := h
simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩⟩
