From e8affed020431e308a4ae70bb92d2b65b5eaf191 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 May 2015 18:18:29 -0700 Subject: [PATCH] refactor(library): test new tactics in the standard library --- library/data/encodable.lean | 2 +- library/data/fintype.lean | 3 +-- library/data/int/basic.lean | 4 ++-- library/data/list/basic.lean | 2 +- library/data/option.lean | 2 +- library/data/sum.lean | 4 ++-- library/init/nat.lean | 17 ++++++++--------- 7 files changed, 16 insertions(+), 18 deletions(-) diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 7129a392b..882cb360d 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -21,7 +21,7 @@ assume e : encodable A, have inj_encode : injective encode, from λ (a₁ a₂ : A) (h : encode a₁ = encode a₂), assert aux : decode A (encode a₁) = decode A (encode a₂), by rewrite h, - by rewrite [*encodek at aux]; exact (option.no_confusion aux (λ e, e)), + by rewrite [*encodek at aux]; injection aux; assumption, exists.intro encode inj_encode definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A := diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 4cee0a434..3b6fbe76e 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -70,8 +70,7 @@ theorem all_eq_of_find_discr_eq_none {f g : A → B} : ∀ {l}, find_discr f g l (λ aeqx : a = x, by rewrite [-aeqx at fx_eq_gx]; exact fx_eq_gx) (λ ainl : a ∈ l, all_eq_of_find_discr_eq_none aux a ainl)) (λ fx_ne_gx : f x ≠ g x, - have aux : some x = none, by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; exact e, - option.no_confusion aux) + by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; contradiction) end find_discr definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : decidable_eq B] : decidable_eq (A → B) := diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 6a4912616..34fbcf995 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -94,10 +94,10 @@ infix * := int.mul /- some basic functions and properties -/ theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n := -int.no_confusion H (λe, e) +by injection H; assumption theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := -int.no_confusion H (λe, e) +by injection H; assumption theorem neg_succ_of_nat_eq (n : ℕ) : -[n +1] = -(n + 1) := rfl diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 7b1f4a017..3350ca6ad 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -65,7 +65,7 @@ theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length theorem eq_nil_of_length_eq_zero : ∀ {l : list T}, length l = 0 → l = [] | [] H := rfl -| (a::s) H := nat.no_confusion H +| (a::s) H := by contradiction -- add_rewrite length_nil length_cons diff --git a/library/data/option.lean b/library/data/option.lean index 6b87915df..97572e2a7 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -23,7 +23,7 @@ namespace option by contradiction theorem some.inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ := - option.no_confusion H (λe, e) + by injection H; assumption protected definition is_inhabited [instance] (A : Type) : inhabited (option A) := inhabited.mk none diff --git a/library/data/sum.lean b/library/data/sum.lean index db844dbf1..38c018799 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -28,10 +28,10 @@ namespace sum by contradiction definition inl_inj {a₁ a₂ : A} : intro_left B a₁ = intro_left B a₂ → a₁ = a₂ := - assume H, sum.no_confusion H (λe, e) + assume H, by injection H; assumption definition inr_inj {b₁ b₂ : B} : intro_right A b₁ = intro_right A b₂ → b₁ = b₂ := - assume H, sum.no_confusion H (λe, e) + assume H, by injection H; assumption protected definition is_inhabited_left [instance] [h : inhabited A] : inhabited (A + B) := inhabited.mk (inl (default A)) diff --git a/library/init/nat.lean b/library/init/nat.lean index a44e1c566..7ace6b2a7 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -34,9 +34,10 @@ namespace nat | has_decidable_eq (succ x) zero := inr (by contradiction) | has_decidable_eq zero (succ y) := inr (by contradiction) | has_decidable_eq (succ x) (succ y) := - if H : x = y - then inl (eq.rec_on H rfl) - else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H)) + match has_decidable_eq x y with + | inl xeqy := inl (by rewrite xeqy) + | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney) + end -- less-than is well-founded definition lt.wf [instance] : well_founded lt := @@ -51,12 +52,10 @@ namespace nat acc.intro (succ n) (λ (m : nat) (hlt : m < succ n), have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from λ n₁ hlt, nat.lt.cases_on hlt - (λ (heq : succ n = succ m), - nat.no_confusion heq (λ (e : n = m), - eq.rec_on e ih)) - (λ b (hlt : m < b) (heq : succ n = succ b), - nat.no_confusion heq (λ (e : n = b), - acc.inv (eq.rec_on e ih) hlt)), + (λ (sn_eq_sm : succ n = succ m), + by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih) + (λ b (hlt : m < b) (sn_eq_sb : succ n = succ b), + by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt), aux hlt rfl))) definition measure {A : Type} (f : A → nat) : A → A → Prop :=