feat(builtin/kernel): add more theorems useful for simplification

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

src/builtin/kernel.lean

@@ -210,6 +210,10 @@ 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 nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B
+:= obtain (w : A) (Hw : true), from H1,
+     H2 w
+
 theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A
 := obtain (w : A) (Hw : P w), from H,
       exists_intro w trivial
@@ -333,6 +337,16 @@ theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a
 theorem imp_falsel (a : Bool) : (false → a) ↔ true
 := case (λ x, (false → x) ↔ true) trivial trivial a
 
+theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
+:= iff_intro
+     (assume H : a → b,
+        (or_elim (em a)
+           (λ Ha  : a,   or_intror (¬ a) (H Ha))
+           (λ Hna : ¬ a, or_introl Hna b)))
+     (assume H : ¬ a ∨ b,
+        assume Ha : a,
+          resolve1 H ((symm (not_not_eq a)) ◂ Ha))
+
 theorem not_true : ¬ true ↔ false
 := trivial
 
@@ -384,6 +398,21 @@ theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
 theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
 := congr2 not H
 
+theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∃ x : A, p),
+       obtain (w : A) (Hw : p), from Hl,
+         Hw)
+    (assume Hr : p,
+       nonempty_elim H (λ w, exists_intro w Hr))
+
+theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∀ x : A, p),
+       nonempty_elim H (λ w, Hl w))
+    (assume Hr : p,
+       take x, Hr)
+
 theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x)
 := congr2 (Exists A) (funext H)
 
@@ -573,6 +602,13 @@ theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨
                 obtain (w : A) (Hw : ψ w), from H2,
                     exists_intro w (or_intror (φ w) Hw)))
 
+
+theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x))
+:= calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x)           : eq_exists_intro (λ x, imp_or (φ x) (ψ x))
+                     ...   = (∃ x, ¬ φ x) ∨ (∃ x, ψ x)   : exists_or_distribute _ _
+                     ...   = ¬ (∀ x, φ x) ∨ (∃ x, ψ x)   : { symm (not_forall A φ) }
+                     ...   = (∀ x, φ x) → (∃ x, ψ x)     : symm (imp_or _ _)
+
 set_opaque exists  true
 set_opaque not     true
 set_opaque or      true

src/kernel/kernel_decls.cpp

@@ -65,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_elim_fn, name("nonempty_elim"));
 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"));
@@ -95,6 +96,7 @@ MK_CONSTANT(imp_truer_fn, name("imp_truer"));
 MK_CONSTANT(imp_truel_fn, name("imp_truel"));
 MK_CONSTANT(imp_falser_fn, name("imp_falser"));
 MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
+MK_CONSTANT(imp_or_fn, name("imp_or"));
 MK_CONSTANT(not_true, name("not_true"));
 MK_CONSTANT(not_false, name("not_false"));
 MK_CONSTANT(not_neq_fn, name("not_neq"));
@@ -108,6 +110,8 @@ MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
 MK_CONSTANT(not_implies_fn, name("not_implies"));
 MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
 MK_CONSTANT(not_congr_fn, name("not_congr"));
+MK_CONSTANT(exists_rem_fn, name("exists_rem"));
+MK_CONSTANT(forall_rem_fn, name("forall_rem"));
 MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro"));
 MK_CONSTANT(not_forall_fn, name("not_forall"));
 MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim"));
@@ -134,4 +138,5 @@ MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute"));
 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"));
 }

src/kernel/kernel_decls.h

@@ -188,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_elim_fn();
+bool is_nonempty_elim_fn(expr const & e);
+inline expr mk_nonempty_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_elim_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}); }
@@ -278,6 +281,9 @@ inline expr mk_imp_falser_th(expr const & e1) { return mk_app({mk_imp_falser_fn(
 expr mk_imp_falsel_fn();
 bool is_imp_falsel_fn(expr const & e);
 inline expr mk_imp_falsel_th(expr const & e1) { return mk_app({mk_imp_falsel_fn(), e1}); }
+expr mk_imp_or_fn();
+bool is_imp_or_fn(expr const & e);
+inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); }
 expr mk_not_true();
 bool is_not_true(expr const & e);
 expr mk_not_false();
@@ -315,6 +321,12 @@ inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const
 expr mk_not_congr_fn();
 bool is_not_congr_fn(expr const & e);
 inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); }
+expr mk_exists_rem_fn();
+bool is_exists_rem_fn(expr const & e);
+inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); }
+expr mk_forall_rem_fn();
+bool is_forall_rem_fn(expr const & e);
+inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); }
 expr mk_eq_exists_intro_fn();
 bool is_eq_exists_intro_fn(expr const & e);
 inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); }
@@ -393,4 +405,7 @@ inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr
 expr mk_exists_or_distribute_fn();
 bool is_exists_or_distribute_fn(expr const & e);
 inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_or_distribute_fn(), e1, e2, e3}); }
+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}); }
 }