From b01cf73a91273ebbb410cbf3d36f20f715803818 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Dec 2014 18:14:03 -0800
Subject: [PATCH] feat(library/init/logic): add is_true and is_false

---
 library/init/logic.lean     | 18 ++++++++++++++++++
 tests/lean/run/is_true.lean |  8 ++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 tests/lean/run/is_true.lean

diff --git a/library/init/logic.lean b/library/init/logic.lean
index af9c0ff58..0c1ca6645 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -605,3 +605,21 @@ decidable.rec
 -- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
 theorem dite_ite_eq (c : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
 rfl
+
+definition is_true (c : Prop) [H : decidable c] : Prop :=
+if c then true else false
+
+definition is_false (c : Prop) [H : decidable c] : Prop :=
+if c then false else true
+
+theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
+decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, false_elim (if_neg Hnc ▸ H₂))
+
+theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c :=
+decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
+
+theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c :=
+decidable.rec_on H₁ (λ Hc, false_elim (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
+
+theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
+decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂))
diff --git a/tests/lean/run/is_true.lean b/tests/lean/run/is_true.lean
new file mode 100644
index 000000000..444a2c0c5
--- /dev/null
+++ b/tests/lean/run/is_true.lean
@@ -0,0 +1,8 @@
+import data.nat
+open nat
+
+example : is_true (2 = 2)  := trivial
+example : is_false (3 = 2) := trivial
+example : is_true (2 < 3) := trivial
+example : is_true (3 | 9) := trivial
+example : is_false (3 | 7) := trivial