Lean4
theorem lem (R : α → β → Prop) {S T} {U : WSeq α → WSeq β → Prop} (ST : LiftRel (LiftRel R) S T)
(HU :
∀ 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) →
U s1 s2)
{a} (ma : a ∈ destruct (join S)) : ∃ b, b ∈ destruct (join T) ∧ LiftRelO R U a b :=
by
obtain ⟨n, h⟩ := exists_results_of_mem ma; clear ma; revert S T ST a
induction n using Nat.strongRecOn with
| _ n IH
intro S T ST a ra; simp only [destruct_join] at ra
exact
let ⟨o, m, k, rs1, rs2, en⟩ := of_results_bind ra
let ⟨p, mT, rop⟩ := Computation.exists_of_liftRel_left (liftRel_destruct ST) rs1.mem
match o, p, rop, rs1, rs2, mT with
| none, none, _, _, rs2, mT => by
simp only [destruct_join]
exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
| some (s, S'), some (t, T'), ⟨st, ST'⟩, _, rs2, mT =>
by
simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
exact
let ⟨k1, rs3, ek⟩ := of_results_think rs2
let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
match o', p', rop', rs4, rs5, mt with
| none, none, _, _, rs5', mt =>
by
have : n1 < n := by
rw [en, ek, ek1]
apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
refine ⟨ob, ?_, rob⟩
· simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
apply mem_bind mT
simp only [destruct_append]
apply think_mem
apply mem_bind mt
exact mb
| some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt =>
by
simp only [destruct_append.aux] at rs5
refine ⟨some (b, append t' (join T')), ?_, ?_⟩
· simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
apply mem_bind mT
simp only [destruct_append]
apply think_mem
apply mem_bind mt
apply ret_mem
rw [eq_of_pure_mem rs5.mem]
exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩
