summaryrefslogtreecommitdiff
path: root/plugins/dp/Dp.v
blob: 5ddc44526293108931a36b1191cd0f64cf8c1795 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
(* Calls to external decision procedures *)

Require Export ZArith.
Require Export Classical.

(* Zenon *)

(*  Copyright 2004 INRIA  *)
(*  $Id: Dp.v 12337 2009-09-17 15:58:14Z glondu $  *)

Lemma zenon_nottrue :
  (~True -> False).
Proof. tauto. Qed.

Lemma zenon_noteq : forall (T : Type) (t : T),
  ((t <> t) -> False).
Proof. tauto. Qed.

Lemma zenon_and : forall P Q : Prop,
  (P -> Q -> False) -> (P /\ Q -> False).
Proof. tauto. Qed.

Lemma zenon_or : forall P Q : Prop,
  (P -> False) -> (Q -> False) -> (P \/ Q -> False).
Proof. tauto. Qed.

Lemma zenon_imply : forall P Q : Prop,
  (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
Proof. tauto. Qed.

Lemma zenon_equiv : forall P Q : Prop,
  (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
Proof. tauto. Qed.

Lemma zenon_notand : forall P Q : Prop,
  (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
Proof. tauto. Qed.

Lemma zenon_notor : forall P Q : Prop,
  (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
Proof. tauto. Qed.

Lemma zenon_notimply : forall P Q : Prop,
  (P -> ~Q -> False) -> (~(P -> Q) -> False).
Proof. tauto. Qed.

Lemma zenon_notequiv : forall P Q : Prop,
  (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
Proof. tauto. Qed.

Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
  (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
Proof. firstorder. Qed.

Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
  ((P t) -> False) -> ((forall x : T, (P x)) -> False).
Proof. firstorder. Qed.

Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
  (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
Proof. firstorder. Qed.

Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.

Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
Proof. auto. Qed.

Lemma zenon_equal_step :
  forall (S T : Type) (fa fb : S -> T) (a b : S),
  (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.

Lemma zenon_pnotp : forall P Q : Prop,
  (P = Q) -> (P -> ~Q -> False).
Proof. intros P Q Ha. rewrite Ha. auto. Qed.

Lemma zenon_notequal : forall (T : Type) (a b : T),
  (a = b) -> (a <> b -> False).
Proof. auto. Qed.

Ltac zenon_intro id :=
  intro id || let nid := fresh in (intro nid; clear nid)
.

Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.

Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.

(* Ergo *)

Set Implicit Arguments.
Section congr.
  Variable t:Type.
Lemma ergo_eq_concat_1 :
  forall (P:t -> Prop) (x y:t),
    P x -> x = y -> P y.
Proof.
  intros; subst; auto.
Qed.

Lemma ergo_eq_concat_2 :
  forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
    P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
Proof.
  intros; subst; auto.
Qed.

End congr.