feat(builtin): simulate subtypes using sigma types

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

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

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

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"));
 }

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}); }
 }