feat(library/data/nat/bigops,library/data/set/card,library/*): add set versions of bigops for nat

This required splitting data/set/card.lean from data/set/finite.lean, to avoid dependencies

library/algebra/group_set_bigops.lean

@@ -82,6 +82,8 @@ section Sum
   notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
 
   theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f
+  theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → B) : Sum s f = 0 :=
+    Prod_of_not_finite nfins f
   theorem Sum_add (s : set A) (f g : A → B) :
     Sum s (λx, f x + g x) = Sum s f + Sum s g := Prod_mul s f g
 

library/data/encodable.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 Type class for encodable types.
 Note that every encodable type is countable.
 -/
-import data.fintype data.list data.sum data.nat data.subtype data.countable data.equiv
+import data.fintype data.list data.sum data.nat.div data.subtype data.countable data.equiv
 open option list nat function
 
 structure encodable [class] (A : Type) :=
@@ -72,7 +72,7 @@ theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = some s
   assert aux : 2 > 0, from dec_trivial,
   begin
     esimp [encode_sum, decode_sum],
-    rewrite [mul_mod_right, if_pos (eq.refl 0), mul_div_cancel_left _ aux, encodable.encodek]
+    rewrite [mul_mod_right, if_pos (eq.refl (0 : nat)), mul_div_cancel_left _ aux, encodable.encodek]
   end
 | (sum.inr b) :=
   assert aux₁ : 2 > 0,       from dec_trivial,

library/data/nat/bigops.lean

@@ -5,8 +5,8 @@ Author: Jeremy Avigad
 
 Finite products and sums on the natural numbers.
 -/
-import data.nat.basic data.nat.order algebra.group_bigops
+import data.nat.basic data.nat.order algebra.group_bigops algebra.group_set_bigops
-open list finset
+open list
 
 namespace nat
 open [classes] algebra
@@ -36,9 +36,10 @@ section deceqA
   theorem Prodl_one (l : list A) : Prodl l (λ x, nat.succ 0) = 1 := algebra.Prodl_one l
 end deceqA
 
-/- Prod -/
+/- Prod over finset -/
 
 namespace finset
+open finset
 
 definition Prod (s : finset A) (f : A → nat) : nat := algebra.finset.Prod s f
 notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
@@ -61,6 +62,32 @@ end deceqA
 
 end finset
 
+/- Prod over set -/
+
+namespace set
+open set
+
+noncomputable definition Prod (s : set A) (f : A → nat) : nat := algebra.set.Prod s f
+notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
+
+theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.set.Prod_empty f
+theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Prod s f = 1 :=
+  algebra.set.Prod_of_not_finite nfins f
+theorem Prod_mul (s : set A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
+  algebra.set.Prod_mul s f g
+theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) :
+  Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H
+theorem Prod_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
+  Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H
+theorem Prod_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
+    (disj : s₁ ∩ s₂ = ∅) :
+  Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj
+theorem Prod_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
+  Prod s f = Prod s g := algebra.set.Prod_ext H
+theorem Prod_one (s : set A) : Prod s (λ x, nat.succ 0) = 1 := algebra.set.Prod_one s
+
+end set
+
 /- Suml -/
 
 definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f
@@ -84,10 +111,10 @@ section deceqA
   theorem Suml_zero (l : list A) : Suml l (λ x, zero) = 0 := algebra.Suml_zero l
 end deceqA
 
-/- Sum -/
+/- Sum over a finset -/
 
 namespace finset
-
+open finset
 definition Sum (s : finset A) (f : A → nat) : nat := algebra.finset.Sum s f
 notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
 
@@ -109,4 +136,30 @@ end deceqA
 
 end finset
 
+/- Sum over a set -/
+
+namespace set
+open set
+
+noncomputable definition Sum (s : set A) (f : A → nat) : nat := algebra.set.Sum s f
+notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r
+
+theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.set.Sum_empty f
+theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Sum s f = 0 :=
+  algebra.set.Sum_of_not_finite nfins f
+theorem Sum_add (s : set A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
+  algebra.set.Sum_add s f g
+theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) :
+  Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H
+theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
+  Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H
+theorem Sum_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
+    (disj : s₁ ∩ s₂ = ∅) :
+  Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj
+theorem Sum_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
+  Sum s f = Sum s g := algebra.set.Sum_ext H
+theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s
+
+end set
+
 end nat

library/data/set/card.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Cardinality of finite sets.
+-/
+import .finite data.finset.card
+open nat
+
+namespace set
+
+variable {A : Type}
+
+noncomputable definition card (s : set A) := finset.card (set.to_finset s)
+
+theorem card_to_set (s : finset A) : card (finset.to_set s) = finset.card s :=
+by rewrite [↑card, to_finset_to_set]
+
+theorem card_of_not_finite {s : set A} (nfins : ¬ finite s) : card s = 0 :=
+by rewrite [↑card, to_finset_of_not_finite nfins]
+
+theorem card_empty : card (∅ : set A) = 0 :=
+by rewrite [-finset.to_set_empty, card_to_set]
+
+theorem card_insert_of_mem {a : A} {s : set A} (H : a ∈ s) : card (insert a s) = card s :=
+if fins : finite s then
+  (by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_mem H])
+else
+  (assert ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins,
+    by rewrite [card_of_not_finite fins, card_of_not_finite this])
+
+theorem card_insert_of_not_mem {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
+  card (insert a s) = card s + 1 :=
+by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_not_mem H]
+
+theorem card_insert_le (a : A) (s : set A) [fins : finite s] :
+  card (insert a s) ≤ card s + 1 :=
+if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ
+else by rewrite [card_insert_of_not_mem H]
+
+theorem card_singleton (a : A) : card '{a} = 1 :=
+by rewrite [card_insert_of_not_mem !not_mem_empty, card_empty]
+
+/- Note: the induction tactic does not work well with the set induction principle with the
+   extra predicate "finite". -/
+theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] : card s = 0 → s = ∅ :=
+induction_on_finite s
+  (by intro H; exact rfl)
+  (begin
+    intro a s' fins' anins IH H,
+    rewrite (card_insert_of_not_mem anins) at H,
+    apply nat.no_confusion H
+  end)
+
+theorem card_upto (n : ℕ) : card {i | i < n} = n :=
+by rewrite [↑card, to_finset_upto, finset.card_upto]
+
+theorem card_add_card (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
+  card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
+begin
+  rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂],
+  rewrite [-finset.to_set_union, -finset.to_set_inter, *card_to_set],
+  apply finset.card_add_card
+end
+
+theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
+  card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
+calc
+  card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel
+             ... = card s₁ + card s₂ - card (s₁ ∩ s₂)               : card_add_card s₁ s₂
+
+theorem card_union_of_disjoint {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ∩ s₂ = ∅) :
+  card (s₁ ∪ s₂) = card s₁ + card s₂ :=
+by rewrite [card_union, H, card_empty]
+
+theorem card_eq_card_add_card_diff {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
+  card s₂ = card s₁ + card (s₂ \ s₁) :=
+have H1 : s₁ ∩ (s₂ \ s₁) = ∅,
+  from eq_empty_of_forall_not_mem (take x, assume H, (and.right (and.right H)) (and.left H)),
+have s₂ = s₁ ∪ (s₂ \ s₁), from eq.symm (union_diff_cancel H),
+calc
+  card s₂ = card (s₁ ∪ (s₂ \ s₁))    : {this}
+      ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1
+
+theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
+  card s₁ ≤ card s₂ :=
+calc
+  card s₂ = card s₁ + card (s₂ \ s₁) : card_eq_card_add_card_diff H
+      ... ≥ card s₁                  : le_add_right
+
+variable {B : Type}
+
+theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [fins : finite s] (injfs : inj_on f s) :
+  card (image f s) = card s :=
+begin
+  rewrite [↑card, to_finset_image];
+  apply finset.card_image_eq_of_inj_on,
+  rewrite to_set_to_finset,
+  apply injfs
+end
+
+theorem card_le_of_inj_on (a : set A) (b : set B) [finb : finite b]
+    (Pex : ∃ f : A → B, inj_on f a ∧ (image f a ⊆ b)) :
+  card a ≤ card b :=
+by_cases
+  (assume fina : finite a,
+    obtain f H, from Pex,
+    finset.card_le_of_inj_on (to_finset a) (to_finset b)
+      (exists.intro f
+        begin
+          rewrite [finset.subset_eq_to_set_subset, finset.to_set_image, *to_set_to_finset],
+          exact H
+        end))
+  (assume nfina : ¬ finite a,
+    by rewrite [card_of_not_finite nfina]; exact !zero_le)
+
+theorem card_image_le (f : A → B) (s : set A) [fins : finite s] : card (image f s) ≤ card s :=
+by rewrite [↑card, to_finset_image]; apply finset.card_image_le
+
+theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [fins : finite s]
+  (H : card (image f s) = card s) : inj_on f s :=
+begin
+  rewrite -to_set_to_finset,
+  apply finset.inj_on_of_card_image_eq,
+  rewrite [-to_finset_to_set (finset.image _ _), finset.to_set_image, to_set_to_finset],
+  exact H
+end
+
+theorem card_pos_of_mem {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : card s > 0 :=
+have (#finset a ∈ to_finset s), by rewrite [finset.mem_eq_mem_to_set, to_set_to_finset]; apply H,
+finset.card_pos_of_mem this
+
+theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
+    (Hcard : card s₁ = card s₂) (Hsub : s₁ ⊆ s₂) :
+  s₁ = s₂ :=
+begin
+  rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂, -finset.eq_eq_to_set_eq],
+  apply finset.eq_of_card_eq_of_subset Hcard,
+  rewrite [to_finset_subset_to_finset_eq],
+  exact Hsub
+end
+
+theorem exists_two_of_card_gt_one {s : set A} (H : 1 < card s) : ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
+assert fins : finite s, from
+  by_contradiction
+    (assume nfins, by rewrite [card_of_not_finite nfins at H]; apply !not_succ_le_zero H),
+by rewrite [-to_set_to_finset s]; apply finset.exists_two_of_card_gt_one H
+
+end set

library/data/set/default.lean

@@ -3,4 +3,4 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
-import .basic .function .map .finite
+import .basic .function .map .finite .card

library/data/set/finite.lean

@@ -7,7 +7,7 @@ The notion of "finiteness" for sets. This approach is not computational: for exa
 an element  s : set A  satsifies  finite s  doesn't mean that we can compute the cardinality. For
 a computational representation, use the finset type.
 -/
-import data.set.function data.finset.card logic.choice
+import data.set.function data.finset.to_set logic.choice
 open nat
 
 variable {A : Type}
@@ -176,141 +176,4 @@ theorem induction_on_finite {P : set A → Prop} (s : set A) [fins : finite s]
   P s :=
 induction_finite H1 H2 s
 
-/- cardinality -/
-
-noncomputable definition card (s : set A) := finset.card (set.to_finset s)
-
-theorem card_to_set (s : finset A) : card (finset.to_set s) = finset.card s :=
-by rewrite [↑card, to_finset_to_set]
-
-theorem card_of_not_finite {s : set A} (nfins : ¬ finite s) : card s = 0 :=
-by rewrite [↑card, to_finset_of_not_finite nfins]
-
-theorem card_empty : card (∅ : set A) = 0 :=
-by rewrite [-finset.to_set_empty, card_to_set]
-
-theorem card_insert_of_mem {a : A} {s : set A} (H : a ∈ s) : card (insert a s) = card s :=
-if fins : finite s then
-  (by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_mem H])
-else
-  (assert ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins,
-    by rewrite [card_of_not_finite fins, card_of_not_finite this])
-
-theorem card_insert_of_not_mem {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
-  card (insert a s) = card s + 1 :=
-by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_not_mem H]
-
-theorem card_insert_le (a : A) (s : set A) [fins : finite s] :
-  card (insert a s) ≤ card s + 1 :=
-if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ
-else by rewrite [card_insert_of_not_mem H]
-
-theorem card_singleton (a : A) : card '{a} = 1 :=
-by rewrite [card_insert_of_not_mem !not_mem_empty, card_empty]
-
-/- Note: the induction tactic does not work well with the set induction principle with the
-   extra predicate "finite". -/
-theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] : card s = 0 → s = ∅ :=
-induction_on_finite s
-  (by intro H; exact rfl)
-  (begin
-    intro a s' fins' anins IH H,
-    rewrite (card_insert_of_not_mem anins) at H,
-    apply nat.no_confusion H
-  end)
-
-theorem card_upto (n : ℕ) : card {i | i < n} = n :=
-by rewrite [↑card, to_finset_upto, finset.card_upto]
-
-theorem card_add_card (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
-  card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
-begin
-  rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂],
-  rewrite [-finset.to_set_union, -finset.to_set_inter, *card_to_set],
-  apply finset.card_add_card
-end
-
-theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
-  card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
-calc
-  card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel
-             ... = card s₁ + card s₂ - card (s₁ ∩ s₂)               : card_add_card s₁ s₂
-
-theorem card_union_of_disjoint {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ∩ s₂ = ∅) :
-  card (s₁ ∪ s₂) = card s₁ + card s₂ :=
-by rewrite [card_union, H, card_empty]
-
-theorem card_eq_card_add_card_diff {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
-  card s₂ = card s₁ + card (s₂ \ s₁) :=
-have H1 : s₁ ∩ (s₂ \ s₁) = ∅,
-  from eq_empty_of_forall_not_mem (take x, assume H, (and.right (and.right H)) (and.left H)),
-have s₂ = s₁ ∪ (s₂ \ s₁), from eq.symm (union_diff_cancel H),
-calc
-  card s₂ = card (s₁ ∪ (s₂ \ s₁))    : {this}
-      ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1
-
-theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
-  card s₁ ≤ card s₂ :=
-calc
-  card s₂ = card s₁ + card (s₂ \ s₁) : card_eq_card_add_card_diff H
-      ... ≥ card s₁                  : le_add_right
-
-variable {B : Type}
-
-theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [fins : finite s] (injfs : inj_on f s) :
-  card (image f s) = card s :=
-begin
-  rewrite [↑card, to_finset_image];
-  apply finset.card_image_eq_of_inj_on,
-  rewrite to_set_to_finset,
-  apply injfs
-end
-
-theorem card_le_of_inj_on (a : set A) (b : set B) [finb : finite b]
-    (Pex : ∃ f : A → B, inj_on f a ∧ (image f a ⊆ b)) :
-  card a ≤ card b :=
-by_cases
-  (assume fina : finite a,
-    obtain f H, from Pex,
-    finset.card_le_of_inj_on (to_finset a) (to_finset b)
-      (exists.intro f
-        begin
-          rewrite [finset.subset_eq_to_set_subset, finset.to_set_image, *to_set_to_finset],
-          exact H
-        end))
-  (assume nfina : ¬ finite a,
-    by rewrite [card_of_not_finite nfina]; exact !zero_le)
-
-theorem card_image_le (f : A → B) (s : set A) [fins : finite s] : card (image f s) ≤ card s :=
-by rewrite [↑card, to_finset_image]; apply finset.card_image_le
-
-theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [fins : finite s]
-  (H : card (image f s) = card s) : inj_on f s :=
-begin
-  rewrite -to_set_to_finset,
-  apply finset.inj_on_of_card_image_eq,
-  rewrite [-to_finset_to_set (finset.image _ _), finset.to_set_image, to_set_to_finset],
-  exact H
-end
-
-theorem card_pos_of_mem {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : card s > 0 :=
-have (#finset a ∈ to_finset s), by rewrite [finset.mem_eq_mem_to_set, to_set_to_finset]; apply H,
-finset.card_pos_of_mem this
-
-theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
-    (Hcard : card s₁ = card s₂) (Hsub : s₁ ⊆ s₂) :
-  s₁ = s₂ :=
-begin
-  rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂, -finset.eq_eq_to_set_eq],
-  apply finset.eq_of_card_eq_of_subset Hcard,
-  rewrite [to_finset_subset_to_finset_eq],
-  exact Hsub
-end
-
-theorem exists_two_of_card_gt_one {s : set A} (H : 1 < card s) : ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
-assert fins : finite s, from
-  by_contradiction
-    (assume nfins, by rewrite [card_of_not_finite nfins at H]; apply !not_succ_le_zero H),
-by rewrite [-to_set_to_finset s]; apply finset.exists_two_of_card_gt_one H
-
 end set

library/data/set/set.md

@@ -8,4 +8,5 @@ Subsets of an arbitrary type.
 * [function](function.lean) : functions from one set to another
 * [map](map.lean) : set functions bundled with their domain and codomain
 * [finite](finite.lean) : the "finite" predicate on sets
+* [card](card.lean) : cardinality (for finite sets)
 * [classical_inverse](classical_inverse.lean) : inverse functions, defined classically