refactor(library/data): replace 'fin' with Haitao's 'less_than'

The commit also fixes vector to use the new definition.

library/data/data.md

@@ -12,7 +12,6 @@ Basic types:
 * [string](string.lean) : ascii strings
 * [nat](nat/nat.md) : the natural numbers
 * [fin](fin.lean) : finite ordinals
-* [less_than](less_than.lean) : finite ordinals
 * [int](int/int.md) : the integers
 * [rat](rat/rat.md) : the rationals
 

library/data/fin.lean

@@ -1,79 +1,106 @@
 /-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
+Author: Haitao Zhang
 
-Finite ordinals.
+Finite ordinal types.
 -/
-import data.nat
+import data.list.basic data.finset.basic data.fintype.card
-open nat
+open eq.ops nat function list finset fintype
 
-inductive fin : nat → Type :=
+structure fin (n : nat) := (val : nat) (is_lt : val < n)
-| fz : Π n, fin (succ n)
+attribute fin.val [coercion]
-| fs : Π {n}, fin n → fin (succ n)
+
+definition less_than [reducible] := fin
 
 namespace fin
-  definition to_nat : Π {n}, fin n → nat
+section
-  | ⌞n+1⌟ (fz n) := zero
+open decidable
-  | ⌞n+1⌟ (fs f) := succ (to_nat f)
+protected definition has_decidable_eq [instance] (n : nat) : ∀ (i j : fin n), decidable (i = j)
+| (mk ival ilt) (mk jval jlt) :=
+      match nat.has_decidable_eq ival jval with
+      | inl veq := inl (by substvars)
+      | inr vne := inr (by intro h; injection h; contradiction)
+      end
+end
 
-  theorem to_nat_fz (n : nat) : to_nat (fz n) = zero :=
+lemma dinj_lt (n : nat) : dinj (λ i, i < n) fin.mk :=
-  rfl
+take a1 a2 Pa1 Pa2 Pmkeq, fin.no_confusion Pmkeq (λ Pe Pqe, Pe)
 
-  theorem to_nat_fs {n : nat} (f : fin n) : to_nat (fs f) = succ (to_nat f) :=
+lemma val_mk (n i : nat) (Plt : i < n) : fin.val (fin.mk i Plt) = i := rfl
-  rfl
 
-  theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n
+definition upto [reducible] (n : nat) : list (fin n) :=
-  | (n+1) (fz n) :=  calc
+dmap (λ i, i < n) fin.mk (list.upto n)
-      to_nat (fz n) = 0    : rfl
-               ...  < n+1  : succ_pos n
-  | (n+1) (fs f) := calc
-      to_nat (fs f) = (to_nat f)+1 : rfl
-               ...  < n+1          : succ_lt_succ (to_nat_lt f)
 
-  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n)
+lemma nodup_upto (n : nat) : nodup (upto n) :=
-  | ⌞n+1⌟ (fz n)  m := fz (m + n)
+dmap_nodup_of_dinj (dinj_lt n) (list.nodup_upto n)
-  | ⌞n+1⌟ (fs f)  m := fs (lift f m)
 
-  theorem lift_fz (n m : nat) : lift (fz n) m = fz (m + n) :=
+lemma mem_upto (n : nat) : ∀ (i : fin n), i ∈ upto n :=
-  rfl
+take i, fin.destruct i
+  (take ival Piltn,
+    assert Pin : ival ∈ list.upto n, from mem_upto_of_lt Piltn,
+    mem_of_dmap Piltn Pin)
 
-  theorem lift_fs {n : nat} (f : fin n) (m : nat) : lift (fs f) m = fs (lift f m) :=
+lemma upto_zero : upto 0 = [] :=
-  rfl
+by rewrite [↑upto, list.upto_nil, dmap_nil]
 
-  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
+lemma map_val_upto (n : nat) : map fin.val (upto n) = list.upto n :=
-  | (n+1) (fz n) m := rfl
+map_of_dmap_inv_pos (val_mk n) (@lt_of_mem_upto n)
-  | (n+1) (fs f) m := calc
-      to_nat (fs f) = (to_nat f) + 1           : rfl
-               ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
-               ...  = to_nat (lift (fs f) m)   : rfl
 
