From c37b5afe936354fbcb41deed85c2bfeff58ff261 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Jul 2014 20:09:47 +0100
Subject: [PATCH] feat(library/standard): add decidable class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/bit.lean            | 37 ++++++------------------
 library/standard/bool_decidable.lean | 26 +++++++++++++++++
 library/standard/decidable.lean      | 43 ++++++++++++++++++++++++++++
 library/standard/if.lean             | 34 ++++++++++++++++++++++
 library/standard/logic.lean          | 24 +++++++++++++++-
 library/standard/pair.lean           |  6 ++++
 library/standard/standard.lean       |  3 ++
 library/standard/sum.lean            | 15 ++++++++++
 library/standard/unit.lean           | 12 +++++++-
 9 files changed, 169 insertions(+), 31 deletions(-)
 create mode 100644 library/standard/bool_decidable.lean
 create mode 100644 library/standard/decidable.lean
 create mode 100644 library/standard/if.lean
 create mode 100644 library/standard/sum.lean

diff --git a/library/standard/bit.lean b/library/standard/bit.lean
index a2bdda654..2ce617365 100644
--- a/library/standard/bit.lean
+++ b/library/standard/bit.lean
@@ -1,7 +1,8 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+import logic decidable
+
 namespace bit
 inductive bit : Type :=
 | b0 : bit
@@ -110,32 +111,10 @@ theorem bnot_false : !'0 = '1
 theorem bnot_true  : !'1 = '0
 := refl _
 
