michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/standard): add forall and exists theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 02:48:00 +01:00
parent 614d8a768b
commit 638bdd5e12
2 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/standard/classical.lean
View file

@ -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)

10
library/standard/logic.lean
View file

@ -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