From 3ca1264f612036c9f2db4a7bf45eac34354c2da2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 30 Sep 2014 09:02:37 -0700
Subject: [PATCH] refactor(library): mark 'decidable' theorems as definitions

If we don't do that, then any 'if' term that uses one of these theorems
will get "stuck". That is, the kernel will not be able to reduce them
because theorems are always opaque
---
 library/data/bool.lean            |  2 +-
 library/data/int/basic.lean       |  5 +++--
 library/data/int/order.lean       | 10 +++++-----
 library/data/list/basic.lean      |  2 +-
 library/data/nat/basic.lean       |  2 +-
 library/data/nat/order.lean       |  8 ++++----
 library/data/option.lean          |  2 +-
 library/data/prod.lean            |  2 +-
 library/data/subtype.lean         |  2 +-
 library/data/sum.lean             |  2 +-
 library/data/unit.lean            |  2 +-
 library/logic/core/decidable.lean | 20 ++++++++++----------
 12 files changed, 30 insertions(+), 29 deletions(-)

diff --git a/library/data/bool.lean b/library/data/bool.lean
index 4a5da82158..266fbb753d 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -138,7 +138,7 @@ namespace bool
   protected theorem is_inhabited [instance] : inhabited bool :=
   inhabited.mk ff
 
-  protected theorem has_decidable_eq [instance] : decidable_eq bool :=
+  protected definition has_decidable_eq [instance] : decidable_eq bool :=
   take a b : bool,
     rec_on a
       (rec_on b (inl rfl) (inr ff_ne_tt))
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index c17fe1adfe..0bc3946fbc 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -203,8 +203,9 @@ exists_intro (pr1 (rep a))
       a = psub (rep a) : (psub_rep a)⁻¹
     ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}))
 
-protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
-take a b : ℤ, _
+-- TODO it should not be opaque.
+protected opaque definition has_decidable_eq [instance] : decidable_eq ℤ :=
+_
 
 irreducible int
 definition of_nat [coercion] (n : ℕ) : ℤ := psub (pair n 0)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 314bb4892a..87b904c956 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -422,8 +422,8 @@ Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n)
 theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
 iff.mp (iff.symm (le_of_nat _ _)) zero_le
 
-theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
-have aux : ∀x, decidable (0 ≤ x), from
+definition le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
+have aux : Πx, decidable (0 ≤ x), from
   take x,
     have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from
       iff.intro
@@ -432,9 +432,9 @@ have aux : ∀x, decidable (0 ≤ x), from
     decidable_iff_equiv _ (iff.symm H),
 decidable_iff_equiv (aux _) (iff.symm (le_iff_sub_nonneg a b))
 
-theorem ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b)
-theorem lt_decidable [instance] {a b : ℤ} : decidable (a < b)
-theorem gt_decidable [instance] {a b : ℤ} : decidable (a > b)
+definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
+definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _
+definition gt_decidable [instance] {a b : ℤ} : decidable (a > b) := _
 
 --to_nat_neg is already taken... rename?
 theorem to_nat_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 0ebc0b79f7..6192a1eba3 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -204,7 +204,7 @@ induction_on l
           from H3 ▸ rfl,
         exists_intro _ (exists_intro _ H4)))
 
-theorem mem_is_decidable [instance] {H : decidable_eq T} {x : T} {l : list T} : decidable (x ∈ l) :=
+definition mem_is_decidable [instance] {H : decidable_eq T} {x : T} {l : list T} : decidable (x ∈ l) :=
 rec_on l
   (decidable.inr (iff.false_elim mem_nil))
   (λ (h : T) (l : list T) (iH : decidable (x ∈ l)),
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index b38018af49..07c962ff3d 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -105,7 +105,7 @@ induction_on n
     absurd H ne)
   (take k IH H, IH (succ_inj H))
 
-protected theorem has_decidable_eq [instance] : decidable_eq ℕ :=
+protected definition has_decidable_eq [instance] : decidable_eq ℕ :=
 take n m : ℕ,
 have general : ∀n, decidable (n = m), from
   rec_on m
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index f700863d3c..79bc63786c 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -230,7 +230,7 @@ le_trans (mul_le_right H1 m) (mul_le_left H2 k)
 
 -- mul_le_[left|right]_inv below
 
