From 638bdd5e12ea89e6a35fbd4fcd3a716d6acbbf88 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2014 02:48:00 +0100 Subject: [PATCH] feat(library/standard): add forall and exists theorems Signed-off-by: Leonardo de Moura --- library/standard/classical.lean | 11 +++++++++++ library/standard/logic.lean | 10 ++++++++++ 2 files changed, 21 insertions(+) diff --git a/library/standard/classical.lean b/library/standard/classical.lean index b38593966..16694023f 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -143,3 +143,14 @@ theorem a_eq_false (a : Bool) : (a = false) = (¬ a) := boolext (assume H, eqf_elim H) (assume H, eqf_intro H) + +theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬ ∃ x, P x) : ∀ x, ¬ P x +:= take x, or_elim (em (P x)) + (assume Hp : P x, absurd_elim (¬ P x) (exists_intro x Hp) H) + (assume Hn : ¬ P x, Hn) + +theorem not_forall_exists {A : Type} {P : A → Bool} (H : ¬ ∀ x, P x) : ∃ x, ¬ P x +:= by_contradiction (assume H1 : ¬ ∃ x, ¬ P x, + have H2 : ∀ x, ¬ ¬ P x, from not_exists_forall H1, + have H3 : ∀ x, P x, from take x, not_not_elim (H2 x), + absurd H3 H) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index a3d0b9c26..107a7d0e5 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -196,6 +196,16 @@ notation `∃` binders `,` r:(scoped P, Exists P) := r theorem exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) : B := Exists_rec H2 H1 +theorem exists_not_forall {A : Type} {P : A → Bool} (H : ∃ x, P x) : ¬ ∀ x, ¬ P x +:= assume H1 : ∀ x, ¬ P x, + obtain (w : A) (Hw : P w), from H, + absurd Hw (H1 w) + +theorem forall_not_exists {A : Type} {P : A → Bool} (H2 : ∀ x, P x) : ¬ ∃ x, ¬ P x +:= assume H1 : ∃ x, ¬ P x, + obtain (w : A) (Hw : ¬ P w), from H1, + absurd (H2 w) Hw + definition exists_unique {A : Type} (p : A → Bool) := ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y notation `∃!` binders `,` r:(scoped P, exists_unique P) := r