-definition beq (a b : bit) : bit
-:= bit_rec (bit_rec '1 '0 b) (bit_rec '0 '1 b) a
-
-infix `==`:50 := beq
-
-theorem beq_refl (a : bit) : (a == a) = '1
-:= induction_on a (refl ('0 == '0)) (refl ('1 == '1))
-
-theorem beq_b1_left (a : bit) : ('1 == a) = a
-:= induction_on a (refl ('1 == '0)) (refl ('1 == '1))
-
-theorem beq_b1_right (a : bit) : (a == '1) = a
-:= induction_on a (refl ('0 == '1)) (refl ('1 == '1))
-
-theorem beq_symm (a b : bit) : (a == b) = (b == a)
-:= induction_on a
-    (induction_on b (refl ('0 == '0)) (refl ('0 == '1)))
-    (induction_on b (refl ('1 == '0)) (refl ('1 == '1)))
-
-theorem to_eq {a b : bit} : a == b = '1 → a = b
-:= induction_on a
-    (induction_on b (assume H, refl '0) (assume H, absurd_elim ('0 = '1) (trans (symm (beq_b1_right '0)) H) b0_ne_b1))
-    (induction_on b (assume H, absurd_elim ('1 = '0) (trans (symm (beq_b1_left '0)) H) b0_ne_b1) (assume H, refl '1))
-
-theorem beq_eq (a b : bit) : (a == b) = '1 ↔ a = b
-:= iff_intro
-    (assume H, to_eq H)
-    (assume H, subst H (beq_refl a))
+using decidable
+theorem decidable_eq [instance] (a b : bit) : decidable (a = b)
+:= bit_rec
+    (bit_rec (inl (refl '0)) (inr b0_ne_b1) b)
+    (bit_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b)
+    a
 end
diff --git a/library/standard/bool_decidable.lean b/library/standard/bool_decidable.lean
new file mode 100644
index 000000000..f2b9040f4
--- /dev/null
+++ b/library/standard/bool_decidable.lean
@@ -0,0 +1,26 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import classical hilbert bit decidable
+using bit decidable
+
+-- Excluded middle + Hilbert implies every proposition is decidable
+definition to_bit (a : Bool) : bit
+:= epsilon (λ b : bit, (b = '1) ↔ a)
+
+theorem to_bit_def (a : Bool) : (to_bit a) = '1 ↔ a
+:= or_elim (em a)
+    (assume Hp, epsilon_ax (exists_intro '1 (iff_intro (assume H, Hp) (assume H, refl b1))))
+    (assume Hn, epsilon_ax (exists_intro '0 (iff_intro (assume H, absurd_elim a H b0_ne_b1) (assume H, absurd_elim ('0 = '1) H Hn))))
+
+theorem bool_decidable [instance] (a : Bool) : decidable a
+:= bit_rec
+    (assume H0 : to_bit a = '0,
+     have e1 : ¬ to_bit a = '1, from subst (symm H0) b0_ne_b1,
+     have Hna : ¬a, from iff_mp_left (iff_flip_sign (to_bit_def a)) e1,
+     inr Hna)
+    (assume H1 : to_bit a = '1,
+     have Ha : a, from iff_mp_left (to_bit_def a) H1,
+     inl Ha)
+    (to_bit a)
+    (refl (to_bit a))
diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean
new file mode 100644
index 000000000..1a0a4ab0a
--- /dev/null
+++ b/library/standard/decidable.lean
@@ -0,0 +1,43 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import logic
+
+namespace decidable
+inductive decidable (p : Bool) : Type :=
+| inl : p  → decidable p
+| inr : ¬p → decidable p
+
+theorem induction_on {p : Bool} {C : Bool} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
+:= decidable_rec H1 H2 H
+
+theorem em (p : Bool) (H : decidable p) : p ∨ ¬p
+:= induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp)
+
+definition rec [inline] {p : Bool} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
+:= decidable_rec H1 H2 H
+
+theorem decidable_true [instance] : decidable true
+:= inl trivial
+
+theorem decidable_false [instance] : decidable false
+:= inr not_false_trivial
+
+theorem decidable_and [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b)
+:= rec Ha
+    (assume Ha  : a, rec Hb
+      (assume Hb  : b,  inl (and_intro Ha Hb))
+      (assume Hnb : ¬b, inr (and_not_right a Hnb)))
+    (assume Hna : ¬a, inr (and_not_left b Hna))
+
+theorem decidable_or [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
+:= rec Ha
+    (assume Ha  : a, inl (or_intro_left b Ha))
+    (assume Hna : ¬a, rec Hb
+      (assume Hb  : b,  inl (or_intro_right a Hb))
+      (assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
+
+theorem decidable_not [instance] {a : Bool} (Ha : decidable a) : decidable (¬a)
+:= rec Ha
+    (assume Ha,  inr (not_not_intro Ha))
+    (assume Hna, inl Hna)
diff --git a/library/standard/if.lean b/library/standard/if.lean
new file mode 100644
index 000000000..0e8965688
--- /dev/null
+++ b/library/standard/if.lean
@@ -0,0 +1,34 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import decidable tactic
+using bit decidable tactic
+
+definition ite (c : Bool) {H : decidable c} {A : Type} (t e : A) : A
+:= rec H (assume Hc,  t) (assume Hnc, e)
+
+notation `if` c `then` t `else` e:45 := ite c t e
+
+theorem if_pos {c : Bool} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t
+:= decidable_rec
+    (assume Hc : c,    calc (@ite c (inl Hc) A t e) = t : refl _)
+    (assume Hnc : ¬c,  absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc)
+    H
+
+theorem if_neg {c : Bool} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e
+:= decidable_rec
+    (assume Hc : c,    absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc)
+    (assume Hnc : ¬c,  calc (@ite c (inr Hnc) A t e) = e : refl _)
+    H
+
+theorem if_t_t (c : Bool) {H : decidable c} {A : Type} (t : A) : (@ite c H A t t) = t -- check why '(if c then t else t) = t' fails
+:= decidable_rec
+    (assume Hc  : c,  calc (@ite c (inl Hc)  A t t) = t : refl _)
+    (assume Hnc : ¬c, calc (@ite c (inr Hnc) A t t) = t : refl _)
+    H
+
+theorem if_true {A : Type} (t e : A) : (if true then t else e) = t
+:= if_pos trivial t e
+
+theorem if_false {A : Type} (t e : A) : (if false then t else e) = e
+:= if_neg not_false_trivial t e
diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index c12b52636..d43fcb32a 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -27,6 +27,9 @@ theorem not_elim {a : Bool} (H1 : ¬a) (H2 : a) : false
 theorem absurd {a : Bool} (H1 : a) (H2 : ¬a) : false
 := H2 H1
 
+theorem not_not_intro {a : Bool} (Ha : a) : ¬¬a
+:= assume Hna : ¬a, absurd Ha Hna
+
 theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬b) : ¬a
 := assume Ha : a, absurd (H1 Ha) H2
 
@@ -66,6 +69,12 @@ theorem and_elim_right {a b : Bool} (H : a ∧ b) : b
 theorem and_swap {a b : Bool} (H : a ∧ b) : b ∧ a
 := and_intro (and_elim_right H) (and_elim_left H)
 
+theorem and_not_left {a : Bool} (b : Bool) (Hna : ¬a) : ¬(a ∧ b)
+:= assume H : a ∧ b, absurd (and_elim_left H) Hna
+
+theorem and_not_right (a : Bool) {b : Bool} (Hnb : ¬b) : ¬(a ∧ b)
+:= assume H : a ∧ b, absurd (and_elim_right H) Hnb
+
 inductive or (a b : Bool) : Bool :=
 | or_intro_left  : a → or a b
 | or_intro_right : b → or a b
@@ -85,6 +94,11 @@ theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬b) : a
 theorem or_swap {a b : Bool} (H : a ∨ b) : b ∨ a
 := or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb)
 
+theorem or_not_intro {a b : Bool} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
+:= assume H : a ∨ b, or_elim H
+    (assume Ha, absurd_elim _ Ha Hna)
+    (assume Hb, absurd_elim _ Hb Hnb)
+
 inductive eq {A : Type} (a : A) : A → Bool :=
 | refl : eq a a
 
@@ -161,9 +175,12 @@ theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false
 theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false
 := H (refl a)
 
-theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a
+theorem not_eq_symm {A : Type} {a b : A} (H : ¬ a = b) : ¬ b = a
 := assume H1 : b = a, H (symm H1)
 
+theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a
+:= not_eq_symm H
+
 theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c
 := subst (symm H1) H2
 
@@ -194,6 +211,11 @@ theorem iff_mp_left {a b : Bool} (H1 : a ↔ b) (H2 : a) : b
 theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a
 := (iff_elim_right H1) H2
 
+theorem iff_flip_sign {a b : Bool} (H1 : a ↔ b) : ¬a ↔ ¬b
+:= iff_intro
+    (assume Hna, mt (iff_elim_right H1) Hna)
+    (assume Hnb, mt (iff_elim_left H1) Hnb)
+
 theorem eq_to_iff {a b : Bool} (H : a = b) : a ↔ b
 := iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
 
diff --git a/library/standard/pair.lean b/library/standard/pair.lean
index bc6f135f6..186f6636e 100644
--- a/library/standard/pair.lean
+++ b/library/standard/pair.lean
@@ -25,6 +25,12 @@ section
 
   theorem pair_ext (p : pair A B) : mk_pair (fst p) (snd p) = p
   := pair_rec (λ x y, refl (mk_pair x y)) p
+
+  theorem pair_ext_eq {p1 p2 : pair A B} (H1 : fst p1 = fst p2) (H2 : snd p1 = snd p2) : p1 = p2
+  := calc p1  = mk_pair (fst p1) (snd p1) : symm (pair_ext p1)
+          ... = mk_pair (fst p2) (snd p1) : {H1}
+          ... = mk_pair (fst p2) (snd p2) : {H2}
+          ... = p2                        : pair_ext p2
 end
 
 instance pair_inhabited
diff --git a/library/standard/standard.lean b/library/standard/standard.lean
index 5fe71f0fe..28cb338bb 100644
--- a/library/standard/standard.lean
+++ b/library/standard/standard.lean
@@ -1 +1,4 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
 import logic tactic num string pair cast
diff --git a/library/standard/sum.lean b/library/standard/sum.lean
new file mode 100644
index 000000000..a1573341d
--- /dev/null
+++ b/library/standard/sum.lean
@@ -0,0 +1,15 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import logic
+
+namespace sum
+inductive sum (A : Type) (B : Type) : Type :=
+| inl : A → sum A B
+| inr : B → sum A B
+
+infixr `+`:25 := sum
+
+theorem induction_on {A : Type} {B : Type} {C : Bool} (s : A + B) (H1 : A → C) (H2 : B → C) : C
+:= sum_rec H1 H2 s
+end
\ No newline at end of file
diff --git a/library/standard/unit.lean b/library/standard/unit.lean
index e6c66a317..4bdefb1b6 100644
--- a/library/standard/unit.lean
+++ b/library/standard/unit.lean
@@ -1,10 +1,20 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+import logic decidable
+using decidable
 
+namespace unit
 inductive unit : Type :=
 | tt : unit
 
+theorem unit_eq (a b : unit) : a = b
+:= unit_rec (unit_rec (refl tt) b) a
+
 theorem inhabited_unit [instance] : inhabited unit
 := inhabited_intro tt
+
+using decidable
+theorem decidable_eq [instance] (a b : unit) : decidable (a = b)
+:= inl (unit_eq a b)
+end
\ No newline at end of file