From 559dd586f28135f388f63f8390d06348cd7e10d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Sep 2014 22:22:04 -0700 Subject: [PATCH] feat(library): add 'decidable_eq' class Signed-off-by: Leonardo de Moura --- library/data/bool.lean | 9 +++--- library/data/int/basic.lean | 4 +-- library/data/list/basic.lean | 10 +++---- library/data/nat/basic.lean | 5 ++-- library/data/option.lean | 18 ++++++------ library/data/prod.lean | 6 ++-- library/data/subtype.lean | 10 +++---- library/data/sum.lean | 42 +++++++++++++++------------ library/data/unit.lean | 4 +-- library/logic/classes/decidable.lean | 8 +++++ tests/lean/run/occurs_check_bug1.lean | 2 +- 11 files changed, 67 insertions(+), 51 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index bd8e48ac0..edd147d32 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -138,8 +138,9 @@ namespace bool theorem is_inhabited [protected] [instance] : inhabited bool := inhabited.mk ff - theorem has_decidable_eq [protected] [instance] (a b : bool) : decidable (a = b) := - rec_on a - (rec_on b (inl rfl) (inr ff_ne_tt)) - (rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl)) + theorem has_decidable_eq [protected] [instance] : decidable_eq bool := + decidable_eq.intro (λ (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))) end bool diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 7e10f7a1e..d1d318627 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -205,8 +205,8 @@ exists_intro (pr1 (rep a)) definition of_nat (n : ℕ) : ℤ := psub (pair n 0) -theorem int_eq_decidable [instance] (a b : ℤ) : decidable (a = b) := _ --- subtype_eq_decidable _ _ (prod_eq_decidable _ _ _ _) +theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ := +decidable_eq.intro (λ (a b : ℤ), _) opaque_hint (hiding int) coercion of_nat diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 6971c35a3..1fde8a5e9 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -236,7 +236,7 @@ induction_on l from H3 ▸ rfl, exists_intro _ (exists_intro _ H4))) -theorem mem_is_decidable [instance] {H : Π (x y : T), decidable (x = y)} {x : T} {l : list T} : decidable (mem x l) := +theorem mem_is_decidable [instance] {H : decidable_eq T} {x : T} {l : list T} : decidable (mem x l) := rec_on l (decidable.inr (iff.false_elim (@mem_nil x))) (λ (h : T) (l : list T) (iH : decidable (mem x l)), @@ -264,15 +264,15 @@ rec_on l -- Find -- ---- -definition find (x : T) {H : Π (x y : T), decidable (x = y)} : list T → nat := +definition find {H : decidable_eq T} (x : T) : list T → nat := rec 0 (fun y l b, if x = y then 0 else succ b) -theorem find_nil {f : T} {H : Π (x y : T), decidable (x = y)} : find f nil = 0 +theorem find_nil {H : decidable_eq T} {f : T} : find f nil = 0 -theorem find_cons {x y : T} {l : list T} {H : Π (x y : T), decidable (x = y)} : +theorem find_cons {H : decidable_eq T} {x y : T} {l : list T} : find x (cons y l) = if x = y then 0 else succ (find x l) -theorem not_mem_find {l : list T} {x : T} {H : Π (x y : T), decidable (x = y)} : +theorem not_mem_find {H : decidable_eq T} {l : list T} {x : T} : ¬mem x l → find x l = length l := rec_on l (assume P₁ : ¬mem x nil, rfl) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index d0b1023bf..cad93965c 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -105,7 +105,8 @@ induction_on n absurd H ne) (take k IH H, IH (succ_inj H)) -theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) := +theorem has_decidable_eq [instance] [protected] : decidable_eq ℕ := +decidable_eq.intro (λ (n m : ℕ), have general : ∀n, decidable (n = m), from rec_on m (take n, @@ -123,7 +124,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 e72674634..f7d5cff84 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -38,13 +38,13 @@ namespace option theorem is_inhabited [protected] [instance] (A : Type) : inhabited (option A) := inhabited.mk none - theorem has_decidable_eq [protected] [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} - (o₁ o₂ : option A) : decidable (o₁ = o₂) := - 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)))) + theorem has_decidable_eq [protected] [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) := + decidable_eq.intro (λ (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))))) end option diff --git a/library/data/prod.lean b/library/data/prod.lean index 0f96ac333..f0c7706ab 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -48,12 +48,12 @@ section theorem is_inhabited [protected] [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) := inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b))) - theorem has_decidable_eq [protected] [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v)) - (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) := + 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), 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 6dcd20f39..098e23498 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -41,10 +41,10 @@ section theorem is_inhabited [protected] [instance] {a : A} (H : P a) : inhabited {x, P x} := inhabited.mk (tag a H) - theorem has_decidable_eq [protected] [instance] (a1 a2 : {x, P x}) - (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) := - 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) + theorem has_decidable_eq [protected] [instance] (H : decidable_eq A) : decidable_eq {x, P x} := + decidable_eq.intro (λ (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)) end end subtype diff --git a/library/data/sum.lean b/library/data/sum.lean index cbba4744a..6b87c7335 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -55,22 +55,28 @@ namespace sum theorem is_inhabited_right [protected] [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) := inhabited.mk (inr A (default B)) - theorem has_eq_decidable [protected] [instance] {A B : Type} (s1 s2 : A ⊎ B) - (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) - (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := - rec_on s1 - (take a1, show decidable (inl B a1 = s2), from - rec_on s2 - (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) - (take b2, - have H3 : (inl B a1 = inr A b2) ↔ false, - from iff.intro inl_neq_inr (assume H4, false_elim H4), - show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3))) - (take b1, show decidable (inr A b1 = s2), from - rec_on s2 - (take a2, - have H3 : (inr A b1 = inl B a2) ↔ false, - from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4), - show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3)) - (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) + 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), + rec_on s1 + (take a1, show decidable (inl B a1 = s2), from + rec_on s2 + (take a2, show decidable (inl B a1 = inl B a2), from + decidable.rec_on (H1 a1 a2) + (assume Heq : a1 = a2, decidable.inl (Heq ▸ rfl)) + (assume Hne : a1 ≠ a2, decidable.inr (mt inl_inj Hne))) + (take b2, + have H3 : (inl B a1 = inr A b2) ↔ false, + from iff.intro inl_neq_inr (assume H4, false_elim H4), + show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3))) + (take b1, show decidable (inr A b1 = s2), from + rec_on s2 + (take a2, + have H3 : (inr A b1 = inl B a2) ↔ false, + from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4), + show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3)) + (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))))) end sum diff --git a/library/data/unit.lean b/library/data/unit.lean index d629c79de..7f2a63810 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -18,6 +18,6 @@ namespace unit theorem is_inhabited [protected] [instance] : inhabited unit := inhabited.mk ⋆ - theorem has_decidable_eq [protected] [instance] (a b : unit) : decidable (a = b) := - inl (equal a b) + theorem has_decidable_eq [protected] [instance] : decidable_eq unit := + decidable_eq.intro (λ (a b : unit), inl (equal a b)) end unit diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean index 766891e16..4f138a420 100644 --- a/library/logic/classes/decidable.lean +++ b/library/logic/classes/decidable.lean @@ -95,3 +95,11 @@ theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidab 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 decidable_eq_to_decidable [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) := +decidable_eq.rec (λ H, H) H x y + +coercion decidable_eq_to_decidable : decidable_eq diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index 1be746bd8..a2b63bba6 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -10,7 +10,7 @@ variable gcd_aux : ℕ × ℕ → ℕ definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y) -theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (decidable_eq (pr2 (pair x y)) 0) nat x (gcd y (x mod y)) := +theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 (pair x y)) 0) nat x (gcd y (x mod y)) := sorry theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=