1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Logic.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
11
Set Implicit Arguments.
13
Require Import Notations.
15
(** * Propositional connectives *)
17
(** [True] is the always true proposition *)
18
Inductive True : Prop :=
21
(** [False] is the always false proposition *)
22
Inductive False : Prop :=.
24
(** [not A], written [~A], is the negation of [A] *)
25
Definition not (A:Prop) := A -> False.
27
Notation "~ x" := (not x) : type_scope.
29
Hint Unfold not: core.
31
(** [and A B], written [A /\ B], is the conjunction of [A] and [B]
33
[conj p q] is a proof of [A /\ B] as soon as
34
[p] is a proof of [A] and [q] a proof of [B]
36
[proj1] and [proj2] are first and second projections of a conjunction *)
38
Inductive and (A B:Prop) : Prop :=
39
conj : A -> B -> A /\ B
41
where "A /\ B" := (and A B) : type_scope.
47
Theorem proj1 : A /\ B -> A.
52
Theorem proj2 : A /\ B -> B.
59
(** [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
61
Inductive or (A B:Prop) : Prop :=
62
| or_introl : A -> A \/ B
63
| or_intror : B -> A \/ B
65
where "A \/ B" := (or A B) : type_scope.
67
(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
69
Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
71
Notation "A <-> B" := (iff A B) : type_scope.
75
Theorem iff_refl : forall A:Prop, A <-> A.
80
Theorem iff_trans : forall A B C:Prop, (A <-> B) -> (B <-> C) -> (A <-> C).
82
intros A B C [H1 H2] [H3 H4]; split; auto.
85
Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
87
intros A B [H1 H2]; split; auto.
92
Hint Unfold iff: extcore.
94
(** Some equivalences *)
96
Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
98
intro A; unfold not; split.
99
intro H; split; [exact H | intro H1; elim H1].
100
intros [H _]; exact H.
103
Theorem and_cancel_l : forall A B C : Prop,
104
(B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
109
Theorem and_cancel_r : forall A B C : Prop,
110
(B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
115
Theorem or_cancel_l : forall A B C : Prop,
116
(B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
121
Theorem or_cancel_r : forall A B C : Prop,
122
(B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
127
(** Backward direction of the equivalences above does not need assumptions *)
129
Theorem and_iff_compat_l : forall A B C : Prop,
130
(B <-> C) -> (A /\ B <-> A /\ C).
135
Theorem and_iff_compat_r : forall A B C : Prop,
136
(B <-> C) -> (B /\ A <-> C /\ A).
141
Theorem or_iff_compat_l : forall A B C : Prop,
142
(B <-> C) -> (A \/ B <-> A \/ C).
147
Theorem or_iff_compat_r : forall A B C : Prop,
148
(B <-> C) -> (B \/ A <-> C \/ A).
153
Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
155
intros A B []; split; trivial.
158
Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
163
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
164
either [P] and [Q], or [~P] and [Q] *)
166
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
168
Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
169
(at level 200, right associativity) : type_scope.
171
(** * First-order quantifiers *)
173
(** [ex P], or simply [exists x, P x], or also [exists x:A, P x],
174
expresses the existence of an [x] of some type [A] in [Set] which
175
satisfies the predicate [P]. This is existential quantification.
177
[ex2 P Q], or simply [exists2 x, P x & Q x], or also
178
[exists2 x:A, P x & Q x], expresses the existence of an [x] of
179
type [A] which satisfies both predicates [P] and [Q].
181
Universal quantification is primitively written [forall x:A, Q]. By
182
symmetry with existential quantification, the construction [all P]
186
(** Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
187
P x] is in fact equivalent to [ex (fun x => P x)] which may be not
188
convertible to [ex P] if [P] is not itself an abstraction *)
191
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
192
ex_intro : forall x:A, P x -> ex (A:=A) P.
194
Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
195
ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
197
Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
199
(* Rule order is important to give printing priority to fully typed exists *)
201
Notation "'exists' x , p" := (ex (fun x => p))
202
(at level 200, x ident, right associativity) : type_scope.
203
Notation "'exists' x : t , p" := (ex (fun x:t => p))
204
(at level 200, x ident, right associativity,
205
format "'[' 'exists' '/ ' x : t , '/ ' p ']'")
208
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
209
(at level 200, x ident, p at level 200, right associativity) : type_scope.
210
Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
211
(at level 200, x ident, t at level 200, p at level 200, right associativity,
212
format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'")
215
(** Derived rules for universal quantification *)
217
Section universal_quantification.
220
Variable P : A -> Prop.
222
Theorem inst : forall x:A, all (fun x => P x) -> P x.
224
unfold all in |- *; auto.
227
Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P.
232
End universal_quantification.
236
(** [eq x y], or simply [x=y] expresses the equality of [x] and
237
[y]. Both [x] and [y] must belong to the same type [A].
238
The definition is inductive and states the reflexivity of the equality.
239
The others properties (symmetry, transitivity, replacement of
240
equals by equals) are proved below. The type of [x] and [y] can be
241
made explicit using the notation [x = y :> A]. This is Leibniz equality
242
as it expresses that [x] and [y] are equal iff every property on
243
[A] which is true of [x] is also true of [y] *)
245
Inductive eq (A:Type) (x:A) : A -> Prop :=
246
refl_equal : x = x :>A
248
where "x = y :> A" := (@eq A x y) : type_scope.
250
Notation "x = y" := (x = y :>_) : type_scope.
251
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
252
Notation "x <> y" := (x <> y :>_) : type_scope.
254
Implicit Arguments eq_ind [A].
255
Implicit Arguments eq_rec [A].
256
Implicit Arguments eq_rect [A].
258
Hint Resolve I conj or_introl or_intror refl_equal: core.
259
Hint Resolve ex_intro ex_intro2: core.
261
Section Logic_lemmas.
263
Theorem absurd : forall A C:Prop, A -> ~ A -> C.
265
unfold not in |- *; intros A C h1 h2.
270
Variables A B : Type.
274
Theorem sym_eq : x = y -> y = x.
280
Theorem trans_eq : x = y -> y = z -> x = z.
286
Theorem f_equal : x = y -> f x = f y.
292
Theorem sym_not_eq : x <> y -> y <> x.
294
red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
297
Definition sym_equal := sym_eq.
298
Definition sym_not_equal := sym_not_eq.
299
Definition trans_equal := trans_eq.
303
Definition eq_ind_r :
304
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
305
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
308
Definition eq_rec_r :
309
forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
310
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
313
Definition eq_rect_r :
314
forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
315
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
320
forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
321
(x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
323
destruct 1; destruct 1; reflexivity.
327
forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
328
(x2 y2:A2) (x3 y3:A3),
329
x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
331
destruct 1; destruct 1; destruct 1; reflexivity.
335
forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
336
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
337
x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
339
destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
343
forall (A1 A2 A3 A4 A5 B:Type) (f:A1 -> A2 -> A3 -> A4 -> A5 -> B)
344
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4) (x5 y5:A5),
347
x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
349
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
352
Hint Immediate sym_eq sym_not_eq: core.
354
(** Basic definitions about relations and properties *)
356
Definition subrelation (A B : Type) (R R' : A->B->Prop) :=
357
forall x y, R x y -> R' x y.
359
Definition unique (A : Type) (P : A->Prop) (x:A) :=
360
P x /\ forall (x':A), P x' -> x=x'.
362
Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
364
(** Unique existence *)
366
Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
367
(at level 200, x ident, right associativity,
368
format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope.
369
Notation "'exists' ! x : A , P" :=
370
(ex (unique (fun x:A => P)))
371
(at level 200, x ident, right associativity,
372
format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope.
374
Lemma unique_existence : forall (A:Type) (P:A->Prop),
375
((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
378
intros ((x,Hx),Huni); exists x; red; auto.
379
intros (x,(Hx,Huni)); split.
380
exists x; assumption.
381
intros x' x'' Hx' Hx''; transitivity x.
386
(** * Being inhabited *)
388
(** The predicate [inhabited] can be used in different contexts. If [A] is
389
thought as a type, [inhabited A] states that [A] is inhabited. If [A] is
390
thought as a computationally relevant proposition, then
391
[inhabited A] weakens [A] so as to hide its computational meaning.
392
The so-weakened proof remains computationally relevant but only in
393
a propositional context.
396
Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
398
Hint Resolve inhabits: core.
400
Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
401
(exists x, P x) -> inhabited A.
406
(** Declaration of stepl and stepr for eq and iff *)
408
Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
410
intros A x y z H1 H2. rewrite <- H2; exact H1.
413
Declare Left Step eq_stepl.
414
Declare Right Step trans_eq.
416
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
421
Declare Left Step iff_stepl.
422
Declare Right Step iff_trans.
added
removed
theories/Init/Logic.v
