feat(builtin/kernel): add nonempty_fun theorem

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

src/builtin/kernel.lean

@@ -85,6 +85,10 @@ theorem eps_singleton {A : TypeU} (H : nonempty A) (a : A) : ε H (λ x, x = a)
        Ha : P a  :=  refl a
    in eps_ax H a Ha
 
+-- A function space (∀ x : A, B x) is nonempty if forall a : A, we have nonempty (B a)
+theorem nonempty_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, nonempty (B a)) : nonempty (∀ x, B x)
+:= nonempty_intro (λ x, ε (Hn x) (λ y, true))
+
 -- if-then-else expression
 definition ite {A : TypeU} (c : Bool) (a b : A) : A
 := ε (nonempty_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b))

src/kernel/kernel_decls.cpp

@@ -29,6 +29,7 @@ MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
 MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(eps_th_fn, name("eps_th"));
 MK_CONSTANT(eps_singleton_fn, name("eps_singleton"));
+MK_CONSTANT(nonempty_fun_fn, name("nonempty_fun"));
 MK_CONSTANT(ite_fn, name("ite"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(eta_fn, name("eta"));

src/kernel/kernel_decls.h

@@ -81,6 +81,9 @@ inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_eps_singleton_fn();
 bool is_eps_singleton_fn(expr const & e);
 inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); }
+expr mk_nonempty_fun_fn();
+bool is_nonempty_fun_fn(expr const & e);
+inline expr mk_nonempty_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_fun_fn(), e1, e2, e3}); }
 expr mk_ite_fn();
 bool is_ite_fn(expr const & e);
 inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; }