diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 40cb8f1df..36ff51bfb 100644 --- a/src/builtin/CMakeLists.txt +++ b/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") diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 0d155c5aa..9fcf643a7 100644 --- a/src/builtin/kernel.lean +++ b/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 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 2c41e9364..6c1b816f4 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean new file mode 100644 index 000000000..53b5f0d30 Binary files /dev/null and b/src/builtin/obj/optional.olean differ diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean new file mode 100644 index 000000000..c4ee00afd Binary files /dev/null and b/src/builtin/obj/subtype.olean differ diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean new file mode 100644 index 000000000..b804888d2 --- /dev/null +++ b/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 + diff --git a/src/builtin/subtype.lean b/src/builtin/subtype.lean index 503241a6b..caa550730 100644 --- a/src/builtin/subtype.lean +++ b/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 -:= take r, iff_intro - (assume Hl : P 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 rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r +:= take r, assume Hl : P r, + @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r) -theorem abst_abst {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') -:= assume Hr Hr', iff_intro - (assume Heq : abst r H = abst r' H, - calc r = rep (abst r H) : symm ((rep_abst H r) ◂ Hr) - ... = rep (abst r' H) : { Heq } - ... = r' : (rep_abst H r') ◂ Hr') - (assume Heq : r = r', - calc abst r H = abst r' H : { Heq }) +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' +:= assume Hr Hr' Heq, + calc r = rep (abst r H) : symm (rep_abst H r Hr) + ... = rep (abst r' H) : { Heq } + ... = r' : rep_abst H r' Hr' theorem ex_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ a, ∃ r, abst r H = a ∧ P r diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 2234e6d63..6aeb89e18 100644 --- a/src/kernel/kernel_decls.cpp +++ b/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")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index b3029d55b..34768f45a 100644 --- a/src/kernel/kernel_decls.h +++ b/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}); }