From c95bd8ba61d72e4faef27c676ac569e3a2413083 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Apr 2015 12:28:48 -0700 Subject: [PATCH] feat(library/data/list): add erase_dup and theorems --- library/data/list/basic.lean | 48 ++++++++++++++++++++++ library/data/list/perm.lean | 78 ++++++++++++++++++++++++++++++++++++ 2 files changed, 126 insertions(+) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 058f2fb1c..82024486d 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -806,6 +806,54 @@ lemma nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l end, absurd xinxs nxinxs, nodup_cons nfxinm ndmfxs + +definition erase_dup [H : decidable_eq A] : list A → list A +| [] := [] +| (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs + +theorem erase_dup_nil [H : decidable_eq A] : erase_dup [] = [] + +theorem erase_dup_cons_of_mem [H : decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l := +assume ainl, calc + erase_dup (a::l) = if a ∈ l then erase_dup l else a :: erase_dup l : rfl + ... = erase_dup l : if_pos ainl + +theorem erase_dup_cons_of_not_mem [H : decidable_eq A] {a : A} {l : list A} : a ∉ l → erase_dup (a::l) = a :: erase_dup l := +assume nainl, calc + erase_dup (a::l) = if a ∈ l then erase_dup l else a :: erase_dup l : rfl + ... = a :: erase_dup l : if_neg nainl + +theorem mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ erase_dup l +| [] h := absurd h !not_mem_nil +| (b::l) h := by_cases + (λ binl : b ∈ l, or.elim h + (λ aeqb : a = b, by rewrite [erase_dup_cons_of_mem binl, -aeqb at binl]; exact (mem_erase_dup binl)) + (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem binl]; exact (mem_erase_dup ainl))) + (λ nbinl : b ∉ l, or.elim h + (λ aeqb : a = b, by rewrite [erase_dup_cons_of_not_mem nbinl, aeqb]; exact !mem_cons) + (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_not_mem nbinl]; exact (or.inr (mem_erase_dup ainl)))) + +theorem mem_of_mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ erase_dup l → a ∈ l +| [] h := by rewrite [erase_dup_nil at h]; exact h +| (b::l) h := by_cases + (λ binl : b ∈ l, + have h₁ : a ∈ erase_dup l, by rewrite [erase_dup_cons_of_mem binl at h]; exact h, + or.inr (mem_of_mem_erase_dup h₁)) + (λ nbinl : b ∉ l, + have h₁ : a ∈ b :: erase_dup l, by rewrite [erase_dup_cons_of_not_mem nbinl at h]; exact h, + or.elim h₁ + (λ aeqb : a = b, by rewrite aeqb; exact !mem_cons) + (λ ainel : a ∈ erase_dup l, or.inr (mem_of_mem_erase_dup ainel))) + +theorem nodup_erase_dup [H : decidable_eq A] : ∀ l : list A, nodup (erase_dup l) +| [] := by rewrite erase_dup_nil; exact nodup_nil +| (a::l) := by_cases + (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem ainl]; exact (nodup_erase_dup l)) + (λ nainl : a ∉ l, + assert r : nodup (erase_dup l), from nodup_erase_dup l, + assert nin : a ∉ erase_dup l, from + assume ab : a ∈ erase_dup l, absurd (mem_of_mem_erase_dup ab) nainl, + by rewrite [erase_dup_cons_of_not_mem nainl]; exact (nodup_cons nin r)) end nodup end list diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 45a37554f..ff89b9f01 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -487,4 +487,82 @@ section fold_thms ... = foldl f a l₂ : foldl_eq_of_perm fcomm fassoc p ... = foldr f a l₂ : by rewrite [foldl_eq_foldr fcomm fassoc] end fold_thms + +theorem perm_erase_dup_of_perm [H : decidable_eq A] {l₁ l₂ : list A} : l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ := +assume p, perm_induction_on p + nil + (λ x t₁ t₂ p r, by_cases + (λ xint₁ : x ∈ t₁, + assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)), + by rewrite [erase_dup_cons_of_mem xint₁, erase_dup_cons_of_mem xint₂]; exact r) + (λ nxint₁ : x ∉ t₁, + assert nxint₂ : x ∉ t₂, from + assume xint₂ : x ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup xint₂))) nxint₁, + by rewrite [erase_dup_cons_of_not_mem nxint₂, erase_dup_cons_of_not_mem nxint₁]; exact (skip x r))) + (λ y x t₁ t₂ p r, by_cases + (λ xinyt₁ : x ∈ y::t₁, by_cases + (λ yint₁ : y ∈ t₁, + assert yint₂ : y ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁)), + assert yinxt₂ : y ∈ x::t₂, from or.inr (yint₂), + or.elim xinyt₁ + (λ xeqy : x = y, + assert xint₂ : x ∈ t₂, by rewrite [-xeqy at yint₂]; exact yint₂, + begin + rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂, + erase_dup_cons_of_mem yint₁, erase_dup_cons_of_mem xint₂], + exact r + end) + (λ xint₁ : x ∈ t₁, + assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)), + begin + rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂, + erase_dup_cons_of_mem yint₁, erase_dup_cons_of_mem xint₂], + exact r + end)) + (λ nyint₁ : y ∉ t₁, + assert nyint₂ : y ∉ t₂, from + assume yint₂ : y ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup yint₂))) nyint₁, + by_cases + (λ xeqy : x = y, + assert nxint₂ : x ∉ t₂, by rewrite [-xeqy at nyint₂]; exact nyint₂, + assert yinxt₂ : y ∈ x::t₂, by rewrite [xeqy]; exact !mem_cons, + begin + rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂, + erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂, xeqy], + exact (skip y r) + end) + (λ xney : x ≠ y, + have xint₁ : x ∈ t₁, from or_resolve_right xinyt₁ xney, + assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)), + assert nyinxt₂ : y ∉ x::t₂, from + assume yinxt₂ : y ∈ x::t₂, or.elim yinxt₂ (λ h, absurd h (ne.symm xney)) (λ h, absurd h nyint₂), + begin + rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_not_mem nyinxt₂, + erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_mem xint₂], + exact (skip y r) + end))) + (λ nxinyt₁ : x ∉ y::t₁, + have xney : x ≠ y, from not_eq_of_not_mem nxinyt₁, + have nxint₁ : x ∉ t₁, from not_mem_of_not_mem nxinyt₁, + assert nxint₂ : x ∉ t₂, from + assume xint₂ : x ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup xint₂))) nxint₁, + by_cases + (λ yint₁ : y ∈ t₁, + assert yinxt₂ : y ∈ x::t₂, from or.inr (mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁))), + begin + rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_mem yinxt₂, + erase_dup_cons_of_mem yint₁, erase_dup_cons_of_not_mem nxint₂], + exact (skip x r) + end) + (λ nyint₁ : y ∉ t₁, + assert nyinxt₂ : y ∉ x::t₂, from + assume yinxt₂ : y ∈ x::t₂, or.elim yinxt₂ + (λ h, absurd h (ne.symm xney)) + (λ h, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup h))) nyint₁), + begin + rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_not_mem nyinxt₂, + erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂], + exact (xswap x y r) + end))) + (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂, trans r₁ r₂) end perm