michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/list/perm): cleanup theorem

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-08 09:29:40 -07:00
parent e0e65705db
commit ef1b057b63
1 changed files with 193 additions and 128 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

321
library/data/list/perm.lean
View file

@ -257,6 +257,70 @@ by_cases
inr (λ p : l₁ ~ l₂, absurd (length_eq_length_of_perm p) neql)) inr (λ p : l₁ ~ l₂, absurd (length_eq_length_of_perm p) neql))
end dec end dec
theorem discriminate {P : Prop} {l : list A} : (l = [] → P) → (∀ h t, l = h::t → P) → P :=
list.cases_on l
(λ h₁ h₂, h₁ rfl)
(λ a l h₁ h₂, h₂ a l rfl)
theorem discriminate₂ {P : Prop} {l : list A} : (l = [] → P) → (∀ a, l = [a] → P) → (∀ a₁ a₂ t, l = a₁::a₂::t → P) → P :=
list.cases_on l
(λ h₁ h₂ h₃, h₁ rfl)
(λ a₁ t, list.cases_on t
(λ h₁ h₂ h₃, h₂ a₁ rfl)
(λ a₂ t₂ h₁ h₂ h₃, h₃ a₁ a₂ t₂ rfl))
theorem tail_eq {a₁ a₂ : A} {t₁ t₂ : list A} : a₁::t₁ = a₂::t₂ → t₁ = t₂ :=
assume h, list.no_confusion h (λ e₁ e₂, e₂)
theorem head_eq {a₁ a₂ : A} {t₁ t₂ : list A} : a₁::t₁ = a₂::t₂ → a₁ = a₂ :=
assume h, list.no_confusion h (λ e₁ e₂, e₁)
-- Auxiliary theorem for performing cases-analysis on l₂.
-- We use it to prove perm_inv_core.
private theorem discr {P : Prop} {a b : A} {l₁ l₂ l₃ : list A} :
a::l₁ = l₂++(b::l₃) →
(l₂ = [] → a = b → l₁ = l₃ → P) →
(∀ t, l₂ = a::t → l₁ = t++(b::l₃) → P) → P :=
list.cases_on l₂
(λ e h₁ h₂, begin rewrite append_nil_left at e, exact (list.no_confusion e (λ e₁ e₂, h₁ rfl e₁ e₂)) end)
(λ h t e h₁ h₂, begin
rewrite append_cons at e, apply (list.no_confusion e), intros [e₁, e₂],
rewrite e₁ at h₂,
exact (h₂ t rfl e₂)
end)
-- Auxiliary theorem for performing cases-analysis on l₂.
-- We use it to prove perm_inv_core.
private theorem discr₂ {P : Prop} {a b c : A} {l₁ l₂ l₃ : list A} :
a::b::l₁ = l₂++(c::l₃) →
(l₂ = [] → l₃ = b::l₁ → a = c → P) →
(l₂ = [a] → b = c → l₁ = l₃ → P) →
(∀ t, l₂ = a::b::t → l₁ = t++(c::l₃) → P) → P :=
list.cases_on l₂
(λ e H₁ H₂ H₃,
begin
apply (list.no_confusion e), intros [a_eq_c, b_l₁_eq_l₃],
exact (H₁ rfl (eq.symm b_l₁_eq_l₃) a_eq_c)
end)
(λ h₁ t₁,
list.cases_on t₁
(λ e H₁ H₂ H₃,
begin
rewrite [append_cons at e, append_nil_left at e],
apply (list.no_confusion e), intros [a_eq_h₁, rest],
apply (list.no_confusion rest), intros [b_eq_c, l₁_eq_l₃],
rewrite [a_eq_h₁ at H₂, b_eq_c at H₂, l₁_eq_l₃ at H₂],
exact (H₂ rfl rfl rfl)
end)
(λ h₂ t₂ e H₁ H₂ H₃,
begin
rewrite [*append_cons at e],
apply (list.no_confusion e), intros [a_eq_h₁, rest],
apply (list.no_confusion rest), intros [b_eq_h₂, l₁_eq],
rewrite [a_eq_h₁ at H₃, b_eq_h₂ at H₃],
exact (H₃ t₂ rfl l₁_eq)
end))
/- permutation inversion -/ /- permutation inversion -/
theorem perm_inv_core {l₁ l₂ : list A} (p' : l₁ ~ l₂) : ∀ {a s₁ s₂}, l₁≈a|s₁ → l₂≈a|s₂ → s₁ ~ s₂ := theorem perm_inv_core {l₁ l₂ : list A} (p' : l₁ ~ l₂) : ∀ {a s₁ s₂}, l₁≈a|s₁ → l₂≈a|s₂ → s₁ ~ s₂ :=
perm_induction_on p' perm_induction_on p'
@ -266,137 +330,138 @@ perm_induction_on p'
(λ x t₁ t₂ p (r : ∀{a s₁ s₂}, t₁≈a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) a s₁ s₂ e₁ e₂, (λ x t₁ t₂ p (r : ∀{a s₁ s₂}, t₁≈a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) a s₁ s₂ e₁ e₂,
obtain (s₁₁ s₁₂ : list A) (C₁ : s₁ = s₁₁ ++ s₁₂ ∧ x::t₁ = s₁₁++(a::s₁₂)), from qeq_split e₁, obtain (s₁₁ s₁₂ : list A) (C₁ : s₁ = s₁₁ ++ s₁₂ ∧ x::t₁ = s₁₁++(a::s₁₂)), from qeq_split e₁,
obtain (s₂₁ s₂₂ : list A) (C₂ : s₂ = s₂₁ ++ s₂₂ ∧ x::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂, obtain (s₂₁ s₂₂ : list A) (C₂ : s₂ = s₂₁ ++ s₂₂ ∧ x::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂,
begin discr (and.elim_right C₁)
cases s₁₁ with [hs₁₁, ts₁₁], (λ (s₁₁_eq : s₁₁ = []) (x_eq_a : x = a) (t₁_eq : t₁ = s₁₂),
{ rewrite *append_nil_left at C₁, assert s₁_p : s₁ ~ t₂, from calc
apply (list.no_confusion (and.elim_right C₁)), intros [x_eq_a, t₁_eq_s₁₂], s₁ = s₁₁ ++ s₁₂ : and.elim_left C₁
rewrite [t₁_eq_s₁₂ at p, -and.elim_left C₁ at p], ... = t₁ : by rewrite [-t₁_eq, s₁₁_eq, append_nil_left]
cases s₂₁ with [hs₁₂, ts₁₂], ... ~ t₂ : p,
{ rewrite *append_nil_left at C₂, discr (and.elim_right C₂)
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a', t₂_eq_s₂₂], (λ (s₂₁_eq : s₂₁ = []) (x_eq_a : x = a) (t₂_eq: t₂ = s₂₂),
rewrite [t₂_eq_s₂₂ at p, -and.elim_left C₂ at p], proof calc
exact p}, s₁ ~ t₂ : s₁_p
{ rewrite *append_cons at C₂, ... = s₂₁ ++ s₂₂ : by rewrite [-t₂_eq, s₂₁_eq, append_nil_left]
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₁₂, t₂_eq_ts₁₂_a_s₂₂], ... = s₂ : by rewrite [and.elim_left C₂]
have eq₁ : s₂ = a :: ts₁₂ ++ s₂₂, begin rewrite [-x_eq_hs₁₂ at C₂, x_eq_a at C₂]; exact (and.elim_left C₂) end, qed)
have p₁ : s₁ ~ ts₁₂ ++ (a :: s₂₂), begin rewrite [t₂_eq_ts₁₂_a_s₂₂ at p]; exact p end, (λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
have p₂ : a :: ts₁₂ ++ s₂₂ ~ ts₁₂ ++ (a :: s₂₂), from !perm_middle, proof calc
rewrite eq₁, exact (trans p₁ (symm p₂))}}, s₁ ~ t₂ : s₁_p
{ rewrite *append_cons at C₁, ... = ts₂₁++(a::s₂₂) : t₂_eq
apply (list.no_confusion (and.elim_right C₁)), intros [x_eq_hs₁₁, t₁_eq_ts₁₁_a_s₁₂], ... ~ (a::ts₂₁)++s₂₂ : !perm_middle
rewrite [t₁_eq_ts₁₁_a_s₁₂ at p], ... = s₂₁ ++ s₂₂ : by rewrite [-x_eq_a, -s₂₁_eq]
cases s₂₁ with [hs₂₁, ts₂₁], ... = s₂ : by rewrite [and.elim_left C₂]
{ rewrite *append_nil_left at C₂, qed))
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, t₂_eq_s₂₂], (λ (ts₁₁ : list A) (s₁₁_eq : s₁₁ = x::ts₁₁) (t₁_eq : t₁ = ts₁₁++(a::s₁₂)),
rewrite [t₂_eq_s₂₂ at p, -and.elim_left C₂ at p], assert t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
have eq₁ : s₁ = a :: ts₁₁ ++ s₁₂, begin rewrite [-x_eq_hs₁₁ at C₁, x_eq_a at C₁], exact (and.elim_left C₁) end, assert s₁_eq : s₁ = x::(ts₁₁++s₁₂), from calc
have p₁ : ts₁₁ ++ (a :: s₁₂) ~ s₂, from p, s₁ = s₁₁ ++ s₁₂ : and.elim_left C₁
have p₂ : a :: ts₁₁ ++ s₁₂ ~ ts₁₁ ++ (a :: s₁₂), from !perm_middle, ... = x::(ts₁₁++ s₁₂) : by rewrite s₁₁_eq,
rewrite eq₁, exact (trans p₂ p₁)}, discr (and.elim_right C₂)
{ rewrite *append_cons at C₂, (λ (s₂₁_eq : s₂₁ = []) (x_eq_a : x = a) (t₂_eq: t₂ = s₂₂),
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, t₂_eq_ts₂₁_a_s₂₂], proof calc
have t₁qeq : t₁ ≈ a | (ts₁₁ ++ s₁₂), begin rewrite t₁_eq_ts₁₁_a_s₁₂, exact !qeq_app end, s₁ = a::(ts₁₁++s₁₂) : by rewrite [s₁_eq, x_eq_a]
have t₂qeq : t₂ ≈ a | (ts₂₁ ++ s₂₂), begin rewrite t₂_eq_ts₂₁_a_s₂₂, exact !qeq_app end, ... ~ ts₁₁++(a::s₁₂) : !perm_middle
have p₁ : x::(ts₁₁++s₁₂) ~ x::(ts₂₁++s₂₂), from skip x (r t₁qeq t₂qeq), ... = t₁ : t₁_eq
rewrite [and.elim_left C₁, and.elim_left C₂, -x_eq_hs₁₁, -x_eq_hs₂₁], ... ~ t₂ : p
exact p₁}} ... = s₂ : by rewrite [t₂_eq, and.elim_left C₂, s₂₁_eq, append_nil_left]
end) qed)
(λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
assert t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
proof calc
s₁ = x::(ts₁₁++s₁₂) : s₁_eq
... ~ x::(ts₂₁++s₂₂) : skip x (r t₁_qeq t₂_qeq)
... = s₂ : by rewrite [-append_cons, -s₂₁_eq, and.elim_left C₂]
qed)))
(λ x y t₁ t₂ p (r : ∀{a s₁ s₂}, t₁≈a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) a s₁ s₂ e₁ e₂, (λ x y t₁ t₂ p (r : ∀{a s₁ s₂}, t₁≈a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) a s₁ s₂ e₁ e₂,
obtain (s₁₁ s₁₂ : list A) (C₁ : s₁ = s₁₁ ++ s₁₂ ∧ y::x::t₁ = s₁₁++(a::s₁₂)), from qeq_split e₁, obtain (s₁₁ s₁₂ : list A) (C₁ : s₁ = s₁₁ ++ s₁₂ ∧ y::x::t₁ = s₁₁++(a::s₁₂)), from qeq_split e₁,
obtain (s₂₁ s₂₂ : list A) (C₂ : s₂ = s₂₁ ++ s₂₂ ∧ x::y::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂, obtain (s₂₁ s₂₂ : list A) (C₂ : s₂ = s₂₁ ++ s₂₂ ∧ x::y::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂,
begin discr₂ (and.elim_right C₁)
clears [e₁, e₂, p', l₁, l₂], (λ (s₁₁_eq : s₁₁ = []) (s₁₂_eq : s₁₂ = x::t₁) (y_eq_a : y = a),
cases s₁₁ with [hs₁₁, ts₁₁], assert s₁_p : s₁ ~ x::t₂, from calc
{ rewrite *append_nil_left at C₁, s₁ = s₁₁ ++ s₁₂ : and.elim_left C₁
apply (list.no_confusion (and.elim_right C₁)), intros [y_eq_a, hs₁₂_t₁_eq_s₁₂], ... = x::t₁ : by rewrite [s₁₂_eq, s₁₁_eq, append_nil_left]
rewrite [y_eq_a at *], clear y_eq_a, ... ~ x::t₂ : skip x p,
cases s₂₁ with [hs₂₁, ts₂₁], discr₂ (and.elim_right C₂)
{ rewrite *append_nil_left at C₂, (λ (s₂₁_eq : s₂₁ = []) (s₂₂_eq : s₂₂ = y::t₂) (x_eq_a : x = a),
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, t₂_eq_s₂₂], proof calc
rewrite [x_eq_a at *], clear x_eq_a, s₁ ~ x::t₂ : s₁_p
rewrite [and.elim_left C₁, and.elim_left C₂, -hs₁₂_t₁_eq_s₁₂, -t₂_eq_s₂₂], ... = s₂₁ ++ s₂₂ : by rewrite [x_eq_a, -y_eq_a, -s₂₂_eq, s₂₁_eq, append_nil_left]
exact (skip a p)}, ... = s₂ : by rewrite [and.elim_left C₂]
{ rewrite *append_cons at C₂, qed)
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, h_t₂_eq_ts₂₁_a_s₂₂], (λ (s₂₁_eq : s₂₁ = [x]) (y_eq_a : y = a) (t₂_eq : t₂ = s₂₂),
rewrite x_eq_hs₂₁ at *, clear x_eq_hs₂₁, proof calc
rewrite [and.elim_left C₁, and.elim_left C₂, -hs₁₂_t₁_eq_s₁₂], s₁ ~ x::t₂ : s₁_p
cases ts₂₁ with [hts₂₁, tts₂₁], ... = s₂₁ ++ s₂₂ : by rewrite [t₂_eq, s₂₁_eq, append_cons]
{ rewrite *append_nil_left at *, ... = s₂ : by rewrite [and.elim_left C₂]
have t₂_eq_s₂₂ : t₂ = s₂₂, from list.no_confusion h_t₂_eq_ts₂₁_a_s₂₂ (λ h t, t), qed)
rewrite -t₂_eq_s₂₂, (λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::y::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
exact (skip _ p)}, proof calc
{ rewrite append_cons at *, s₁ ~ x::t₂ : s₁_p
apply (list.no_confusion h_t₂_eq_ts₂₁_a_s₂₂), intros [a_eq_hts₂₁, t₂_eq_tts₂₁_a_s₂₂], ... = x::(ts₂₁++(y::s₂₂)) : by rewrite [t₂_eq, -y_eq_a]
rewrite [a_eq_hts₂₁ at t₂_eq_tts₂₁_a_s₂₂, t₂_eq_tts₂₁_a_s₂₂ at p], ... ~ x::y::(ts₂₁++s₂₂) : skip x !perm_middle
have p₁ : t₁ ~ tts₂₁ ++ (hts₂₁ :: s₂₂), from p, ... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq, append_cons]
have p₂ : tts₂₁ ++ (hts₂₁ :: s₂₂) ~ hts₂₁::(tts₂₁++s₂₂), from symm (!perm_middle), ... = s₂ : by rewrite [and.elim_left C₂]
exact (skip _ (trans p₁ p₂))}}}, qed))
{ rewrite *append_cons at *, (λ (s₁₁_eq : s₁₁ = [y]) (x_eq_a : x = a) (t₁_eq : t₁ = s₁₂),
apply (list.no_confusion (and.elim_right C₁)), intros [y_eq_hs₁₁, xt₁_eq_ts₁₁_a_s₁₂], assert s₁_p : s₁ ~ y::t₂, from calc
rewrite [-y_eq_hs₁₁ at C₁], clears [y_eq_hs₁₁, hs₁₁], s₁ = y::t₁ : by rewrite [and.elim_left C₁, s₁₁_eq, t₁_eq]
cases s₂₁ with [hs₂₁, ts₂₁], ... ~ y::t₂ : skip y p,
{ rewrite *append_nil_left at C₂, discr₂ (and.elim_right C₂)
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, y_t₂_eq_s₂₂], (λ (s₂₁_eq : s₂₁ = []) (s₂₂_eq : s₂₂ = y::t₂) (x_eq_a : x = a),
rewrite [-x_eq_a at (C₁, C₂, xt₁_eq_ts₁₁_a_s₁₂)], clears [x_eq_a, a], proof calc
cases ts₁₁ with [hts₁₁, tts₁₁], s₁ ~ y::t₂ : s₁_p
{ rewrite *append_nil_left at *, ... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq, s₂₂_eq]
apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [xeqx, t₁_eq_s₁₂], clears [xeqx, xt₁_eq_ts₁₁_a_s₁₂], ... = s₂ : by rewrite [and.elim_left C₂]
rewrite [t₁_eq_s₁₂ at p, and.elim_left C₂, -y_t₂_eq_s₂₂, and.elim_left C₁], qed)
exact (skip _ p)}, (λ (s₂₁_eq : s₂₁ = [x]) (y_eq_a : y = a) (t₂_eq : t₂ = s₂₂),
{ rewrite *append_cons at *, proof calc
apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_hts₁₁, t₁_eq_tts₁₁_x_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, s₁ ~ y::t₂ : s₁_p
rewrite [-x_eq_hts₁₁ at C₁], clears [x_eq_hts₁₁, hts₁₁], ... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq, t₂_eq, y_eq_a, -x_eq_a]
cases s₂₂ with [hs₂₂, ts₂₂], ... = s₂ : by rewrite [and.elim_left C₂]
{ apply (list.no_confusion y_t₂_eq_s₂₂) }, qed)
{ apply (list.no_confusion y_t₂_eq_s₂₂), intros [y_eq_hs₂₂, t₂_eq_ts₂₂], clear y_t₂_eq_s₂₂, (λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::y::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
rewrite [-y_eq_hs₂₂ at C₂, -t₂_eq_ts₂₂ at C₂, t₁_eq_tts₁₁_x_s₁₂ at p], proof calc
clears [y_eq_hs₂₂, t₂_eq_ts₂₂, t₁_eq_tts₁₁_x_s₁₂], s₁ ~ y::t₂ : s₁_p
have p₁ : x :: tts₁₁ ++ s₁₂ ~ t₂, from trans (!perm_middle) p, ... = y::(ts₂₁++(x::s₂₂)) : by rewrite [t₂_eq, -x_eq_a]
rewrite [and.elim_left C₁, and.elim_left C₂], ... ~ y::x::(ts₂₁++s₂₂) : skip y !perm_middle
exact (skip _ p₁)}}}, ... ~ x::y::(ts₂₁++s₂₂) : swap
{ rewrite *append_cons at *, ... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq]
apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, y_t₂_eq_ts₂₁_a_s₂₂], ... = s₂ : by rewrite [and.elim_left C₂]
rewrite [-x_eq_hs₂₁ at C₂], clears [x_eq_hs₂₁, hs₂₁], qed))
cases ts₁₁ with [hts₁₁, tts₁₁], (λ (ts₁₁ : list A) (s₁₁_eq : s₁₁ = y::x::ts₁₁) (t₁_eq : t₁ = ts₁₁++(a::s₁₂)),
{ rewrite *append_nil_left at *, assert s₁_eq : s₁ = y::x::(ts₁₁++s₁₂), by rewrite [and.elim_left C₁, s₁₁_eq],
apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_a, t₁_at_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, discr₂ (and.elim_right C₂)
rewrite [-x_eq_a at (C₁, C₂, y_t₂_eq_ts₂₁_a_s₂₂), -t₁_at_s₁₂ at C₁], clears [x_eq_a, a, t₁_at_s₁₂, s₁₂], (λ (s₂₁_eq : s₂₁ = []) (s₂₂_eq : s₂₂ = y::t₂) (x_eq_a : x = a),
cases ts₂₁ with [hts₂₁, tts₂₁], proof calc
{ rewrite *append_nil_left at *, s₁ = y::a::(ts₁₁++s₁₂) : by rewrite [s₁_eq, x_eq_a]
apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_x, t₂_eq_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, ... ~ y::(ts₁₁++(a::s₁₂)) : skip y !perm_middle
rewrite [y_eq_x at (C₁, C₂), -t₂_eq_s₂₂ at (C₁, C₂)], clears [y_eq_x, t₂_eq_s₂₂], ... = y::t₁ : by rewrite t₁_eq
rewrite [and.elim_left C₁, and.elim_left C₂], ... ~ y::t₂ : skip y p
exact (skip _ p)}, ... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq, s₂₂_eq]
{ rewrite *append_cons at *, ... = s₂ : by rewrite [and.elim_left C₂]
apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_hts₂₁, t₂_eq_tts₂₁_x_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, qed)
rewrite [-y_eq_hts₂₁ at C₂, t₂_eq_tts₂₁_x_s₂₂ at p], (λ (s₂₁_eq : s₂₁ = [x]) (y_eq_a : y = a) (t₂_eq : t₂ = s₂₂),
have p₁ : y::t₁ ~ y::x::(tts₂₁ ++ s₂₂), from skip y (trans p (symm !perm_middle)), proof calc
have p₂ : y::x::(tts₂₁ ++ s₂₂) ~ x::y::(tts₂₁ ++ s₂₂), from !swap, s₁ = y::x::(ts₁₁++s₁₂) : by rewrite s₁_eq
rewrite [and.elim_left C₁, and.elim_left C₂], ... ~ x::y::(ts₁₁++s₁₂) : swap
exact (trans p₁ p₂)}}, ... = x::a::(ts₁₁++s₁₂) : by rewrite y_eq_a
{ rewrite *append_cons at *, ... ~ x::(ts₁₁++(a::s₁₂)) : skip x !perm_middle
apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_hts₁₁, t₁_eq_tts₁₁_a_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, ... = x::t₁ : by rewrite t₁_eq
rewrite [-x_eq_hts₁₁ at C₁], clears [x_eq_hts₁₁, hts₁₁], ... ~ x::t₂ : skip x p
cases ts₂₁ with [hts₂₁, tts₂₁], ... = s₂₁ ++ s₂₂ : by rewrite [t₂_eq, s₂₁_eq]
{ rewrite *append_nil_left at *, ... = s₂ : by rewrite [and.elim_left C₂]
apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_a, t₂_eq_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, qed)
rewrite [-y_eq_a at (C₁, C₂, t₁_eq_tts₁₁_a_s₁₂), -t₂_eq_s₂₂ at C₂, t₁_eq_tts₁₁_a_s₁₂ at p], (λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::y::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
clears [y_eq_a, a, t₂_eq_s₂₂, s₂₂], assert t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
have p₁ : x::y::(tts₁₁ ++ s₁₂) ~ x::t₂, from skip x (trans !perm_middle p), assert t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
have p₂ : y::x::(tts₁₁ ++ s₁₂) ~ x::y::(tts₁₁ ++ s₁₂), from !swap, assert p_aux : ts₁₁++s₁₂ ~ ts₂₁++s₂₂, from r t₁_qeq t₂_qeq,
rewrite [and.elim_left C₁, and.elim_left C₂], proof calc
exact (trans p₂ p₁)}, s₁ = y::x::(ts₁₁++s₁₂) : by rewrite s₁_eq
{ rewrite *append_cons at *, ... ~ y::x::(ts₂₁++s₂₂) : skip y (skip x p_aux)
apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_hts₂₁, t₂_eq_tts₂₁_a_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, ... ~ x::y::(ts₂₁++s₂₂) : swap
rewrite [-y_eq_hts₂₁ at C₂], clears [y_eq_hts₂₁, hts₂₁], ... = s₂₁ ++ s₂₂ : by rewrite s₂₁_eq
have aux₁ : tts₁₁ ++ (a :: s₁₂) ≈ a|(tts₁₁ ++ s₁₂), from !qeq_app, ... = s₂ : by rewrite [and.elim_left C₂]
have aux₂ : tts₂₁ ++ (a :: s₂₂) ≈ a|(tts₂₁ ++ s₂₂), from !qeq_app, qed)))
rewrite [-t₁_eq_tts₁₁_a_s₁₂ at aux₁, -t₂_eq_tts₂₁_a_s₂₂ at aux₂],
have p₁ : y::x::(tts₁₁ ++ s₁₂) ~ y::x::(tts₂₁ ++ s₂₂), from skip y (skip x (r aux₁ aux₂)),
have p₂ : y::x::(tts₂₁ ++ s₂₂) ~ x::y::(tts₂₁ ++ s₂₂), from !swap,
rewrite [and.elim_left C₁, and.elim_left C₂],
exact (trans p₁ p₂)}}}}
end)
(λ t₁ t₂ t₃ p₁ p₂ (λ t₁ t₂ t₃ p₁ p₂
(r₁ : ∀{a s₁ s₂}, t₁ ≈ a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) (r₁ : ∀{a s₁ s₂}, t₁ ≈ a|s₁ → t₂≈a|s₂ → s₁ ~ s₂)
(r₂ : ∀{a s₁ s₂}, t₂ ≈ a|s₁ → t₃≈a|s₂ → s₁ ~ s₂) (r₂ : ∀{a s₁ s₂}, t₂ ≈ a|s₁ → t₃≈a|s₂ → s₁ ~ s₂)