feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it

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

src/builtin/kernel.lean

@@ -58,6 +58,11 @@ axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A
 -- Forall extensionality
 axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
 
+-- Epsilon (Hilbert's operator)
+variable eps {A : TypeU} (P : A → Bool) : A
+alias ε : eps
+axiom eps_ax {A : TypeU} {P : A → Bool} {a : A} : P a → P (ε P)
+
 -- Proof irrelevance
 axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
 
@@ -196,6 +201,14 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
 := assume H1 : (∀ x : A, ¬ P x),
       absurd H (H1 a)
 
+theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε P)
+:= exists_elim H (λ (w : A) (Hw : P w), @eps_ax A P w Hw)
+
+theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
+:= exists_intro
+      (λ x, ε (λ y, R x y))       -- witness for f
+      (λ x, exists_to_eps (H x))  -- proof that witness satisfies ∀ x, R x (f x)
+
 theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := or_elim (boolcomplete a)
        (λ Hat : a = true,  or_elim (boolcomplete b)

src/kernel/kernel_decls.cpp

@@ -21,6 +21,8 @@ MK_CONSTANT(refl_fn, name("refl"));
 MK_CONSTANT(subst_fn, name("subst"));
 MK_CONSTANT(funext_fn, name("funext"));
 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(substp_fn, name("substp"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
@@ -60,6 +62,8 @@ 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(exists_to_eps_fn, name("exists_to_eps"));
+MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
 MK_CONSTANT(boolext_fn, name("boolext"));
 MK_CONSTANT(iff_intro_fn, name("iff_intro"));
 MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));

src/kernel/kernel_decls.h

@@ -55,6 +55,13 @@ inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_allext_fn();
 bool is_allext_fn(expr const & e);
 inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); }
+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}); }
+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}); }
 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}); }
@@ -171,6 +178,12 @@ 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_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}); }
+expr mk_axiom_of_choice_fn();
+bool is_axiom_of_choice_fn(expr const & e);
+inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); }
 expr mk_boolext_fn();
 bool is_boolext_fn(expr const & e);
 inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); }