refactor(builtin/kernel): cleanup Hilbert operator definition

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

src/builtin/kernel.lean

@@ -45,7 +45,8 @@ definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x))
 
 definition nonempty (A : TypeU) := ∃ x : A, true
 
-theorem nonempty_intro {A : TypeU} (a : A) : (nonempty A)
+-- If we have an element of type A, then A is nonempty
+theorem nonempty_intro {A : TypeU} (a : A) : nonempty A
 := assume H : (∀ x, ¬ true), (H a)
 
 theorem em (a : Bool) : a ∨ ¬ a
@@ -66,11 +67,14 @@ axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x
 -- Epsilon (Hilbert's operator)
 variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A
 alias ε : eps
-axiom eps_ax {A : TypeU} {P : A → Bool} {a : A} : P a → P (ε (nonempty_intro a) P)
+axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P)
 
 -- Proof irrelevance
 axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
 
+theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P)
+:= assume H : P a, @eps_ax A (nonempty_intro a) P a H
+
 -- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
 theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
 := subst H1 H2
@@ -210,13 +214,9 @@ theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonemp
 := exists_elim H (λ (w : A) (Hw : P w), exists_intro w trivial)
 
 theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P)
-:= exists_elim H (λ (w : A) (Hw : P w),
+:= exists_elim H (λ (w : A) (Hw : P w), @eps_ax A (nonempty_ex_intro H) P w Hw)
-                    let Peps : P (ε (nonempty_intro w) P)                 := @eps_ax A P w Hw,
-                        eqpr : (nonempty_intro w) = (nonempty_ex_intro H) := proof_irrel (nonempty_intro w) (nonempty_ex_intro H)
-                        in subst Peps eqpr)
 
-theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (Hne : nonempty A) (H : ∀ x, ∃ y, R x y) :
+theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
-        ∃ f, ∀ x, R x (f x)
 := exists_intro
       (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f
       (λ x, exists_to_eps (H x))                      -- proof that witness satisfies ∀ x, R x (f x)

src/kernel/kernel_decls.cpp

@@ -15,6 +15,8 @@ MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(iff_fn, name("iff"));
 MK_CONSTANT(exists_fn, name("exists"));
+MK_CONSTANT(nonempty_fn, name("nonempty"));
+MK_CONSTANT(nonempty_intro_fn, name("nonempty_intro"));
 MK_CONSTANT(em_fn, name("em"));
 MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(refl_fn, name("refl"));
@@ -24,6 +26,7 @@ MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(eps_fn, name("eps"));
 MK_CONSTANT(eps_ax_fn, name("eps_ax"));
 MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
+MK_CONSTANT(eps_th_fn, name("eps_th"));
 MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(eta_fn, name("eta"));
@@ -62,6 +65,7 @@ MK_CONSTANT(congr2_fn, name("congr2"));
 MK_CONSTANT(congr_fn, name("congr"));
 MK_CONSTANT(exists_elim_fn, name("exists_elim"));
 MK_CONSTANT(exists_intro_fn, name("exists_intro"));
+MK_CONSTANT(nonempty_ex_intro_fn, name("nonempty_ex_intro"));
 MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps"));
 MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
 MK_CONSTANT(boolext_fn, name("boolext"));

src/kernel/kernel_decls.h

@@ -37,6 +37,13 @@ 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)); }
 inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
+expr mk_nonempty_fn();
+bool is_nonempty_fn(expr const & e);
+inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)); }
+inline expr mk_nonempty(expr const & e1) { return mk_app({mk_nonempty_fn(), e1}); }
+expr mk_nonempty_intro_fn();
+bool is_nonempty_intro_fn(expr const & e);
+inline expr mk_nonempty_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_nonempty_intro_fn(), e1, e2}); }
 expr mk_em_fn();
 bool is_em_fn(expr const & e);
 inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
@@ -58,13 +65,16 @@ inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_eps_fn();
 bool is_eps_fn(expr const & e);
 inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)); }
-inline expr mk_eps(expr const & e1, expr const & e2) { return mk_app({mk_eps_fn(), e1, e2}); }
+inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); }
 expr mk_eps_ax_fn();
 bool is_eps_ax_fn(expr const & e);
-inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4}); }
+inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); }
 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}); }
+expr mk_eps_th_fn();
+bool is_eps_th_fn(expr const & e);
+inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); }
 expr mk_substp_fn();
 bool is_substp_fn(expr const & e);
 inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
@@ -178,6 +188,9 @@ inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_exists_intro_fn();
 bool is_exists_intro_fn(expr const & e);
 inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
+expr mk_nonempty_ex_intro_fn();
+bool is_nonempty_ex_intro_fn(expr const & e);
+inline expr mk_nonempty_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_ex_intro_fn(), e1, e2, e3}); }
 expr mk_exists_to_eps_fn();
 bool is_exists_to_eps_fn(expr const & e);
 inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); }