-  definition of_nat : Π (p : nat) (n : nat), p < n → fin n
+lemma length_upto (n : nat) : length (upto n) = n :=
-  | 0     0     h := absurd h (not_lt_zero zero)
+calc
-  | 0     (n+1) h := fz n
+  length (upto n) = length (list.upto n) : (map_val_upto n ▸ length_map fin.val (upto n))⁻¹
-  | (p+1) 0     h := absurd h (not_lt_zero (succ p))
+              ... = n                    : list.length_upto n
-  | (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
 
-  theorem of_nat_zero_succ (n : nat) (h : 0 < n+1) : of_nat 0 (n+1) h = fz n :=
+definition is_fintype [instance] (n : nat) : fintype (fin n) :=
-  rfl
+fintype.mk (upto n) (nodup_upto n) (mem_upto n)
 
-  theorem of_nat_succ_succ (p n : nat) (h : p+1 < n+1) :
+section pigeonhole
-               of_nat (p+1) (n+1) h = fs (of_nat p n (lt_of_succ_lt_succ h)) :=
+open fintype
-  rfl
 
-  theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p
+lemma card_fin (n : nat) : card (fin n) = n := length_upto n
-  | 0     0     h := absurd h (not_lt_zero 0)
-  | 0     (n+1) h := rfl
-  | (p+1) 0     h := absurd h (not_lt_zero (p+1))
-  | (p+1) (n+1) h := calc
-      to_nat (of_nat (p+1) (n+1) h)
-               = succ (to_nat (of_nat p n _)) : rfl
-           ... = succ p                       : {to_nat_of_nat p n _}
 
-  theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f
+theorem pigeonhole {n m : nat} (Pmltn : m < n) : ¬∃ f : fin n → fin m, injective f :=
-  | (n+1) (fz n) h := rfl
+assume Pex, absurd Pmltn (not_lt_of_ge
-  | (n+1) (fs f) h := calc
+  (calc
-      of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
+       n = card (fin n) : card_fin
-                                   ...  = fs f                       : {of_nat_to_nat f _}
+     ... ≤ card (fin m) : card_le_of_inj (fin n) (fin m) Pex
+     ... = m : card_fin))
 
+end pigeonhole
+
+definition zero (n : nat) : fin (succ n) :=
+mk 0 !zero_lt_succ
+
+variable {n : nat}
+
+theorem val_lt : ∀ i : fin n, val i < n
+| (mk v h) := h
+
+definition lift : fin n → Π m, fin (n + m)
+| (mk v h) m := mk v (lt_add_of_lt_right h m)
+
+theorem val_lift : ∀ (i : fin n) (m : nat), val i = val (lift i m)
+| (mk v h) m := rfl
+
+definition pred : fin n → fin n
+| (mk v h) := mk (nat.pred v) (pre_lt_of_lt h)
+
+lemma val_pred : ∀ (i : fin n), val (pred i) = nat.pred (val i)
+| (mk v h) := rfl
+
+lemma pred_zero : pred (zero n) = zero n :=
+rfl
+
+definition mk_pred (i : nat) (h : succ i < succ n) : fin n :=
+mk i (lt_of_succ_lt_succ h)
+
+definition succ : fin n → fin (succ n)
+| (mk v h) := mk (nat.succ v) (succ_lt_succ h)
+
+lemma val_succ : ∀ (i : fin n), val (succ i) = nat.succ (val i)
+| (mk v h) := rfl
+
+definition elim0 {C : Type} : fin 0 → C
+| (mk v h) := absurd h !not_lt_zero
 end fin

library/data/less_than.lean

@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2015 Haitao Zhang. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Haitao Zhang
-
-Finite ordinal types.
--/
-import data.list.basic data.finset.basic data.fintype.card
-open eq.ops nat function list finset fintype
-
-structure less_than (n : nat) := (val : nat) (is_lt : val < n)
-attribute less_than.val [coercion]
-
-namespace less_than
-
-section
-open decidable
-protected definition has_decidable_eq [instance] (n : nat) : ∀ (i j : less_than n), decidable (i = j)
-| (mk ival ilt) (mk jval jlt) :=
-      match nat.has_decidable_eq ival jval with
-      | inl veq := inl (by substvars)
-      | inr vne := inr (by intro h; injection h; contradiction)
-      end
-end
-
-lemma dinj_lt (n : nat) : dinj (λ i, i < n) less_than.mk :=
-take a1 a2 Pa1 Pa2 Pmkeq, less_than.no_confusion Pmkeq (λ Pe Pqe, Pe)
-
-lemma val_mk (n i : nat) (Plt : i < n) : less_than.val (less_than.mk i Plt) = i := rfl
-
-definition upto [reducible] (n : nat) : list (less_than n) :=
-dmap (λ i, i < n) less_than.mk (list.upto n)
-
-lemma nodup_upto (n : nat) : nodup (upto n) :=
-dmap_nodup_of_dinj (dinj_lt n) (list.nodup_upto n)
-
-lemma mem_upto (n : nat) : ∀ (i : less_than n), i ∈ upto n :=
-take i, less_than.destruct i
-  (take ival Piltn,
-    assert Pin : ival ∈ list.upto n, from mem_upto_of_lt Piltn,
-    mem_of_dmap Piltn Pin)
-
-lemma upto_zero : upto 0 = [] :=
-by rewrite [↑upto, list.upto_nil, dmap_nil]
-
-lemma map_val_upto (n : nat) : map less_than.val (upto n) = list.upto n :=
-map_of_dmap_inv_pos (val_mk n) (@lt_of_mem_upto n)
-
-lemma length_upto (n : nat) : length (upto n) = n :=
-calc
-  length (upto n) = length (list.upto n) : (map_val_upto n ▸ length_map less_than.val (upto n))⁻¹
-              ... = n                    : list.length_upto n
-
-definition fintype_less_than [instance] (n : nat) : fintype (less_than n) :=
-fintype.mk (upto n) (nodup_upto n) (mem_upto n)
-
-section pigeonhole
-open fintype
-
-lemma card_less_than (n : nat) : card (less_than n) = n := length_upto n
-
-theorem pigeonhole {n m : nat} (Pmltn : m < n) : ¬ (∃ f : less_than n → less_than m, injective f) :=
-not.intro
-  (assume Pex, absurd Pmltn (not_lt_of_ge
-    (calc
-        n = card (less_than n) : card_less_than
-      ... ≤ card (less_than m) : card_le_of_inj (less_than n) (less_than m) Pex
-      ... = m : card_less_than)))
-
-end pigeonhole
-
-end less_than

library/data/vector.lean

@@ -60,18 +60,28 @@ namespace vector
   | (n+1) a := last_const n a
 
   definition nth : Π {n : nat}, vector A n → fin n → A
-  | ⌞n+1⌟ (h :: t) (fz n) := h
+  | ⌞0⌟   []       i               := elim0 i
-  | ⌞n+1⌟ (h :: t) (fs f) := nth t f
+  | ⌞n+1⌟ (a :: v) (mk 0 _)        := a
+  | ⌞n+1⌟ (a :: v) (mk (succ i) h) := nth v (mk_pred i h)
+
+  lemma nth_zero {n : nat} (a : A) (v : vector A n) (h : 0 < succ n) : nth (a::v) (mk 0 h) = a :=
+  rfl
+
+  lemma nth_succ {n : nat} (a : A) (v : vector A n) (i : nat) (h : succ i < succ n)
+                 : nth (a::v) (mk (succ i) h) = nth v (mk_pred i h) :=
+  rfl
 
   definition tabulate : Π {n : nat}, (fin n → A) → vector A n
   | 0      f :=  []
-  | (n+1)  f :=  f (fz n) :: tabulate (λ i : fin n, f (fs i))
+  | (n+1)  f :=  f (@zero n) :: tabulate (λ i : fin n, f (succ i))
 
   theorem nth_tabulate : ∀ {n : nat} (f : fin n → A) (i : fin n), nth (tabulate f) i = f i
-  | (n+1) f (fz n) := rfl
+  | 0     f i               := elim0 i
-  | (n+1) f (fs i) :=
+  | (n+1) f (mk 0 h)        := rfl
+  | (n+1) f (mk (succ i) h) :=
     begin
-      change (nth (tabulate (λ i : fin n, f (fs i))) i = f (fs i)),
+      change nth (f (@zero n) :: tabulate (λ i : fin n, f (succ i))) (mk (succ i) h) = f (mk (succ i) h),
+      rewrite nth_succ,
       rewrite nth_tabulate
     end
 
@@ -86,12 +96,9 @@ namespace vector
   rfl
 
   theorem nth_map (f : A → B) : ∀ {n : nat} (v : vector A n) (i : fin n), nth (map f v) i = f (nth v i)
-  | (succ n) (h :: t) (fz n) := rfl
+  | 0        v        i               := elim0 i
-  | (succ n) (h :: t) (fs i) :=
+  | (succ n) (a :: t) (mk 0 h)        := rfl
-    begin
+  | (succ n) (a :: t) (mk (succ i) h) := by rewrite [map_cons, *nth_succ, nth_map]
-      change (nth (map f t) i = f (nth t i)),
-      rewrite nth_map
-    end
 
   definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
   | map2 []      []      := []

tests/lean/run/empty_eq.lean

@@ -1,5 +1,9 @@
-import data.fin
 open nat
+
+inductive fin : nat → Type :=
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
+
 open fin
 
 definition case0 {C : fin zero → Type} : Π (f : fin zero), C f

tests/lean/run/empty_match_bug.lean

@@ -1,5 +1,9 @@
-import data.fin
 open nat
+
+inductive fin : nat → Type :=
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
+
 open fin
 
 definition case0 {C : fin zero → Type} (f : fin zero) : C f :=

tests/lean/run/inversion1.lean

@@ -1,6 +1,9 @@
-import data.fin
 open nat
 
+inductive fin : nat → Type :=
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
+
 namespace fin
 
   definition z_cases_on2 (C : fin zero → Type) (p : fin zero) : C p :=

tests/lean/run/local_eqns2.lean

@@ -1,5 +1,10 @@
-import data.fin
+open nat
-open fin nat
+
+inductive fin : nat → Type :=
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
+
+open fin
 
 definition nz_cases_on {C  : Π n, fin (succ n) → Type}
                        (H₁ : Π n, C n (fz n))