From 072971f3bbd98583820feebe96f977cbef33bba0 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 27 Aug 2015 14:26:21 -0400
Subject: [PATCH] feat(library/data/finset/comb,library/data/set/basic): define
 set complement

---
 library/data/finset/comb.lean | 32 ++++++++++++++++++++++++++++++++
 library/data/set/basic.lean   | 19 +++++++++++++++++++
 library/logic/identities.lean |  8 ++++++++
 3 files changed, 59 insertions(+)

diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index afce8c5f1e..335800a95b 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -212,6 +212,38 @@ 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
 
+/- set complement -/
+section complement
+
+variables {A : Type} [deceqA : decidable_eq A] [h : fintype A]
+include deceqA h
+
+definition complement (s : finset A) : finset A := univ \ s
+prefix [priority finset.prio] - := complement
+
+theorem mem_complement {s : finset A} {x : A} (H : x ∉ s) : x ∈ -s :=
+mem_diff !mem_univ H
+
+theorem not_mem_of_mem_complement {s : finset A} {x : A} (H : x ∈ -s) : x ∉ s :=
+not_mem_of_mem_diff H
+
+theorem mem_complement_iff (s : finset A) (x : A) : x ∈ -s ↔ x ∉ s :=
+iff.intro not_mem_of_mem_complement mem_complement
+
+section
+  open classical
+
+  theorem union_eq_comp_comp_inter_comp (s t : finset A) : s ∪ t = -(-s ∩ -t) :=
+  ext (take x, by rewrite [mem_union_iff, mem_complement_iff, mem_inter_iff, *mem_complement_iff,
+                           or_iff_not_and_not])
+
+  theorem inter_eq_comp_comp_union_comp (s t : finset A) : s ∩ t = -(-s ∪ -t) :=
+  ext (take x, by rewrite [mem_inter_iff, mem_complement_iff, mem_union_iff, *mem_complement_iff,
+                           and_iff_not_or_not])
+end
+
+end complement
+
 /- all -/
 section all
 variables {A : Type}
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 17d3fc6162..e0a7e554ec 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -266,6 +266,25 @@ ext (take x, iff.intro
   (suppose x ∈ s, and.intro (ssubt this) this)
   (suppose x ∈ {x ∈ t | x ∈ s}, and.right this))
 
+/- complement -/
+
+definition complement (s : set X) : set X := {x | x ∉ s}
+prefix `-` := complement
+
+theorem mem_complement {s : set X} {x : X} (H : x ∉ s) : x ∈ -s := H
+
+theorem not_mem_of_mem_complement {s : set X} {x : X} (H : x ∈ -s) : x ∉ s := H
+
+section
+  open classical
+
+  theorem union_eq_comp_comp_inter_comp (s t : set X) : s ∪ t = -(-s ∩ -t) :=
+  ext (take x, !or_iff_not_and_not)
+
+  theorem inter_eq_comp_comp_union_comp (s t : set X) : s ∩ t = -(-s ∪ -t) :=
+  ext (take x, !and_iff_not_or_not)
+end
+
 /- set difference -/
 
 definition diff (s t : set X) : set X := {x ∈ s | x ∉ t}
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 093b70f3a7..d5ba754fae 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -48,6 +48,14 @@ iff.intro
   (λH, by_cases (λa, or.inr (not.mto (and.intro a) H)) or.inl)
   (or.rec (not.mto and.left) (not.mto and.right))
 
+theorem or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  a ∨ b ↔ ¬ (¬a ∧ ¬b) :=
+by rewrite [-not_or_iff_not_and_not, not_not_iff]
+
+theorem and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
+  a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=
+by rewrite [-not_and_iff_not_or_not, not_not_iff]
+
 theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b :=
 iff.intro
   (by_cases (λHa H, or.inr (H Ha)) (λHa H, or.inl Ha))