From 148836d14bc51deca19ee60ec2ca81671f56cb8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Aug 2014 16:59:01 -0700
Subject: [PATCH] feat(library/standard/data/option): add basic theorems for
 option types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/data/option.lean             | 41 +++++++++++++++++--
 library/standard/logic/classes/decidable.lean |  2 +-
 2 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/library/standard/data/option.lean b/library/standard/data/option.lean
index f86193dc4..026131234 100644
--- a/library/standard/data/option.lean
+++ b/library/standard/data/option.lean
@@ -1,13 +1,48 @@
------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------
+-- 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.connectives.basic logic.connectives.eq logic.classes.inhabited logic.classes.decidable
+using eq_proofs decidable
 
-import logic.classes.inhabited
-
+namespace option
 inductive option (A : Type) : Type :=
 | none {} : option A
 | some    : A → option A
 
+theorem induction_on {A : Type} {p : option A → Prop} (o : option A) (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
+option_rec H1 H2 o
+
+definition rec_on {A : Type} {C : option A → Type} (o : option A) (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
+option_rec H1 H2 o
+
+definition is_none {A : Type} (o : option A) : Prop :=
+option_rec true (λ a, false) o
+
+theorem is_none_none {A : Type} : is_none (@none A) :=
+trivial
+
+theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
+not_false_trivial
+
+theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
+assume H : none = some a, absurd
+  (H ▸ is_none_none)
+  (not_is_none_some a)
+
+theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
+congr2 (option_rec a₁ (λ a, a)) H
+
 theorem inhabited_option [instance] (A : Type) : inhabited (option A) :=
 inhabited_intro none
+
+theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
+rec_on o₁
+  (rec_on o₂ (inl (refl _)) (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 ▸ refl _))
+      (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
+end
\ No newline at end of file
diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean
index e4723a902..96f83683f 100644
--- a/library/standard/logic/classes/decidable.lean
+++ b/library/standard/logic/classes/decidable.lean
@@ -15,7 +15,7 @@ inductive decidable (p : Prop) : Type :=
 theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
 decidable_rec H1 H2 H
 
-theorem em (p : Prop) (H : decidable p) : p ∨ ¬p :=
+theorem em {p : Prop} (H : decidable p) : p ∨ ¬p :=
 induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
 
 definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=