From dfef4c5dafe84a74be6a6d22bb7afbe55d3944ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Apr 2015 14:55:41 -0700
Subject: [PATCH] feat(library/data): define fintype type class

---
 library/data/finset/basic.lean |  9 ++++++++-
 library/data/fintype.lean      | 31 +++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 library/data/fintype.lean

diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 9ccf49f8a4..99cde6e8e7 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 
 Finite sets
 -/
-import data.nat data.list.perm data.subtype algebra.binary
+import data.fintype data.nat data.list.perm data.subtype algebra.binary
 open nat quot list subtype binary function
 open [declarations] perm
 
@@ -104,6 +104,13 @@ notation `∅` := !empty
 theorem not_mem_empty (a : A) : a ∉ ∅ :=
 λ aine : a ∈ ∅, aine
 
+/- universe -/
+definition univ [h : fintype A] : finset A :=
+to_finset_of_nodup (@fintype.elems A h) (@fintype.unique A h)
+
+theorem mem_univ [h : fintype A] (x : A) : x ∈ univ :=
+fintype.complete x
+
 /- card -/
 definition card (s : finset A) : nat :=
 quot.lift_on s
diff --git a/library/data/fintype.lean b/library/data/fintype.lean
new file mode 100644
index 0000000000..87764de7bf
--- /dev/null
+++ b/library/data/fintype.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2015 Leonardo de Moura. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+
+Finite type (type class)
+-/
+import data.list data.bool
+open list bool unit decidable
+
+structure fintype [class] (A : Type) : Type :=
+(elems : list A) (unique : nodup elems) (complete : ∀ a, a ∈ elems)
+
+definition fintype_unit [instance] : fintype unit :=
+fintype.mk [star] dec_trivial (λ u, match u with star := dec_trivial end)
+
+definition fintype_bool [instance] : fintype bool :=
+fintype.mk [ff, tt]
+  dec_trivial
+  (λ b, match b with | tt := dec_trivial | ff := dec_trivial end)
+
+definition fintype_product [instance] {A B : Type} : fintype A → fintype B → fintype (A × B)
+| (fintype.mk e₁ u₁ c₁) (fintype.mk e₂ u₂ c₂) :=
+  fintype.mk
+    (cross_product e₁ e₂)
+    (nodup_cross_product u₁ u₂)
+    (λ p,
+      match p with
+      (a, b) := mem_cross_product (c₁ a) (c₂ b)
+      end)