From f523d3a99575d1b62fbdfa351b34d97bd7716855 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 12 Apr 2015 17:33:58 -0700
Subject: [PATCH] feat(library/data): add structure for converting a list of
 elements into a type, and then show the resultant type is a finite type

---
 library/data/fintype.lean      | 64 ++++++++++++++++++++++++++++++++++
 library/data/list/as_type.lean | 20 +++++++++++
 library/data/list/basic.lean   |  3 ++
 library/data/list/default.lean |  2 +-
 library/data/list/set.lean     |  6 ++++
 5 files changed, 94 insertions(+), 1 deletion(-)
 create mode 100644 library/data/list/as_type.lean

diff --git a/library/data/fintype.lean b/library/data/fintype.lean
index 30c5244a2..a18d68186 100644
--- a/library/data/fintype.lean
+++ b/library/data/fintype.lean
@@ -12,6 +12,9 @@ open list bool unit decidable option function
 structure fintype [class] (A : Type) : Type :=
 (elems : list A) (unique : nodup elems) (complete : ∀ a, a ∈ elems)
 
+definition elements_of (A : Type) [h : fintype A] : list A :=
+@fintype.elems A h
+
 definition fintype_unit [instance] : fintype unit :=
 fintype.mk [star] dec_trivial (λ u, match u with star := dec_trivial end)
 
@@ -80,3 +83,64 @@ definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : d
     | none   := λ h : find_discr f g e = none, inl (show f = g, from funext (λ a : A, all_eq_of_find_discr_eq_none h a (c a)))
     end rfl
   end
