From ec1a60b02cdf58daf56300463bb0c2d69398ab72 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Mar 2015 12:41:46 -0700
Subject: [PATCH] feat(library/init/logic): add helper function for proving
 decidable equality

---
 library/data/bool.lean                        | 18 ------------
 library/init/logic.lean                       | 28 +++++++++++++++++++
 .../lean/interactive/alias.input.expected.out |  4 +--
 3 files changed, 30 insertions(+), 20 deletions(-)

diff --git a/library/data/bool.lean b/library/data/bool.lean
index 4b64f06cd..7407d1558 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -22,13 +22,6 @@ namespace bool
   theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
   rfl
 
-  theorem ff_ne_tt : ¬ ff = tt :=
-  assume H : ff = tt, absurd
-    (calc true  = cond tt true false : cond_tt
-            ... = cond ff true false : H
-            ... = false              : cond_ff)
-    true_ne_false
-
   theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt
   | @eq_tt_of_ne_ff tt H := rfl
   | @eq_tt_of_ne_ff ff H := absurd rfl H
@@ -124,14 +117,3 @@ namespace bool
   rfl
 
 end bool
-
-open bool
-
-protected definition bool.is_inhabited [instance] : inhabited bool :=
-inhabited.mk ff
-
-protected definition bool.has_decidable_eq [instance] : decidable_eq bool :=
-take a b : bool,
-  bool.rec_on a
-    (bool.rec_on b (inl rfl) (inr ff_ne_tt))
-    (bool.rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl))
diff --git a/library/init/logic.lean b/library/init/logic.lean
index c708dbabe..ab202e255 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -248,6 +248,8 @@ notation `∃` binders `,` r:(scoped P, Exists P) := r
 theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
 Exists.rec H2 H1
 
+/- decidable -/
+
 inductive decidable [class] (p : Prop) : Type :=
 | inl :  p → decidable p
 | inr : ¬p → decidable p
@@ -334,6 +336,29 @@ definition decidable_eq   [reducible] (A : Type) := decidable_rel (@eq A)
 definition decidable_ne [instance] {A : Type} [H : decidable_eq A] : Π (a b : A), decidable (a ≠ b) :=
 show Π x y : A, decidable (x = y → false), from _
 
+namespace bool
+  definition ff_ne_tt : ff = tt → false
+  | [none]
+end bool
+
+open bool
+definition is_dec_eq {A : Type} (p : A → A → bool) : Prop   := ∀ ⦃x y : A⦄, p x y = tt → x = y
+definition is_dec_refl {A : Type} (p : A → A → bool) : Prop := ∀x, p x x = tt
+
+open decidable
+protected definition bool.has_decidable_eq [instance] : ∀a b : bool, decidable (a = b)
+| ff ff := inl rfl
+| ff tt := inr ff_ne_tt
+| tt ff := inr (ne.symm ff_ne_tt)
+| tt tt := inl rfl
+
+definition decidable_eq_of_bool_pred {A : Type} {p : A → A → bool} (H₁ : is_dec_eq p) (H₂ : is_dec_refl p) : decidable_eq A :=
+take x y : A, by_cases
+ (assume Hp : p x y = tt,   inl (H₁ Hp))
+ (assume Hn : ¬ p x y = tt, inr (assume Hxy : x = y, absurd (H₂ y) (eq.rec_on Hxy Hn)))
+
+/- inhabited -/
+
 inductive inhabited [class] (A : Type) : Type :=
 mk : A → inhabited A
 
@@ -359,6 +384,9 @@ definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabit
   inhabited (Πx, B x) :=
 inhabited.mk (λa, inhabited.rec_on (H a) (λb, b))
 
+protected definition bool.is_inhabited [instance] : inhabited bool :=
+inhabited.mk ff
+
 inductive nonempty [class] (A : Type) : Prop :=
 intro : A → nonempty A
 
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
index e8b6fa2b2..7f6fa7ecd 100644
--- a/tests/lean/interactive/alias.input.expected.out
+++ b/tests/lean/interactive/alias.input.expected.out
@@ -10,7 +10,7 @@ bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
 bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
 bool.tt_band|∀ (a : bool), eq (bool.band bool.tt a) a
 bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
-bool.ff_ne_tt|not (eq bool.ff bool.tt)
+bool.ff_ne_tt|eq bool.ff bool.tt → false
 bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
 bool.tt_bor|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
 -- ENDFINDP
@@ -25,6 +25,6 @@ band_tt|∀ (a : bool), eq (band a tt) a
 absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
 eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
 cond_tt|∀ (t e : ?A), eq (cond tt t e) t
-ff_ne_tt|not (eq ff tt)
+ff_ne_tt|eq ff tt → false
 eq_ff_of_ne_tt|ne ?a tt → eq ?a ff
 -- ENDFINDP