From 9b9adf88319fd0265ab926e34a429fa81885c3c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Sep 2014 16:07:07 -0700 Subject: [PATCH] refactor(library): replace decidable_eq with abbreviation --- library/data/bool.lean | 4 ++-- library/data/int/basic.lean | 2 +- library/data/nat/basic.lean | 4 ++-- library/data/option.lean | 4 ++-- library/data/prod.lean | 4 ++-- library/data/subtype.lean | 4 ++-- library/data/sum.lean | 4 ++-- library/data/unit.lean | 2 +- library/logic/classes/decidable.lean | 6 +----- tests/lean/interactive/coe.input | 2 +- tests/lean/interactive/coe.input.expected.out | 6 +++--- tests/lean/interactive/coe.lean | 2 +- tests/lean/run/whnfinst.lean | 3 ++- 13 files changed, 22 insertions(+), 25 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index edd147d32..f149f7999 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -139,8 +139,8 @@ namespace bool inhabited.mk ff theorem has_decidable_eq [protected] [instance] : decidable_eq bool := - decidable_eq.intro (λ (a b : bool), + take a b : bool, rec_on a (rec_on b (inl rfl) (inr ff_ne_tt)) - (rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl))) + (rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl)) end bool diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 4dd940352..83e43b034 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -206,7 +206,7 @@ exists_intro (pr1 (rep a)) definition of_nat (n : ℕ) : ℤ := psub (pair n 0) theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ := -decidable_eq.intro (λ (a b : ℤ), _) +take a b : ℤ, _ opaque_hint (hiding int) coercion of_nat diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 60c19c5df..b7eb85a6b 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -106,7 +106,7 @@ induction_on n (take k IH H, IH (succ_inj H)) theorem has_decidable_eq [instance] [protected] : decidable_eq ℕ := -decidable_eq.intro (λ (n m : ℕ), +take n m : ℕ, have general : ∀n, decidable (n = m), from rec_on m (take n, @@ -123,7 +123,7 @@ have general : ∀n, decidable (n = m), from have H1 : succ n' ≠ succ m', from assume Heq, absurd (succ_inj Heq) Hne, inr H1))), -general n) +general n theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := diff --git a/library/data/option.lean b/library/data/option.lean index f7d5cff84..d8fe0ebf8 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -39,12 +39,12 @@ namespace option inhabited.mk none theorem has_decidable_eq [protected] [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) := - decidable_eq.intro (λ (o₁ o₂ : option A), + take o₁ o₂ : option A, rec_on o₁ (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂)))) (take a₁ : A, rec_on o₂ (inr (ne.symm (none_ne_some a₁))) (take a₂ : A, decidable.rec_on (H a₁ a₂) (assume Heq : a₁ = a₂, inl (Heq ▸ rfl)) - (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (equal Hn) Hne))))) + (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (equal Hn) Hne)))) end option diff --git a/library/data/prod.lean b/library/data/prod.lean index f0c7706ab..a20117f89 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -49,11 +49,11 @@ section inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b))) theorem has_decidable_eq [protected] [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) := - decidable_eq.intro (λ (u v : A × B), + take u v : A × B, have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from iff.intro (assume H, H ▸ and.intro rfl rfl) (assume H, and.elim H (assume H4 H5, equal H4 H5)), - decidable_iff_equiv _ (iff.symm H3)) + decidable_iff_equiv _ (iff.symm H3) end end prod diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 098e23498..f7a9e250f 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -42,9 +42,9 @@ section inhabited.mk (tag a H) theorem has_decidable_eq [protected] [instance] (H : decidable_eq A) : decidable_eq {x, P x} := - decidable_eq.intro (λ (a1 a2 : {x, P x}), + take a1 a2 : {x, P x}, have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from iff.intro (assume H, eq.subst H rfl) (assume H, equal H), - decidable_iff_equiv _ (iff.symm H1)) + decidable_iff_equiv _ (iff.symm H1) end end subtype diff --git a/library/data/sum.lean b/library/data/sum.lean index 6b87c7335..09a59cc74 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -57,7 +57,7 @@ namespace sum theorem has_eq_decidable [protected] [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A ⊎ B) := - decidable_eq.intro (λ (s1 s2 : A ⊎ B), + take s1 s2 : A ⊎ B, rec_on s1 (take a1, show decidable (inl B a1 = s2), from rec_on s2 @@ -78,5 +78,5 @@ namespace sum (take b2, show decidable (inr A b1 = inr A b2), from decidable.rec_on (H2 b1 b2) (assume Heq : b1 = b2, decidable.inl (Heq ▸ rfl)) - (assume Hne : b1 ≠ b2, decidable.inr (mt inr_inj Hne))))) + (assume Hne : b1 ≠ b2, decidable.inr (mt inr_inj Hne)))) end sum diff --git a/library/data/unit.lean b/library/data/unit.lean index 7f2a63810..ef127c481 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -19,5 +19,5 @@ namespace unit inhabited.mk ⋆ theorem has_decidable_eq [protected] [instance] : decidable_eq unit := - decidable_eq.intro (λ (a b : unit), inl (equal a b)) + take (a b : unit), inl (equal a b) end unit diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean index 43052ef58..85d7ff617 100644 --- a/library/logic/classes/decidable.lean +++ b/library/logic/classes/decidable.lean @@ -96,8 +96,4 @@ decidable_iff_equiv Ha (eq_to_iff H) end decidable -inductive decidable_eq [class] (A : Type) : Type := -intro : (Π x y : A, decidable (x = y)) → decidable_eq A - -theorem of_decidable_eq [instance] [coercion] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) := -decidable_eq.rec (λ H, H) H x y +abbreviation decidable_eq (A : Type) := Π (a b : A), decidable (a = b) diff --git a/tests/lean/interactive/coe.input b/tests/lean/interactive/coe.input index a48b96988..5c16f475a 100644 --- a/tests/lean/interactive/coe.input +++ b/tests/lean/interactive/coe.input @@ -1,3 +1,3 @@ VISIT coe.lean WAIT -INFO 5 33 \ No newline at end of file +INFO 5 16 \ No newline at end of file diff --git a/tests/lean/interactive/coe.input.expected.out b/tests/lean/interactive/coe.input.expected.out index 05dc75685..90c3026cc 100644 --- a/tests/lean/interactive/coe.input.expected.out +++ b/tests/lean/interactive/coe.input.expected.out @@ -1,13 +1,13 @@ -- BEGINWAIT -- ENDWAIT -- BEGININFO --- TYPE|5|33 +-- TYPE|5|16 decidable (eq a b) -- ACK --- SYNTH|5|33 +-- SYNTH|5|16 int.has_decidable_eq a b -- ACK --- SYMBOL|5|33 +-- SYMBOL|5|16 _ -- ACK -- ENDINFO diff --git a/tests/lean/interactive/coe.lean b/tests/lean/interactive/coe.lean index 6133271a9..b7fe820ef 100644 --- a/tests/lean/interactive/coe.lean +++ b/tests/lean/interactive/coe.lean @@ -2,7 +2,7 @@ import data.int open int theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ := -decidable_eq.intro (λ (a b : ℤ), _) +take (a b : ℤ), _ variable n : nat variable i : int diff --git a/tests/lean/run/whnfinst.lean b/tests/lean/run/whnfinst.lean index 3c5949f92..f79626431 100644 --- a/tests/lean/run/whnfinst.lean +++ b/tests/lean/run/whnfinst.lean @@ -9,5 +9,6 @@ section theorem tst1 (H : Πx y, decidable (R x y)) (a b c : A) : decidable (R a b ∧ R b a) - theorem tst2 (H : decidable_bin_rel R) (a b c : A) : decidable (R a b ∧ R b a) + theorem tst2 (H : decidable_bin_rel R) (a b c : A) : decidable (R a b ∧ R b a ∨ R b b) := + _ end