feat(library/data/fintype,finset): add cardinality for finite types from Haitao Zhang

library/data/data.md

@@ -33,5 +33,5 @@ Constructors:
 
 Types with extra information:
 
-* [fintype](fintype.lean) : finite types
+* [fintype](fintype/fintype.md) : finite types
 * [encodable](encodable.lean) : types with a coding to nat

library/data/finset/basic.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura, Jeremy Avigad
 
 Finite sets.
 -/
-import data.fintype data.nat data.list.perm data.subtype algebra.binary
+import data.fintype.basic data.nat data.list.perm data.subtype algebra.binary
 open nat quot list subtype binary function
 open [declarations] perm
 

library/data/finset/card.lean

@@ -61,7 +61,8 @@ section card_image
 open set
 include deceqB
 
-theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} (H1 : inj_on f (ts s)) : card (image f s) = card s :=
+theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} (H1 : inj_on f (ts s)) :
+  card (image f s) = card s :=
 begin
   induction s with a t H IH,
     { rewrite [card_empty] },
@@ -81,6 +82,15 @@ begin
                                 ... = card (insert a t)               : card_insert_of_not_mem H
     }
 end
+
+lemma card_le_of_inj_on (a : finset A) (b : finset B)
+    (Pex : ∃ f : A → B, set.inj_on f (ts a) ∧ (image f a ⊆ b)):
+  card a ≤ card b :=
+obtain f Pinj, from Pex,
+assert Psub : _, from and.right Pinj,
+assert Ple : card (image f a) ≤ card b, from card_le_card_of_subset Psub,
+by rewrite [(card_image_eq_of_inj_on (and.left Pinj))⁻¹]; exact Ple
+
 end card_image
 
 theorem Sum_const_eq_card_mul (s : finset A) (n : nat) : (∑ x ∈ s, n) = card s * n :=

library/data/fintype/card.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Haitao Zhang
+
+Cardinality for finite types.
+-/
+import .basic data.list data.finset.card
+open eq.ops nat function list finset
+
+namespace fintype
+
+definition card [reducible] (A : Type) [finA : fintype A] := finset.card (@finset.univ A _)
+
+lemma card_eq_card_image_of_inj
+      {A : Type} [finA : fintype A] [deceqA : decidable_eq A]
+      {B : Type} [finB : fintype B] [deceqB : decidable_eq B]
+      {f : A → B} :
+  injective f → finset.card (image f univ) = card A :=
+assume Pinj,
+card_image_eq_of_inj_on (to_set_univ⁻¹ ▸ (iff.mp !set.injective_iff_inj_on_univ Pinj))
+
+-- General version of the pigeonhole principle. See also data.less_than.
+lemma card_le_of_inj (A : Type) [finA : fintype A] [deceqA : decidable_eq A]
+                     (B : Type) [finB : fintype B] [deceqB : decidable_eq B] :
+   (∃ f : A → B, injective f) → card A ≤ card B :=
+assume Pex, obtain f Pinj, from Pex,
+assert Pinj_on_univ : _, from iff.mp !set.injective_iff_inj_on_univ Pinj,
+assert Pinj_ts : _, from to_set_univ⁻¹ ▸ Pinj_on_univ,
+assert Psub : (image f univ) ⊆ univ, from !subset_univ,
+finset.card_le_of_inj_on univ univ (exists.intro f (and.intro Pinj_ts Psub))
+
+-- used to prove that inj ∧ eq card => surj
+lemma univ_of_card_eq_univ {A : Type} [finA : fintype A] [deceqA : decidable_eq A] {s : finset A} :
+  finset.card s = card A → s = univ :=
+assume Pcardeq, ext (take a,
+assert D : decidable (a ∈ s), from decidable_mem a s, begin
+apply iff.intro,
+  intro ain, apply mem_univ,
+  intro ain, cases D with Pin Pnin,
+    exact Pin,
+    assert Pplus1 : finset.card (insert a s) = finset.card s + 1,
+      exact card_insert_of_not_mem Pnin,
+    rewrite Pcardeq at Pplus1,
+    assert Ple : finset.card (insert a s) ≤ card A,
+      apply card_le_card_of_subset, apply subset_univ,
+    rewrite Pplus1 at Ple,
+    exact false.elim (not_succ_le_self Ple)
+end)
+
+end fintype

library/data/fintype/default.lean

@@ -5,4 +5,4 @@ Authors: Leonardo de Moura
 
 Finite type (type class).
 -/
-import data.fintype.basic data.fintype.function
+import .basic .function .card

library/data/fintype/fintype.md

@@ -0,0 +1,8 @@
+data.fintype
+============
+
+Finite types.
+
+* [basic](basic.lean) 
+* [function](function.lean)
+* [card](card.lean)