diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-21 18:42:22 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-21 18:42:22 +0000 |
commit | 40183da6b54d8deef242bac074079617d4a657c2 (patch) | |
tree | 4e70870a5b1e36ba65965f6e87cd8141d01d8d75 /theories/Logic/Classical_Pred_Type.v | |
parent | 249c6b5e1e2d00549dde9093e134df2f25a68609 (diff) |
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
Diffstat (limited to 'theories/Logic/Classical_Pred_Type.v')
-rwxr-xr-x | theories/Logic/Classical_Pred_Type.v | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v new file mode 100755 index 000000000..2f3b331cb --- /dev/null +++ b/theories/Logic/Classical_Pred_Type.v @@ -0,0 +1,57 @@ + +(* $Id$ *) + +(* Classical Predicate Logic on Type *) + +Require Classical_Prop. + +Section Generic. +Variable U: Type. + +(* de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EXT 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)) -> (EXT 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)(~(EXT 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)(~(EXT 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) (EXT 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)) -> ~(EXT n:U | (P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. |