1
(* Copyright 2004 INRIA *)
2
(* $Id: zenon.v 10739 2008-04-01 14:45:20Z herbelin $ *)
4
Require Export Classical.
10
Lemma zenon_noteq : forall (T : Type) (t : T),
14
Lemma zenon_and : forall P Q : Prop,
15
(P -> Q -> False) -> (P /\ Q -> False).
18
Lemma zenon_or : forall P Q : Prop,
19
(P -> False) -> (Q -> False) -> (P \/ Q -> False).
22
Lemma zenon_imply : forall P Q : Prop,
23
(~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
26
Lemma zenon_equiv : forall P Q : Prop,
27
(~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
30
Lemma zenon_notand : forall P Q : Prop,
31
(~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
34
Lemma zenon_notor : forall P Q : Prop,
35
(~P -> ~Q -> False) -> (~(P \/ Q) -> False).
38
Lemma zenon_notimply : forall P Q : Prop,
39
(P -> ~Q -> False) -> (~(P -> Q) -> False).
42
Lemma zenon_notequiv : forall P Q : Prop,
43
(~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
46
Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
47
(forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
48
Proof. firstorder. Qed.
50
Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
51
((P t) -> False) -> ((forall x : T, (P x)) -> False).
52
Proof. firstorder. Qed.
54
Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
55
(~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
56
Proof. firstorder. Qed.
58
Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
59
(forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
60
Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
62
Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
65
Lemma zenon_equal_step :
66
forall (S T : Type) (fa fb : S -> T) (a b : S),
67
(fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
68
Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
70
Lemma zenon_pnotp : forall P Q : Prop,
71
(P = Q) -> (P -> ~Q -> False).
72
Proof. intros P Q Ha. rewrite Ha. auto. Qed.
74
Lemma zenon_notequal : forall (T : Type) (a b : T),
75
(a = b) -> (a <> b -> False).
78
Ltac zenon_intro id :=
79
intro id || let nid := fresh in (intro nid; clear nid)
82
Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
83
Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
84
Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
85
Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
86
Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
87
Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
88
Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
89
Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
90
Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
91
Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
93
Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
94
Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.