diff options
Diffstat (limited to 'theories/Logic/Classical_Pred_Type.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Logic/Classical_Pred_Type.v | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 804ff32d..56ebf967 100755..100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Type.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: Classical_Pred_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) (** Classical Predicate Logic on Type *) @@ -17,29 +17,30 @@ Variable U : Type. (** de Morgan laws for quantifiers *) -Lemma not_all_ex_not : - forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. +Lemma not_all_not_ex : + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. Proof. -unfold not in |- *; intros P notall. -apply NNPP; unfold not in |- *. +intros P notall. +apply NNPP. intro abs. -cut (forall n:U, P n); auto. -intro n; apply NNPP. -unfold not in |- *; intros. -apply abs; exists n; trivial. +apply notall. +intros n H. +apply abs; exists n; exact H. Qed. -Lemma not_all_not_ex : - forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. +Lemma not_all_ex_not : + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. Proof. -intros P H. -elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. -apply NNPP; trivial. +intros P notall. +apply not_all_not_ex with (P:=fun x => ~ P x). +intro all; apply notall. +intro n; apply NNPP. +apply all. Qed. Lemma not_ex_all_not : forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P notex n abs. apply notex. exists n; trivial. @@ -55,16 +56,16 @@ Qed. Lemma ex_not_not_all : forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). -Proof. +Proof. (* Intuitionistic *) unfold not in |- *; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. Qed. -End Generic.
\ No newline at end of file +End Generic. |