+
+open list.as_type
+-- Auxiliary function for returning a list with all elements of the type: (list.as_type l)
+-- Remark ⟪s⟫ is notation for (list.as_type l)
+-- We use this function to define the instance for (fintype ⟪s⟫)
+private definition ltype_elems {A : Type} {s : list A} : Π {l : list A}, l ⊆ s → list ⟪s⟫
+| []     h := []
+| (a::l) h := lval a (h a !mem_cons) :: ltype_elems (sub_of_cons_sub h)
+
+private theorem mem_of_mem_ltype_elems {A : Type} {a : A} {s : list A}
+                : Π {l : list A} {h : l ⊆ s} {m : a ∈ s}, mk a m ∈ ltype_elems h → a ∈ l
+| []     h m lin := absurd lin !not_mem_nil
+| (b::l) h m lin := or.elim (eq_or_mem_of_mem_cons lin)
+  (λ leq : mk a m = mk b (h b (mem_cons b l)),
+     as_type.no_confusion leq (λ aeqb em, by rewrite [aeqb]; exact !mem_cons))
+  (λ linl : mk a m ∈ ltype_elems (sub_of_cons_sub h),
+     have ainl : a ∈ l, from mem_of_mem_ltype_elems linl,
+     mem_cons_of_mem _ ainl)
+
+private theorem nodup_ltype_elems {A : Type} {s : list A} : Π {l : list A} (d : nodup l) (h : l ⊆ s), nodup (ltype_elems h)
+| []     d h := nodup_nil
+| (a::l) d h :=
+  have d₁    : nodup l, from nodup_of_nodup_cons d,
+  have nainl : a ∉ l, from not_mem_of_nodup_cons d,
+  let  h₁    : l ⊆ s := sub_of_cons_sub h in
+  have d₂    : nodup (ltype_elems h₁), from nodup_ltype_elems d₁ h₁,
+  have nin   : mk a (h a (mem_cons a l)) ∉ ltype_elems h₁, from
+    assume ab, absurd (mem_of_mem_ltype_elems ab) nainl,
+  nodup_cons nin d₂
+
+private theorem mem_ltype_elems {A : Type} {s : list A} {a : ⟪s⟫}
+                : Π {l : list A} (h : l ⊆ s), value a ∈ l → a ∈ ltype_elems h
+| []     h vainl  := absurd vainl !not_mem_nil
+| (b::l) h vainbl := or.elim (eq_or_mem_of_mem_cons vainbl)
+  (λ vaeqb : value a = b,
+   begin
+     clear vainbl, reverts [vaeqb, h],
+     apply (as_type.cases_on a),
+     intros [va, ma, vaeqb], esimp at vaeqb,
+     apply (eq.rec_on vaeqb), intro h,
+     change (mk va ma ∈ mk va (h !mem_cons) :: ltype_elems (sub_of_cons_sub h)),
+     apply mem_cons
+   end)
+  (λ vainl : value a ∈ l,
+     assert s₁  : l ⊆ s, from sub_of_cons_sub h,
+     have   aux : a ∈ ltype_elems (sub_of_cons_sub h), from mem_ltype_elems s₁ vainl,
+     mem_cons_of_mem _ aux)
+
+definition fintype_list_as_type [instance] {A : Type} [h : decidable_eq A] {s : list A} : fintype ⟪s⟫ :=
+let  nds     : list A := erase_dup s in
+assert sub₁  : nds ⊆ s, from erase_dup_sub s,
+assert sub₂  : s ⊆ nds, from sub_erase_dup s,
+assert dnds  : nodup nds, from nodup_erase_dup s,
+let  e       : list ⟪s⟫ := ltype_elems sub₁ in
+fintype.mk
+  e
+  (nodup_ltype_elems dnds sub₁)
+  (λ a : ⟪s⟫, show a ∈ e, from
+   assert vains   : value a ∈ s,   from is_member a,
+   assert vainnds : value a ∈ nds, from sub₂ vains,
+   mem_ltype_elems sub₁ vainnds)
diff --git a/library/data/list/as_type.lean b/library/data/list/as_type.lean
new file mode 100644
index 000000000..83ec2cc58
--- /dev/null
+++ b/library/data/list/as_type.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2015 Leonardo de Moura. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.list.as_type
+Authors: Leonardo de Moura
+-/
+import data.list.basic
+
+namespace list
+structure as_type {A : Type} (l : list A) : Type :=
+(value : A) (is_member : value ∈ l)
+
+namespace as_type
+notation `⟪`:max l `⟫`:0 := as_type l
+
+definition lval {A : Type} (a : A) {l : list A} (m : a ∈ l) : ⟪l⟫ :=
+mk a m
+end as_type
+end list
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index d1e1fbb03..225645343 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -301,6 +301,9 @@ theorem sub.trans {l₁ l₂ l₃ : list T} (H₁ : l₁ ⊆ l₂) (H₂ : l₂
 theorem sub_cons (a : T) (l : list T) : l ⊆ a::l :=
 λ b i, or.inr i
 
+theorem sub_of_cons_sub {a : T} {l₁ l₂ : list T} : a::l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
+λ s b i, s b (mem_cons_of_mem _ i)
+
 theorem cons_sub_cons  {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l₁) ⊆ (a::l₂) :=
 λ b Hin, or.elim (eq_or_mem_of_mem_cons Hin)
   (λ e : b = a,  or.inl e)
diff --git a/library/data/list/default.lean b/library/data/list/default.lean
index b2ae900fd..762151a70 100644
--- a/library/data/list/default.lean
+++ b/library/data/list/default.lean
@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 import data.list.basic data.list.comb data.list.set data.list.perm
-import data.list.bigop
+import data.list.bigop data.list.as_type
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index 1d0ec6009..d3177ef1e 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -361,6 +361,12 @@ theorem mem_of_mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ erase
       (λ aeqb  : a = b, by rewrite aeqb; exact !mem_cons)
       (λ ainel : a ∈ erase_dup l, or.inr (mem_of_mem_erase_dup ainel)))
 
+theorem erase_dup_sub [H : decidable_eq A] (l : list A) : erase_dup l ⊆ l :=
+λ a i, mem_of_mem_erase_dup i
+
+theorem sub_erase_dup [H : decidable_eq A] (l : list A) : l ⊆ erase_dup l :=
+λ a i, mem_erase_dup i
+
 theorem nodup_erase_dup [H : decidable_eq A] : ∀ l : list A, nodup (erase_dup l)
 | []        := by rewrite erase_dup_nil; exact nodup_nil
 | (a::l)    := by_cases