-theorem le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
+definition le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
 have general : ∀n, decidable (n ≤ m), from
   rec_on m
     (take n,
@@ -422,9 +422,9 @@ theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
 or.resolve_right le_or_gt H
 
 -- The following three theorems are automatically proved using the instance le_decidable
-theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m)
-theorem gt_decidable [instance] (n m : ℕ) : decidable (n > m)
-theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m)
+definition lt_decidable [instance] (n m : ℕ) : decidable (n < m) := _
+definition gt_decidable [instance] (n m : ℕ) : decidable (n > m) := _
+definition ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) := _
 
 -- Note: interaction with multiplication under "positivity"
 
diff --git a/library/data/option.lean b/library/data/option.lean
index 5857b7459b..387a499139 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -38,7 +38,7 @@ namespace option
   protected theorem is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none
 
-  protected theorem has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
+  protected definition has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
   take o₁ o₂ : option A,
     rec_on o₁
       (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
diff --git a/library/data/prod.lean b/library/data/prod.lean
index d8d41cd9dd..e12b3e4aee 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -48,7 +48,7 @@ section
   protected theorem is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
 
-  protected theorem has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
+  protected definition has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
   take u v : A × B,
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff.intro
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index c462e789b3..3e217a162d 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -41,7 +41,7 @@ section
   protected theorem is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited.mk (tag a H)
 
-  protected theorem has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
+  protected definition has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {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),
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 9db6904a1b..f517f66a8a 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -55,7 +55,7 @@ namespace sum
   protected theorem is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
   inhabited.mk (inr A (default B))
 
-  protected theorem has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
+  protected definition has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
        decidable_eq (A ⊎ B) :=
   take s1 s2 : A ⊎ B,
     rec_on s1
diff --git a/library/data/unit.lean b/library/data/unit.lean
index 36a1289a89..aee94ce84c 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -18,6 +18,6 @@ namespace unit
   protected theorem is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆
 
-  protected theorem has_decidable_eq [instance] : decidable_eq unit :=
+  protected definition has_decidable_eq [instance] : decidable_eq unit :=
   take (a b : unit), inl (equal a b)
 end unit
diff --git a/library/logic/core/decidable.lean b/library/logic/core/decidable.lean
index 876ec1eba2..44c373e7bb 100644
--- a/library/logic/core/decidable.lean
+++ b/library/logic/core/decidable.lean
@@ -10,10 +10,10 @@ inr : ¬p → decidable p
 
 namespace decidable
 
-theorem true_decidable [instance] : decidable true :=
+definition true_decidable [instance] : decidable true :=
 inl trivial
 
-theorem false_decidable [instance] : decidable false :=
+definition false_decidable [instance] : decidable false :=
 inr not_false_trivial
 
 protected theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
@@ -38,7 +38,7 @@ decidable.rec
 theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
 induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
 
-theorem by_cases {a : Prop} {b : Type} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
+definition by_cases {a : Prop} {b : Type} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
 rec_on C (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
 
 theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
@@ -46,7 +46,7 @@ or.elim (em p)
   (assume H1 : p, H1)
   (assume H1 : ¬p, false_elim (H H1))
 
-theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ∧ b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
@@ -54,7 +54,7 @@ rec_on Ha
     (assume Hnb : ¬b, inr (and.not_right a Hnb)))
   (assume Hna : ¬a, inr (and.not_left b Hna))
 
-theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ∨ b) :=
 rec_on Ha
   (assume Ha  : a, inl (or.inl Ha))
@@ -62,12 +62,12 @@ rec_on Ha
     (assume Hb  : b,  inl (or.inr Hb))
     (assume Hnb : ¬b, inr (or.not_intro Hna Hnb)))
 
-theorem not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
+definition not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
 rec_on Ha
   (assume Ha,  inr (not_not_intro Ha))
   (assume Hna, inl Hna)
 
-theorem iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ↔ b) :=
 rec_on Ha
   (assume Ha, rec_on Hb
@@ -78,7 +78,7 @@ rec_on Ha
     (assume Hnb : ¬b, inl
         (iff.intro (assume Ha, absurd Ha Hna) (assume Hb, absurd Hb Hnb))))
 
-theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a → b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
@@ -86,12 +86,12 @@ rec_on Ha
     (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
   (assume Hna : ¬a, inl (assume Ha, absurd Ha Hna))
 
-theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
+definition decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
 rec_on Ha
   (assume Ha : a,   inl (iff.elim_left H Ha))
   (assume Hna : ¬a, inr (iff.elim_left (iff.flip_sign H) Hna))
 
-theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
+definition decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
 decidable_iff_equiv Ha (eq_to_iff H)
 
 end decidable