From a7654cfdbe5b60c93d5ceb88c9b90530ccc19024 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 20:16:01 -0800 Subject: [PATCH] chore(builtin/basic): remove unnecessary parentheses Signed-off-by: Leonardo de Moura --- src/builtin/basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/builtin/basic.lean b/src/builtin/basic.lean index cb3aae0526..27b042fda4 100644 --- a/src/builtin/basic.lean +++ b/src/builtin/basic.lean @@ -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)