From e0e65705db72052b0a5ec4fb81429e790bcb768f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Apr 2015 18:54:02 -0700 Subject: [PATCH] feat(library/data/list/perm): add perm inversion theorems --- library/data/list/perm.lean | 165 +++++++++++++++++++++++++++++++++++- 1 file changed, 163 insertions(+), 2 deletions(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 97b7b8c11..931ca2023 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -64,7 +64,7 @@ calc_refl perm.refl calc_symm perm.symm calc_trans perm.trans -theorem mem_perm (a : A) (l₁ l₂ : list A) : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ := +theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ := assume p, perm.induction_on p (λ h, h) (λ x l₁ l₂ p₁ r₁ i, or.elim i @@ -246,7 +246,7 @@ definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁ absurd p₂ np) end) (assume nxinl₂ : x ∉ l₂, - inr (λ p : x::t₁ ~ l₂, absurd (mem_perm x (x::t₁) l₂ p !mem_cons) nxinl₂)) + inr (λ p : x::t₁ ~ l₂, absurd (mem_perm p !mem_cons) nxinl₂)) definition decidable_perm [instance] : ∀ (l₁ l₂ : list A), decidable (l₁ ~ l₂) := λ l₁ l₂, @@ -256,4 +256,165 @@ by_cases (assume neql : length l₁ ≠ length l₂, inr (λ p : l₁ ~ l₂, absurd (length_eq_length_of_perm p) neql)) end dec + +/- permutation inversion -/ +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' + (λ a s₁ s₂ e₁ e₂, + have innil : a ∈ [], from mem_head_of_qeq e₁, + absurd innil !not_mem_nil) + (λ 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₂, + begin + cases s₁₁ with [hs₁₁, ts₁₁], + { rewrite *append_nil_left at C₁, + apply (list.no_confusion (and.elim_right C₁)), intros [x_eq_a, t₁_eq_s₁₂], + rewrite [t₁_eq_s₁₂ at p, -and.elim_left C₁ at p], + cases s₂₁ with [hs₁₂, ts₁₂], + { rewrite *append_nil_left at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a', t₂_eq_s₂₂], + rewrite [t₂_eq_s₂₂ at p, -and.elim_left C₂ at p], + exact p}, + { rewrite *append_cons at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₁₂, t₂_eq_ts₁₂_a_s₂₂], + have eq₁ : s₂ = a :: ts₁₂ ++ s₂₂, begin rewrite [-x_eq_hs₁₂ at C₂, x_eq_a at C₂]; exact (and.elim_left C₂) end, + have p₁ : s₁ ~ ts₁₂ ++ (a :: s₂₂), begin rewrite [t₂_eq_ts₁₂_a_s₂₂ at p]; exact p end, + have p₂ : a :: ts₁₂ ++ s₂₂ ~ ts₁₂ ++ (a :: s₂₂), from !perm_middle, + rewrite eq₁, exact (trans p₁ (symm p₂))}}, + { rewrite *append_cons at C₁, + apply (list.no_confusion (and.elim_right C₁)), intros [x_eq_hs₁₁, t₁_eq_ts₁₁_a_s₁₂], + rewrite [t₁_eq_ts₁₁_a_s₁₂ at p], + cases s₂₁ with [hs₂₁, ts₂₁], + { rewrite *append_nil_left at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, t₂_eq_s₂₂], + rewrite [t₂_eq_s₂₂ at p, -and.elim_left C₂ at p], + have eq₁ : s₁ = a :: ts₁₁ ++ s₁₂, begin rewrite [-x_eq_hs₁₁ at C₁, x_eq_a at C₁], exact (and.elim_left C₁) end, + have p₁ : ts₁₁ ++ (a :: s₁₂) ~ s₂, from p, + have p₂ : a :: ts₁₁ ++ s₁₂ ~ ts₁₁ ++ (a :: s₁₂), from !perm_middle, + rewrite eq₁, exact (trans p₂ p₁)}, + { rewrite *append_cons at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, t₂_eq_ts₂₁_a_s₂₂], + have t₁qeq : t₁ ≈ a | (ts₁₁ ++ s₁₂), begin rewrite t₁_eq_ts₁₁_a_s₁₂, exact !qeq_app end, + have t₂qeq : t₂ ≈ a | (ts₂₁ ++ s₂₂), begin rewrite t₂_eq_ts₂₁_a_s₂₂, exact !qeq_app end, + have p₁ : x::(ts₁₁++s₁₂) ~ x::(ts₂₁++s₂₂), from skip x (r t₁qeq t₂qeq), + rewrite [and.elim_left C₁, and.elim_left C₂, -x_eq_hs₁₁, -x_eq_hs₂₁], + exact p₁}} + end) + (λ 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₂₂ ∧ x::y::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂, + begin + clears [e₁, e₂, p', l₁, l₂], + cases s₁₁ with [hs₁₁, ts₁₁], + { rewrite *append_nil_left at C₁, + apply (list.no_confusion (and.elim_right C₁)), intros [y_eq_a, hs₁₂_t₁_eq_s₁₂], + rewrite [y_eq_a at *], clear y_eq_a, + cases s₂₁ with [hs₂₁, ts₂₁], + { rewrite *append_nil_left at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, t₂_eq_s₂₂], + rewrite [x_eq_a at *], clear x_eq_a, + rewrite [and.elim_left C₁, and.elim_left C₂, -hs₁₂_t₁_eq_s₁₂, -t₂_eq_s₂₂], + exact (skip a p)}, + { rewrite *append_cons at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, h_t₂_eq_ts₂₁_a_s₂₂], + rewrite x_eq_hs₂₁ at *, clear x_eq_hs₂₁, + rewrite [and.elim_left C₁, and.elim_left C₂, -hs₁₂_t₁_eq_s₁₂], + cases ts₂₁ with [hts₂₁, tts₂₁], + { rewrite *append_nil_left at *, + have t₂_eq_s₂₂ : t₂ = s₂₂, from list.no_confusion h_t₂_eq_ts₂₁_a_s₂₂ (λ h t, t), + rewrite -t₂_eq_s₂₂, + exact (skip _ p)}, + { rewrite append_cons at *, + apply (list.no_confusion h_t₂_eq_ts₂₁_a_s₂₂), intros [a_eq_hts₂₁, t₂_eq_tts₂₁_a_s₂₂], + rewrite [a_eq_hts₂₁ at t₂_eq_tts₂₁_a_s₂₂, t₂_eq_tts₂₁_a_s₂₂ at p], + have p₁ : t₁ ~ tts₂₁ ++ (hts₂₁ :: s₂₂), from p, + have p₂ : tts₂₁ ++ (hts₂₁ :: s₂₂) ~ hts₂₁::(tts₂₁++s₂₂), from symm (!perm_middle), + exact (skip _ (trans p₁ p₂))}}}, + { rewrite *append_cons at *, + apply (list.no_confusion (and.elim_right C₁)), intros [y_eq_hs₁₁, xt₁_eq_ts₁₁_a_s₁₂], + rewrite [-y_eq_hs₁₁ at C₁], clears [y_eq_hs₁₁, hs₁₁], + cases s₂₁ with [hs₂₁, ts₂₁], + { rewrite *append_nil_left at C₂, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_a, y_t₂_eq_s₂₂], + rewrite [-x_eq_a at (C₁, C₂, xt₁_eq_ts₁₁_a_s₁₂)], clears [x_eq_a, a], + cases ts₁₁ with [hts₁₁, tts₁₁], + { rewrite *append_nil_left at *, + apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [xeqx, t₁_eq_s₁₂], clears [xeqx, xt₁_eq_ts₁₁_a_s₁₂], + rewrite [t₁_eq_s₁₂ at p, and.elim_left C₂, -y_t₂_eq_s₂₂, and.elim_left C₁], + exact (skip _ p)}, + { rewrite *append_cons at *, + apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_hts₁₁, t₁_eq_tts₁₁_x_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, + rewrite [-x_eq_hts₁₁ at C₁], clears [x_eq_hts₁₁, hts₁₁], + cases s₂₂ with [hs₂₂, ts₂₂], + { apply (list.no_confusion y_t₂_eq_s₂₂) }, + { apply (list.no_confusion y_t₂_eq_s₂₂), intros [y_eq_hs₂₂, t₂_eq_ts₂₂], clear y_t₂_eq_s₂₂, + rewrite [-y_eq_hs₂₂ at C₂, -t₂_eq_ts₂₂ at C₂, t₁_eq_tts₁₁_x_s₁₂ at p], + clears [y_eq_hs₂₂, t₂_eq_ts₂₂, t₁_eq_tts₁₁_x_s₁₂], + have p₁ : x :: tts₁₁ ++ s₁₂ ~ t₂, from trans (!perm_middle) p, + rewrite [and.elim_left C₁, and.elim_left C₂], + exact (skip _ p₁)}}}, + { rewrite *append_cons at *, + apply (list.no_confusion (and.elim_right C₂)), intros [x_eq_hs₂₁, y_t₂_eq_ts₂₁_a_s₂₂], + rewrite [-x_eq_hs₂₁ at C₂], clears [x_eq_hs₂₁, hs₂₁], + cases ts₁₁ with [hts₁₁, tts₁₁], + { rewrite *append_nil_left at *, + apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_a, t₁_at_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, + 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₁₂], + cases ts₂₁ with [hts₂₁, tts₂₁], + { rewrite *append_nil_left at *, + apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_x, t₂_eq_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, + rewrite [y_eq_x at (C₁, C₂), -t₂_eq_s₂₂ at (C₁, C₂)], clears [y_eq_x, t₂_eq_s₂₂], + rewrite [and.elim_left C₁, and.elim_left C₂], + exact (skip _ p)}, + { rewrite *append_cons at *, + 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₂₂, + rewrite [-y_eq_hts₂₁ at C₂, t₂_eq_tts₂₁_x_s₂₂ at p], + have p₁ : y::t₁ ~ y::x::(tts₂₁ ++ s₂₂), from skip y (trans p (symm !perm_middle)), + 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₂)}}, + { rewrite *append_cons at *, + apply (list.no_confusion xt₁_eq_ts₁₁_a_s₁₂), intros [x_eq_hts₁₁, t₁_eq_tts₁₁_a_s₁₂], clear xt₁_eq_ts₁₁_a_s₁₂, + rewrite [-x_eq_hts₁₁ at C₁], clears [x_eq_hts₁₁, hts₁₁], + cases ts₂₁ with [hts₂₁, tts₂₁], + { rewrite *append_nil_left at *, + apply (list.no_confusion y_t₂_eq_ts₂₁_a_s₂₂), intros [y_eq_a, t₂_eq_s₂₂], clear y_t₂_eq_ts₂₁_a_s₂₂, + rewrite [-y_eq_a at (C₁, C₂, t₁_eq_tts₁₁_a_s₁₂), -t₂_eq_s₂₂ at C₂, t₁_eq_tts₁₁_a_s₁₂ at p], + clears [y_eq_a, a, t₂_eq_s₂₂, s₂₂], + have p₁ : x::y::(tts₁₁ ++ s₁₂) ~ x::t₂, from skip x (trans !perm_middle p), + 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₁)}, + { rewrite *append_cons at *, + 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₂₂, + rewrite [-y_eq_hts₂₁ at C₂], clears [y_eq_hts₂₁, hts₂₁], + have aux₁ : tts₁₁ ++ (a :: s₁₂) ≈ a|(tts₁₁ ++ s₁₂), from !qeq_app, + have aux₂ : tts₂₁ ++ (a :: s₂₂) ≈ a|(tts₂₁ ++ s₂₂), from !qeq_app, + 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₂ + (r₁ : ∀{a s₁ s₂}, t₁ ≈ a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) + (r₂ : ∀{a s₁ s₂}, t₂ ≈ a|s₁ → t₃≈a|s₂ → s₁ ~ s₂) + a s₁ s₂ e₁ e₂, + have aint₁ : a ∈ t₁, from mem_head_of_qeq e₁, + have aint₂ : a ∈ t₂, from mem_perm p₁ aint₁, + obtain (t₂' : list A) (e₂' : t₂≈a|t₂'), from qeq_of_mem aint₂, + calc s₁ ~ t₂' : r₁ e₁ e₂' + ... ~ s₂ : r₂ e₂' e₂) + +theorem perm_cons_inv {a : A} {l₁ l₂ : list A} : a::l₁ ~ a::l₂ → l₁ ~ l₂ := +assume p, perm_inv_core p (qeq.qhead a l₁) (qeq.qhead a l₂) + +theorem perm_app_inv {a : A} {l₁ l₂ l₃ l₄ : list A} : l₁++(a::l₂) ~ l₃++(a::l₄) → l₁++l₂ ~ l₃++l₄ := +assume p : l₁++(a::l₂) ~ l₃++(a::l₄), + have p' : a::(l₁++l₂) ~ a::(l₃++l₄), from calc + a::(l₁++l₂) ~ l₁++(a::l₂) : perm_middle + ... ~ l₃++(a::l₄) : p + ... ~ a::(l₃++l₄) : symm (!perm_middle), + perm_cons_inv p' end perm