feat(library/data/finset/comb.lean): add filter, diff, theorems

library/data/finset/comb.lean

@@ -1,16 +1,16 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura, Jeremy Avigad
 
-Module: data.finset
+Combinators for finite sets.
-Author: Leonardo de Moura
-
-Combinators for finite sets
 -/
 import data.finset.basic logic.identities
 open list quot subtype decidable perm function
 
 namespace finset
+
+/- map -/
 section map
 variables {A B : Type}
 variable [h : decidable_eq B]
@@ -25,6 +25,84 @@ theorem map_empty (f : A → B) : map f ∅ = ∅ :=
 rfl
 end map
 
+/- filter and set-builder notation -/
+section filter
+  variables {A : Type} [deceq : decidable_eq A]
+  include deceq
+  variables (p : A → Prop) [decp : decidable_pred p] (s : finset A) {x : A}
+  include decp
+
+  definition filter : finset A :=
+  quot.lift_on s
+    (λl, to_finset_of_nodup
+      (list.filter p (subtype.elt_of l))
+      (list.nodup_filter p (subtype.has_property l)))
+    (λ l₁ l₂ u, quot.sound (perm.perm_filter u))
+
+  notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
+
+  theorem filter_empty : filter p ∅ = ∅ := rfl
+
+  variables {p s}
+
+  theorem of_mem_filter : x ∈ filter p s → p x :=
+  quot.induction_on s (take l, list.of_mem_filter)
+
+  theorem mem_of_mem_filter : x ∈ filter p s → x ∈ s :=
+  quot.induction_on s (take l, list.mem_of_mem_filter)
+
+  theorem mem_filter_of_mem {x : A} : x ∈ s → p x → x ∈ filter p s :=
+  quot.induction_on s (take l, list.mem_filter_of_mem)
+
+  variables (p s)
+
+  theorem mem_filter_eq : x ∈ filter p s = (x ∈ s ∧ p x) :=
+  propext (iff.intro
+    (assume H, and.intro (mem_of_mem_filter H) (of_mem_filter H))
+    (assume H, mem_filter_of_mem (and.left H) (and.right H)))
+end filter
+
+/- set difference -/
+section diff
+  variables {A : Type} [deceq : decidable_eq A]
+  include deceq
+
+  definition diff (s t : finset A) : finset A := {x ∈ s | x ∉ t}
+  infix `\`:70 := diff
+
+  theorem mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∈ s :=
+  mem_of_mem_filter H
+
+  theorem not_mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∉ t :=
+  of_mem_filter H
+
+  theorem mem_diff {s t : finset A} {x : A} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t :=
+  mem_filter_of_mem H1 H2
+
+  theorem mem_diff_iff (s t : finset A) (x : A) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t :=
+  iff.intro
+    (assume H, and.intro (mem_of_mem_diff H) (not_mem_of_mem_diff H))
+    (assume H, mem_diff (and.left H) (and.right H))
+
+  theorem mem_diff_eq (s t : finset A) (x : A) : x ∈ s \ t = (x ∈ s ∧ x ∉ t) :=
+  propext !mem_diff_iff
+
+  theorem union_diff_cancel {s t : finset A} (H : s ⊆ t) : s ∪ (t \ s) = t :=
+  ext (take x, iff.intro
+    (assume H1 : x ∈ s ∪ (t \ s),
+      or.elim (mem_or_mem_of_mem_union H1)
+        (assume H2 : x ∈ s, mem_of_subset_of_mem H H2)
+        (assume H2 : x ∈ t \ s, mem_of_mem_diff H2))
+    (assume H1 : x ∈ t,
+      decidable.by_cases
+        (assume H2 : x ∈ s, mem_union_left _ H2)
+        (assume H2 : x ∉ s, mem_union_right _ (mem_diff H1 H2))))
+
+  theorem diff_union_cancel {s t : finset A} (H : s ⊆ t) : (t \ s) ∪ s = t :=
+  eq.subst !union.comm (!union_diff_cancel H)
+end diff
+
+/- all -/
 section all
 variables {A : Type}
 definition all (s : finset A) (p : A → Prop) : Prop :=
@@ -32,6 +110,10 @@ quot.lift_on s
   (λ l, all (elt_of l) p)
   (λ l₁ l₂ p, foldr_eq_of_perm (λ a₁ a₂ q, propext !and.left_comm) p true)
 
+-- notation for bounded quantifiers
+notation `forallb` binders `∈` a `,` r:(scoped:1 P, P) := all a r
+notation `∀₀` binders `∈` a `,` r:(scoped:1 P, P) := all a r
+
 theorem all_empty (p : A → Prop) : all ∅ p = true :=
 rfl