From 9a677331da82836fb5d2de46a3f1256fb61da285 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2014 01:46:50 -0800 Subject: [PATCH] feat(builtin): simulate subtypes using sigma types Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 13 ++++++-- src/builtin/obj/kernel.olean | Bin 44201 -> 44428 bytes src/builtin/subtype.lean | 58 +++++++++++++++++++++++++++++++++++ src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 5 ++- 5 files changed, 73 insertions(+), 4 deletions(-) create mode 100644 src/builtin/subtype.lean diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 45aa54ac3..1fdac42a1 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -889,6 +889,13 @@ variable ind : Type -- ind is infinite, i.e., there is a function f s.t. f is injective, and not surjective axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f --- Proof irrelevance, this is true in the set theoretic model we have for Lean --- It is also useful when we introduce casts -axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 +-- Pair extensionality +axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} + (H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b) + : a = b + +-- Proof irrelevance, this is true in the set theoretic model we have for Lean. +-- In this model, the interpretation of Bool is the set {{*}, {}}. +-- Thus, if A : Bool is inhabited, then its interpretation must be {*}. +-- So, the interpretation of H1 and H2 must be *. +axiom proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 56f9d8aea2eef8a6f35f36e95734ad8c66cd8118..dab99de9c523c830e09715d0cd85f082b7dbae28 100644 GIT binary patch delta 242 zcmZ2^ld0!6(}uJ)%!!#rlM~xT>N)v1m=YN{nJO4SfEh%ja4;n?Z~_@DGeBGc5K+&; zYhH?5W=<*t0N`#99RL6T diff --git a/src/builtin/subtype.lean b/src/builtin/subtype.lean new file mode 100644 index 000000000..75c7615d4 --- /dev/null +++ b/src/builtin/subtype.lean @@ -0,0 +1,58 @@ +import heq +import macros + +-- Simulate "subtypes" using Sigma types and proof irrelevance +definition subtype (A : (Type U)) (P : A → Bool) := sig x, P x + +namespace subtype +definition rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : A +:= proj1 a + +definition abst {A : (Type U)} {P : A → Bool} (r : A) (H : inhabited (subtype A P)) : subtype A P +:= ε H (λ a, rep a = r) + +theorem subtype_inhabited {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited (subtype A P) +:= obtain (w : A) (Hw : P w), from H, + inhabited_intro (tuple (subtype A P) : w, Hw) + +theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a) +:= proj2 a + +theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a = rep b) : a = b +:= pairext H (proof_irrel (proj2 a) (proj2 b)) + +theorem ex_abst {A : (Type U)} {P : A → Bool} {r : A} (H : P r) : ∃ a, rep a = r +:= exists_intro (tuple (subtype A P) : r, H) (refl r) + +theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (a : subtype A P) + : abst (rep a) H = a +:= let s1 : rep (abst (rep a) H) = rep a := + @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 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 ex_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : + ∀ a, ∃ r, abst r H = a ∧ P r +:= take a, exists_intro (rep a) (and_intro (abst_rep H a) (proj2 a)) + +set_opaque rep true +set_opaque abst true +end -- namespace subtype +set_opaque subtype true diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index db1b56b45..49f6749ad 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -186,5 +186,6 @@ MK_CONSTANT(injective_fn, name("injective")); MK_CONSTANT(non_surjective_fn, name("non_surjective")); MK_CONSTANT(ind, name("ind")); MK_CONSTANT(infinity, name("infinity")); +MK_CONSTANT(pairext_fn, name("pairext")); MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 4ff9b571b..4fae18c7d 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -544,7 +544,10 @@ expr mk_ind(); bool is_ind(expr const & e); expr mk_infinity(); bool is_infinity(expr const & e); +expr mk_pairext_fn(); +bool is_pairext_fn(expr const & e); +inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); } expr mk_proof_irrel_fn(); bool is_proof_irrel_fn(expr const & e); -inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); } +inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3, e4}); } }