feat(builtin/kernel): add Not.*Elim theorems

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

src/builtin/kernel.lean

@@ -306,24 +306,36 @@ Theorem NotAnd (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
         (Case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) Trivial Trivial b)
         a
 
+Theorem NotAndElim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
+:= EqMP (NotAnd a b) H.
+
 Theorem NotOr (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
 := Case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
         (Case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y))   Trivial Trivial b)
         (Case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) Trivial Trivial b)
         a
 
+Theorem NotOrElim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
+:= EqMP (NotOr a b) H.
+
 Theorem NotEq (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
 := Case (λ x, (¬ (x == b)) == ((¬ x) == b))
         (Case (λ y, (¬ (true == y)) == ((¬ true) == y)) Trivial Trivial b)
         (Case (λ y, (¬ (false == y)) == ((¬ false) == y)) Trivial Trivial b)
         a
 
+Theorem NotEqElim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
+:= EqMP (NotEq a b) H.
+
 Theorem NotImp (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
 := Case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b))
         (Case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) Trivial Trivial b)
         (Case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) Trivial Trivial b)
         a
 
+Theorem NotImpElim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b
+:= EqMP (NotImp a b) H.
+
 Theorem NotCongr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
 := Congr2 not H.
 
@@ -339,11 +351,17 @@ Theorem NotForall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (
             NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x)))))
    in Trans L2 L1.
 
+Theorem NotForallElim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
+:= EqMP (NotForall A P) H.
+
 Theorem NotExists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x)
 := let L1 : (¬ ∃ x : A, P x) == (¬ ¬ ∀ x : A, ¬ P x) := Refl (¬ ∃ x : A, P x),
        L2 : (¬ ¬ ∀ x : A, ¬ P x) == (∀ x : A, ¬ P x) := DoubleNeg (∀ x : A, ¬ P x)
    in Trans L1 L2.
 
+Theorem NotExistsElim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
+:= EqMP (NotExists A P) H.
+
 Theorem UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
 := ExistsElim H
      (λ (w : A) (H1 : P w),

tests/lean/exists8.lean

@@ -0,0 +1,27 @@
+Import int.
+Variable P : Int -> Int -> Bool
+
+Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
+         ForallIntro (fun a,
+             ForallIntro (fun b,
+                 ForallElim (NotExistsElim (ForallElim (NotExistsElim R1) a)) b))
+
+Axiom Ax : forall x, exists y, P x y
+
+Theorem T2 : exists x y, P x y :=
+    Refute (fun R : not (exists x y, P x y),
+              let L1 : forall x y, not (P x y) := ForallIntro (fun a,
+                                                     ForallIntro (fun b,
+                                                         ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)),
+                  L2 : exists y, P 0 y         := ForallElim Ax 0
+              in ExistsElim L2 (fun (w : Int) (H : P 0 w),
+                                    Absurd H (ForallElim (ForallElim L1 0) w))).
+
+Theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
+    Refute (fun R : not (exists x y, P x y),
+              let L1 : forall x y, not (P x y) := ForallIntro (fun a,
+                                                     ForallIntro (fun b,
+                                                         ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)),
+                  L2 : exists y, P a y         := ForallElim H1 a
+              in ExistsElim L2 (fun (w : A) (H : P a w),
+                                    Absurd H (ForallElim (ForallElim L1 a) w))).

tests/lean/exists8.lean.expected.out

@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'int'
+  Assumed: P
+  Proved: T1
+  Assumed: Ax
+  Proved: T2
+  Proved: T3