From 40183da6b54d8deef242bac074079617d4a657c2 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 21 Jan 2000 18:42:22 +0000 Subject: gros commit de tout ce que j'ai fait pendant les vacances : - tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/Classical_Pred_Set.v | 57 +++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100755 theories/Logic/Classical_Pred_Set.v (limited to 'theories/Logic/Classical_Pred_Set.v') diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v new file mode 100755 index 000000000..3b4e17041 --- /dev/null +++ b/theories/Logic/Classical_Pred_Set.v @@ -0,0 +1,57 @@ + +(* $Id$ *) + +(* Classical Predicate Logic on Set*) + +Require Classical_Prop. + +Section Generic. +Variable U: Set. + +(* de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EX n:U | ~(P n)). +Proof. +Unfold not; Intros P notall. +Apply NNPP; Unfold not. +Intro abs. +Cut ((n:U)(P n)); Auto. +Intro n; Apply NNPP. +Unfold not; Intros. +Apply abs; Exists n; Trivial. +Qed. + +Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EX n:U |(P n)). +Proof. +Intros P H. +Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n. +Apply NNPP; Trivial. +Qed. + +Lemma not_ex_all_not : (P:U->Prop) (~(EX n:U |(P n))) -> (n:U)~(P n). +Proof. +Unfold not; Intros P notex n abs. +Apply notex. +Exists n; Trivial. +Qed. + +Lemma not_ex_not_all : (P:U->Prop)(~(EX n:U | ~(P n))) -> (n:U)(P n). +Proof. +Intros P H n. +Apply NNPP. +Red; Intro K; Apply H; Exists n; Trivial. +Qed. + +Lemma ex_not_not_all : (P:U->Prop) (EX n:U | ~(P n)) -> ~(n:U)(P n). +Proof. +Unfold not; Intros P exnot allP. +Elim exnot; Auto. +Qed. + +Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EX n:U |(P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. -- cgit v1.2.3