feat(library/data/set): show that (set A) is a comm_semiring

library/data/set/basic.lean

@@ -29,6 +29,15 @@ theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
 theorem subset.trans (a b c : set X) (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
 take x, assume ax, subbc (subab ax)
 
+theorem subset.antisymm (a b : set X) (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
+setext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
+
+definition strict_subset (a b : set X) := a ⊆ b ∧ a ≠ b
+infix `⊂`:50 := strict_subset
+
+theorem strict_subset.irrefl (a : set X) : ¬ a ⊂ a :=
+assume h, absurd rfl (and.elim_right h)
+
 /- bounded quantification -/
 
 abbreviation bounded_forall (a : set X) (P : X → Prop) := ∀⦃x⦄, x ∈ a → P x
@@ -57,6 +66,10 @@ theorem mem_univ (x : X) : x ∈ univ := trivial
 
 theorem mem_univ_eq (x : X) : x ∈ univ = true := rfl
 
+theorem empty_ne_univ [h : inhabited X] : (empty : set X) ≠ univ :=
+assume H : empty = univ,
+absurd (mem_univ (inhabited.value h)) (eq.rec_on H (not_mem_empty _))
+
 /- union -/
 
 definition union [reducible] (a b : set X) : set X := λx, x ∈ a ∨ x ∈ b
@@ -78,7 +91,7 @@ setext (take x, !false_or)
 theorem union.comm (a b : set X) : a ∪ b = b ∪ a :=
 setext (take x, or.comm)
 
-theorem union_assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
+theorem union.assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
 setext (take x, or.assoc)
 
 /- intersection -/
@@ -105,6 +118,12 @@ setext (take x, !and.comm)
 theorem inter.assoc (a b c : set X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
 setext (take x, !and.assoc)
 
+theorem inter_univ (a : set X) : a ∩ univ = a :=
+setext (take x, !and_true)
+
+theorem univ_inter (a : set X) : univ ∩ a = a :=
+setext (take x, !true_and)
+
 /- distributivity laws -/
 
 theorem inter.distrib_left (s t u : set X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=

library/data/set/comm_semiring.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+
+(set A) is an instance of a commutative semiring
+-/
+import data.set.basic algebra.ring
+open algebra set
+
+definition set_comm_semiring [instance] (A : Type) : comm_semiring (set A) :=
+⦃ comm_semiring,
+  add           := union,
+  mul           := inter,
+  zero          := empty,
+  one           := univ,
+  add_assoc     := union.assoc,
+  add_comm      := union.comm,
+  zero_add      := empty_union,
+  add_zero      := union_empty,
+  mul_assoc     := inter.assoc,
+  mul_comm      := inter.comm,
+  zero_mul      := empty_inter,
+  mul_zero      := inter_empty,
+  one_mul       := univ_inter,
+  mul_one       := inter_univ,
+  left_distrib  := inter.distrib_left,
+  right_distrib := inter.distrib_right
+⦄