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

chore(builtin/basic): remove unnecessary parentheses

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 20:16:01 -08:00
parent de77851a00
commit a7654cfdbe
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/builtin/basic.lean
View file

@ -324,15 +324,15 @@ Theorem ForallEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q
Theorem ExistsEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
:= Congr2 (Exists A) (Abst H).
Theorem NotForall (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)))) :=
Theorem NotForall (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) :=
NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x)))))
in Trans L2 L1.
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))
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 UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)