From 7db84c7036df51a7dfa61cb77b5f647926ea7de2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Jun 2015 10:32:24 -0700 Subject: [PATCH] refactor(library/data): replace 'fin' with Haitao's 'less_than' The commit also fixes vector to use the new definition. --- library/data/data.md | 1 - library/data/fin.lean | 143 +++++++++++++++++----------- library/data/less_than.lean | 72 -------------- library/data/vector.lean | 31 +++--- tests/lean/run/empty_eq.lean | 6 +- tests/lean/run/empty_match_bug.lean | 6 +- tests/lean/run/inversion1.lean | 5 +- tests/lean/run/local_eqns2.lean | 9 +- 8 files changed, 125 insertions(+), 148 deletions(-) delete mode 100644 library/data/less_than.lean diff --git a/library/data/data.md b/library/data/data.md index f27861c15..e8d1f9e7e 100644 --- a/library/data/data.md +++ b/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 diff --git a/library/data/fin.lean b/library/data/fin.lean index 0858447d7..2d38c5789 100644 --- a/library/data/fin.lean +++ b/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 -open nat +import data.list.basic data.finset.basic data.fintype.card +open eq.ops nat function list finset fintype -inductive fin : nat → Type := -| fz : Π n, fin (succ n) -| fs : Π {n}, fin n → fin (succ n) +structure fin (n : nat) := (val : nat) (is_lt : val < n) +attribute fin.val [coercion] + +definition less_than [reducible] := fin namespace fin - definition to_nat : Π {n}, fin n → nat - | ⌞n+1⌟ (fz n) := zero - | ⌞n+1⌟ (fs f) := succ (to_nat f) +section +open decidable +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 := - rfl +lemma dinj_lt (n : nat) : dinj (λ i, i < n) fin.mk := +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) := - rfl +lemma val_mk (n i : nat) (Plt : i < n) : fin.val (fin.mk i Plt) = i := rfl - theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n - | (n+1) (fz n) := calc - 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 upto [reducible] (n : nat) : list (fin n) := +dmap (λ i, i < n) fin.mk (list.upto n) - definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n) - | ⌞n+1⌟ (fz n) m := fz (m + n) - | ⌞n+1⌟ (fs f) m := fs (lift f m) +lemma nodup_upto (n : nat) : nodup (upto n) := +dmap_nodup_of_dinj (dinj_lt n) (list.nodup_upto n) - theorem lift_fz (n m : nat) : lift (fz n) m = fz (m + n) := - rfl +lemma mem_upto (n : nat) : ∀ (i : fin n), i ∈ upto n := +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) := - rfl +lemma upto_zero : upto 0 = [] := +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) - | (n+1) (fz n) m := rfl - | (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 +lemma map_val_upto (n : nat) : map fin.val (upto n) = list.upto n := +map_of_dmap_inv_pos (val_mk n) (@lt_of_mem_upto n) - definition of_nat : Π (p : nat) (n : nat), p < n → fin n - | 0 0 h := absurd h (not_lt_zero zero) - | 0 (n+1) h := fz n - | (p+1) 0 h := absurd h (not_lt_zero (succ p)) - | (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h)) +lemma length_upto (n : nat) : length (upto n) = n := +calc + length (upto n) = length (list.upto n) : (map_val_upto n ▸ length_map fin.val (upto n))⁻¹ + ... = n : list.length_upto n - theorem of_nat_zero_succ (n : nat) (h : 0 < n+1) : of_nat 0 (n+1) h = fz n := - rfl +definition is_fintype [instance] (n : nat) : fintype (fin n) := +fintype.mk (upto n) (nodup_upto n) (mem_upto n) - theorem of_nat_succ_succ (p n : nat) (h : p+1 < n+1) : - of_nat (p+1) (n+1) h = fs (of_nat p n (lt_of_succ_lt_succ h)) := - rfl +section pigeonhole +open fintype - theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p - | 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 _} +lemma card_fin (n : nat) : card (fin n) = n := length_upto n - theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f - | (n+1) (fz n) h := rfl - | (n+1) (fs f) h := calc - of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl - ... = fs f : {of_nat_to_nat f _} +theorem pigeonhole {n m : nat} (Pmltn : m < n) : ¬∃ f : fin n → fin m, injective f := +assume Pex, absurd Pmltn (not_lt_of_ge + (calc + n = card (fin n) : card_fin + ... ≤ 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 diff --git a/library/data/less_than.lean b/library/data/less_than.lean deleted file mode 100644 index b53c93208..000000000 --- a/library/data/less_than.lean +++ /dev/null @@ -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 diff --git a/library/data/vector.lean b/library/data/vector.lean index 252833135..85a92502b 100644 --- a/library/data/vector.lean +++ b/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 - | ⌞n+1⌟ (h :: t) (fs f) := nth t f + | ⌞0⌟ [] i := elim0 i + | ⌞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 - | (n+1) f (fs i) := + | 0 f i := elim0 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 - | (succ n) (h :: t) (fs i) := - begin - change (nth (map f t) i = f (nth t i)), - rewrite nth_map - end + | 0 v i := elim0 i + | (succ n) (a :: t) (mk 0 h) := rfl + | (succ n) (a :: t) (mk (succ i) h) := by rewrite [map_cons, *nth_succ, nth_map] definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n | map2 [] [] := [] diff --git a/tests/lean/run/empty_eq.lean b/tests/lean/run/empty_eq.lean index 818d8ec20..d805901f3 100644 --- a/tests/lean/run/empty_eq.lean +++ b/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 diff --git a/tests/lean/run/empty_match_bug.lean b/tests/lean/run/empty_match_bug.lean index 3e893c86f..ea71d45e8 100644 --- a/tests/lean/run/empty_match_bug.lean +++ b/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 := diff --git a/tests/lean/run/inversion1.lean b/tests/lean/run/inversion1.lean index fcfbc2022..db567ade0 100644 --- a/tests/lean/run/inversion1.lean +++ b/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 := diff --git a/tests/lean/run/local_eqns2.lean b/tests/lean/run/local_eqns2.lean index badd54c20..0271bae6c 100644 --- a/tests/lean/run/local_eqns2.lean +++ b/tests/lean/run/local_eqns2.lean @@ -1,5 +1,10 @@ -import data.fin -open fin nat +open 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))