feat(library/data/list): define intersection for lists

library/data/list/perm.lean

@@ -637,6 +637,49 @@ assume p, by_cases
    by rewrite [insert_eq_of_not_mem nainl₁, insert_eq_of_not_mem nainl₂]; exact (skip _ p))
 end perm_insert
 
+section perm_intersection
+variable [H : decidable_eq A]
+include H
+
+theorem perm_intersection_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (intersection l₁ t₁) ~ (intersection l₂ t₁) :=
+assume p, perm.induction_on p
+  !refl
+  (λ x l₁ l₂ p₁ r₁, by_cases
+    (λ xint₁  : x ∈ t₁, by rewrite [*intersection_cons_of_mem _ xint₁]; exact (skip x r₁))
+    (λ nxint₁ : x ∉ t₁, by rewrite [*intersection_cons_of_not_mem _ nxint₁]; exact r₁))
+  (λ x y l, by_cases
+    (λ yint  : y ∈ t₁, by_cases
+      (λ xint  : x ∈ t₁,
+        by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_mem _ yint, *intersection_cons_of_mem _ xint];
+           exact !swap)
+      (λ nxint : x ∉ t₁,
+        by rewrite [*intersection_cons_of_mem _ yint, *intersection_cons_of_not_mem _ nxint, intersection_cons_of_mem _ yint];
+           exact !refl))
+    (λ nyint : y ∉ t₁, by_cases
+      (λ xint  : x ∈ t₁,
+        by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_not_mem _ nyint, intersection_cons_of_mem _ xint];
+           exact !refl)
+      (λ nxint : x ∉ t₁,
+        by rewrite [*intersection_cons_of_not_mem _ nxint, *intersection_cons_of_not_mem _ nyint,
+                     intersection_cons_of_not_mem _ nxint];
+           exact !refl)))
+  (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
+
+theorem perm_intersection_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (intersection l t₁) ~ (intersection l t₂) :=
+list.induction_on l
+  (λ p, by rewrite [*intersection_nil]; exact !refl)
+  (λ x xs r p, by_cases
+    (λ xint₁  : x ∈ t₁,
+      assert xint₂ : x ∈ t₂, from mem_perm p xint₁,
+      by rewrite [intersection_cons_of_mem _ xint₁, intersection_cons_of_mem _ xint₂]; exact (skip _ (r p)))
+    (λ nxint₁ : x ∉ t₁,
+      assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
+      by rewrite [intersection_cons_of_not_mem _ nxint₁, intersection_cons_of_not_mem _ nxint₂]; exact (r p)))
+
+theorem perm_intersection {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (intersection l₁ t₁) ~ (intersection l₂ t₂) :=
+assume p₁ p₂, trans (perm_intersection_left t₁ p₁) (perm_intersection_right l₂ p₂)
+end perm_intersection
+
 /- extensionality -/
 section ext
 open eq.ops

library/data/list/set.lean

@@ -543,4 +543,81 @@ assume ainl, by rewrite [insert_eq_of_mem ainl]
 theorem length_insert_of_not_mem {a : A} {l : list A} : a ∉ l → length (insert a l) = length l + 1 :=
 assume nainl, by rewrite [insert_eq_of_not_mem nainl]
 end insert
+
+/- intersection -/
+section intersection
+variable {A : Type}
+variable [H : decidable_eq A]
+include H
+
+definition intersection : list A → list A → list A
+| []      l₂ := []
+| (a::l₁) l₂ := if a ∈ l₂ then a :: intersection l₁ l₂ else intersection l₁ l₂
+
+theorem intersection_nil (l : list A) : intersection [] l = []
+
+theorem intersection_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → intersection (a::l₁) l₂ = a :: intersection l₁ l₂ :=
+assume i, if_pos i
+
+theorem intersection_cons_of_not_mem {a : A} (l₁ : list A) {l₂} : a ∉ l₂ → intersection (a::l₁) l₂ = intersection l₁ l₂ :=
+assume i, if_neg i
+
+theorem mem_of_mem_intersection_left : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₁
+| []      l₂ a i := absurd i !not_mem_nil
+| (b::l₁) l₂ a i := by_cases
+  (λ binl₂  : b ∈ l₂,
+    have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i,
+    or.elim (eq_or_mem_of_mem_cons aux)
+      (λ aeqb : a = b, by rewrite [aeqb]; exact !mem_cons)
+      (λ aini, mem_cons_of_mem _ (mem_of_mem_intersection_left aini)))
+  (λ nbinl₂ : b ∉ l₂,
+    have ainl₁ : a ∈ l₁, by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_left i),
+    mem_cons_of_mem _ ainl₁)
+
+theorem mem_of_mem_intersection_right : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₂
+| []      l₂ a i := absurd i !not_mem_nil
+| (b::l₁) l₂ a i := by_cases
+  (λ binl₂  : b ∈ l₂,
+    have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i,
+    or.elim (eq_or_mem_of_mem_cons aux)
+      (λ aeqb : a = b, by rewrite [aeqb]; exact binl₂)
+      (λ aini : a ∈ intersection l₁ l₂, mem_of_mem_intersection_right aini))
+  (λ nbinl₂ : b ∉ l₂,
+    by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_right i))
+
+theorem mem_intersection_of_mem_of_men : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ intersection l₁ l₂
+| []      l₂ a i₁ i₂ := absurd i₁ !not_mem_nil
+| (b::l₁) l₂ a i₁ i₂ := by_cases
+  (λ binl₂  : b ∈ l₂,
+    or.elim (eq_or_mem_of_mem_cons i₁)
+      (λ aeqb  : a = b,
+        by rewrite [intersection_cons_of_mem _ binl₂, aeqb]; exact !mem_cons)
+     (λ ainl₁ : a ∈ l₁,
+        by rewrite [intersection_cons_of_mem _ binl₂];
+           apply mem_cons_of_mem;
+           exact (mem_intersection_of_mem_of_men ainl₁ i₂)))
+  (λ nbinl₂ : b ∉ l₂,
+    or.elim (eq_or_mem_of_mem_cons i₁)
+     (λ aeqb  : a = b, absurd (aeqb ▸ i₂) nbinl₂)
+     (λ ainl₁ : a ∈ l₁,
+       by rewrite [intersection_cons_of_not_mem _ nbinl₂]; exact (mem_intersection_of_mem_of_men ainl₁ i₂)))
+
+theorem nodup_intersection_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (intersection l₁ l₂)
+| []      l₂ d := nodup_nil
+| (a::l₁) l₂ d :=
+  have   d₁     : nodup l₁,                   from nodup_of_nodup_cons d,
+  assert d₂     : nodup (intersection l₁ l₂), from nodup_intersection_of_nodup _ d₁,
+  have   nainl₁ : a ∉ l₁,                     from not_mem_of_nodup_cons d,
+  assert naini  : a ∉ intersection l₁ l₂,     from λ i, absurd (mem_of_mem_intersection_left i) nainl₁,
+  by_cases
+    (λ ainl₂  : a ∈ l₂, by rewrite [intersection_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂))
+    (λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact d₂)
+
+theorem intersection_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → intersection l₁ l₂ = []
+| []      l₂ d := rfl
+| (a::l₁) l₂ d :=
+  assert aux_eq : intersection l₁ l₂ = [], from intersection_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d),
+  assert nainl₂ : a ∉ l₂,                  from disjoint_left d !mem_cons,
+  by rewrite [intersection_cons_of_not_mem _ nainl₂, aux_eq]
+end intersection
 end list