feat(builtin/kernel): add skolem_th, we need it to justify skolemization preprocessing step

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

src/builtin/kernel.lean

@@ -211,10 +211,12 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
       absurd H (H1 a)
 
 theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A
-:= exists_elim H (λ (w : A) (Hw : P w), exists_intro w trivial)
+:= obtain (w : A) (Hw : P w), from H,
+      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), @eps_ax A (nonempty_ex_intro H) P w Hw)
+:= obtain (w : A) (Hw : P w), from H,
+      @eps_ax A (nonempty_ex_intro H) 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
@@ -233,6 +235,15 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b
 := boolext Hab Hba
 
+theorem skolem_th {A : TypeU} {B : TypeU} {P : A → B → Bool} :
+        (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
+:= iff_intro
+      (λ H : (∀ x, ∃ y, P x y),
+             @axiom_of_choice A B P H)
+      (λ H : (∃ f, (∀ x, P x (f x))),
+             take x, obtain (fw : A → B) (Hw : ∀ x, P x (fw x)), from H,
+                  exists_intro (fw x) (Hw x))
+
 theorem eqt_intro {a : Bool} (H : a) : a = true
 := boolext (assume H1 : a,    trivial)
            (assume H2 : true, H)

src/kernel/kernel_decls.cpp

@@ -70,6 +70,7 @@ 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(skolem_th_fn, name("skolem_th"));
 MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
 MK_CONSTANT(eqf_intro_fn, name("eqf_intro"));
 MK_CONSTANT(neq_elim_fn, name("neq_elim"));

src/kernel/kernel_decls.h

@@ -203,6 +203,9 @@ inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, exp
 expr mk_iff_intro_fn();
 bool is_iff_intro_fn(expr const & e);
 inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); }
+expr mk_skolem_th_fn();
+bool is_skolem_th_fn(expr const & e);
+inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); }
 expr mk_eqt_intro_fn();
 bool is_eqt_intro_fn(expr const & e);
 inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); }