feat(builtin/kernel): add nonempty_range theorem

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

src/builtin/kernel.lean

@@ -650,6 +650,16 @@ theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x
                      ...   = ¬ (∀ x, φ x) ∨ (∃ x, ψ x)   : { symm (not_forall A φ) }
                      ...   = (∀ x, φ x) → (∃ x, ψ x)     : symm (imp_or _ _)
 
+-- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty
+theorem nonempty_range {A : TypeU} {B : A → TypeU} (H : nonempty (∀ x, B x)) (a : A) : nonempty (B a)
+:= refute (λ N : ¬ nonempty (B a),
+     let s1 : ¬ ∃ x : B a, true       := N,
+         s2 : ∀ x : B a, false        := not_exists_elim s1,
+         s3 : ∃ y : (∀ x, B x), true := H
+     in obtain (w : (∀ x, B x)) (Hw : true), from s3,
+           let s4 : B a := w a
+           in s2 s4)
+
 theorem if_true {A : TypeU} (a b : A) : (if true then a else b) = a
 := calc (if true then a else b) = ε (nonempty_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b)
                            ...  = ε (nonempty_intro a) (λ r, r = a)                               : by simp

src/kernel/kernel_decls.cpp

@@ -147,6 +147,7 @@ MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer"));
 MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
 MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute"));
 MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute"));
+MK_CONSTANT(nonempty_range_fn, name("nonempty_range"));
 MK_CONSTANT(if_true_fn, name("if_true"));
 MK_CONSTANT(if_false_fn, name("if_false"));
 MK_CONSTANT(if_a_a_fn, name("if_a_a"));

src/kernel/kernel_decls.h

@@ -433,6 +433,9 @@ inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr co
 expr mk_exists_imp_distribute_fn();
 bool is_exists_imp_distribute_fn(expr const & e);
 inline expr mk_exists_imp_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_imp_distribute_fn(), e1, e2, e3}); }
+expr mk_nonempty_range_fn();
+bool is_nonempty_range_fn(expr const & e);
+inline expr mk_nonempty_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_range_fn(), e1, e2, e3, e4}); }
 expr mk_if_true_fn();
 bool is_if_true_fn(expr const & e);
 inline expr mk_if_true_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_true_fn(), e1, e2, e3}); }