feat(builtin): add optional type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/CMakeLists.txt

@@ -93,6 +93,8 @@ add_kernel_theory("Nat.lean"       ${CMAKE_CURRENT_BINARY_DIR}/kernel.olean)
 add_theory("Int.lean"          "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 add_theory("Real.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
 add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
+add_theory("subtype.lean"      "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+add_theory("optional.lean"     "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
 
 update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")

src/builtin/kernel.lean

@@ -88,6 +88,9 @@ theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
 definition Exists (A : (Type U)) (P : A → Bool)
 := ¬ (∀ x, ¬ (P x))
 
+definition exists_unique {A : (Type U)} (p : A → Bool)
+:= ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y
+
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
 theorem false_elim (a : Bool) (H : false) : a

src/builtin/optional.lean

@@ -0,0 +1,69 @@
+import subtype
+import macros
+using subtype
+-- We are encoding the (optional A) as a subset of A → Bool where
+--   none     is the predicate that is false everywhere
+--   some(a)  is the predicate that is true only at a
+definition optional_pred (A : (Type U)) := (λ p : A → Bool, (∀ x, ¬ p x) ∨ exists_unique p)
+definition optional (A : (Type U)) := subtype (A → Bool) (optional_pred A)
+
+namespace optional
+theorem some_pred {A : (Type U)} (a : A) : optional_pred A (λ x, x = a)
+:= or_intror
+     (∀ x, ¬ x = a)
+     (exists_intro a
+       (and_intro (refl a) (take y, assume H : y ≠ a, H)))
+
+theorem none_pred (A : (Type U)) : optional_pred A (λ x, false)
+:= or_introl (take x, not_false_trivial) (exists_unique (λ x, false))
+
+theorem optional_inhabited (A : (Type U)) : inhabited (optional A)
+:= subtype_inhabited (exists_intro (λ x, false) (none_pred A))
+
+definition none {A : (Type U)} : optional A
+:= abst (λ x, false) (optional_inhabited A)
+
+definition some {A : (Type U)} (a : A) : optional A
+:= abst (λ x, x = a) (optional_inhabited A)
+
+definition is_some {A : (Type U)} (n : optional A) := ∃ x : A, some x = n
+
+theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
+:= assume Heq,
+     let eq_reps : (λ x, x = a) = (λ x, x = a') := abst_inj (optional_inhabited A) (some_pred a) (some_pred a') Heq
+     in  (congr1 a eq_reps) ◂ (refl a)
+
+theorem distinct {A : (Type U)} (a : A) : some a ≠ none
+:= assume N : some a = none,
+     let eq_reps : (λ x, x = a) = (λ x, false) := abst_inj (optional_inhabited A) (some_pred a) (none_pred A) N
+     in (congr1 a eq_reps) ◂ (refl a)
+
+definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
+:= ε (inhabited_ex_intro H) (λ x, some x = n)
+
+theorem is_some_some {A : (Type U)} (a : A) : is_some (some a)
+:= exists_intro a (refl (some a))
+
+theorem not_is_some_none {A : (Type U)} : ¬ is_some (@none A)
+:= assume N : is_some (@none A),
+     obtain (w : A) (Hw : some w = @none A), from N,
+       absurd Hw (distinct w)
+
+theorem value_some {A : (Type U)} (a : A) (H : is_some (some a)) : value (some a) H = a
+:= let eq1  : some (value (some a) H) = some a := eps_ax (inhabited_ex_intro H) a (refl (some a))
+   in injectivity eq1
+
+-- TODO
+-- theorem dichotomy {A : (Type U)} (n : optional A) : n = none ∨ ∃ a, n = some a
+-- theorem induction {A : (Type U)} {P : optional A → Bool} (H1 : P none) (H2 : ∀ x, P (some x)) : ∀ o, P o
+
+set_opaque some           true
+set_opaque none           true
+set_opaque is_some        true
+set_opaque value          true
+end
+set_opaque optional       true
+set_opaque optional_pred  true
+definition optional_inhabited := optional::optional_inhabited
+add_rewrite optional::is_some_some optional::not_is_some_none optional::distinct optional::value_some
+

src/builtin/subtype.lean

@@ -1,6 +1,4 @@
-import heq
 import macros
-
 -- Simulate "subtypes" using Sigma types and proof irrelevance
 definition subtype (A : (Type U)) (P : A → Bool) := sig x, P x
 
@@ -30,23 +28,16 @@ theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (
                 @eps_ax (subtype A P) H (λ x, rep x = rep a) a (refl (rep a))
    in rep_inj s1
 
-theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r ↔ rep (abst r H) = r
+theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r
-:= take r, iff_intro
+:= take r, assume Hl : P r,
-     (assume Hl : P r,
+     @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r)
-         @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r))
-     (assume Hr : rep (abst r H) = r,
-         let s1 : P (rep (abst r H)) := P_rep (abst r H)
-         in  subst s1 Hr)
 
-theorem abst_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} :
+theorem abst_inj {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} :
-                  P r → P r' → (abst r H = abst r' H ↔ r = r')
+                 P r → P r' → abst r H = abst r' H → r = r'
-:= assume Hr Hr', iff_intro
+:= assume Hr Hr' Heq,
-     (assume Heq : abst r H = abst r' H,
+      calc r    = rep (abst r  H)  :  symm (rep_abst H r Hr)
-         calc r    = rep (abst r  H)  :  symm ((rep_abst H r) ◂ Hr)
+           ...  = rep (abst r' H)  :  { Heq }
-              ...  = rep (abst r' H)  :  { Heq }
+           ...  = r'               :  rep_abst H r' Hr'
-              ...  = r'               :  (rep_abst H r') ◂ Hr')
-     (assume Heq : r = r',
-         calc abst r H = abst r' H  : { Heq })
 
 theorem ex_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) :
                ∀ a, ∃ r, abst r H = a ∧ P r

src/kernel/kernel_decls.cpp

@@ -27,6 +27,7 @@ MK_CONSTANT(em_fn, name("em"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(absurd_fn, name("absurd"));
 MK_CONSTANT(exists_fn, name("exists"));
+MK_CONSTANT(exists_unique_fn, name("exists_unique"));
 MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(false_elim_fn, name("false_elim"));
 MK_CONSTANT(mt_fn, name("mt"));

src/kernel/kernel_decls.h

@@ -72,6 +72,10 @@ expr mk_exists_fn();
 bool is_exists_fn(expr const & e);
 inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)) && num_args(e) == 3; }
 inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
+expr mk_exists_unique_fn();
+bool is_exists_unique_fn(expr const & e);
+inline bool is_exists_unique(expr const & e) { return is_app(e) && is_exists_unique_fn(arg(e, 0)) && num_args(e) == 3; }
+inline expr mk_exists_unique(expr const & e1, expr const & e2) { return mk_app({mk_exists_unique_fn(), e1, e2}); }
 expr mk_case_fn();
 bool is_case_fn(expr const & e);
 inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }