summaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r--theories/Init/Logic.v92
1 files changed, 48 insertions, 44 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 71583718..8b487432 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,17 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic.v 8936 2006-06-09 15:43:33Z herbelin $ i*)
+(*i $Id: Logic.v 9245 2006-10-17 12:53:34Z notin $ i*)
Set Implicit Arguments.
Require Import Notations.
-(** *** Propositional connectives *)
+(** * Propositional connectives *)
(** [True] is the always true proposition *)
Inductive True : Prop :=
- I : True.
+ I : True.
(** [False] is the always false proposition *)
Inductive False : Prop :=.
@@ -36,8 +36,8 @@ Hint Unfold not: core.
[proj1] and [proj2] are first and second projections of a conjunction *)
Inductive and (A B:Prop) : Prop :=
- conj : A -> B -> A /\ B
-
+ conj : A -> B -> A /\ B
+
where "A /\ B" := (and A B) : type_scope.
Section Conjunction.
@@ -46,12 +46,12 @@ Section Conjunction.
Theorem proj1 : A /\ B -> A.
Proof.
- destruct 1; trivial.
+ destruct 1; trivial.
Qed.
Theorem proj2 : A /\ B -> B.
Proof.
- destruct 1; trivial.
+ destruct 1; trivial.
Qed.
End Conjunction.
@@ -97,7 +97,7 @@ Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
(at level 200, right associativity) : type_scope.
-(** *** First-order quantifiers *)
+(** * First-order quantifiers *)
(** [ex P], or simply [exists x, P x], or also [exists x:A, P x],
expresses the existence of an [x] of some type [A] in [Set] which
@@ -112,16 +112,16 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
is provided too.
*)
-(* Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
+(** Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
P x] is in fact equivalent to [ex (fun x => P x)] which may be not
convertible to [ex P] if [P] is not itself an abstraction *)
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
- ex_intro : forall x:A, P x -> ex (A:=A) P.
+ ex_intro : forall x:A, P x -> ex (A:=A) P.
Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
- ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
+ ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
@@ -131,14 +131,14 @@ Notation "'exists' x , p" := (ex (fun x => p))
(at level 200, x ident, right associativity) : type_scope.
Notation "'exists' x : t , p" := (ex (fun x:t => p))
(at level 200, x ident, right associativity,
- format "'[' 'exists' '/ ' x : t , '/ ' p ']'")
+ format "'[' 'exists' '/ ' x : t , '/ ' p ']'")
: type_scope.
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
(at level 200, x ident, p at level 200, right associativity) : type_scope.
Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
(at level 200, x ident, t at level 200, p at level 200, right associativity,
- format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'")
+ format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
(** Derived rules for universal quantification *)
@@ -150,17 +150,17 @@ Section universal_quantification.
Theorem inst : forall x:A, all (fun x => P x) -> P x.
Proof.
- unfold all in |- *; auto.
+ unfold all in |- *; auto.
Qed.
Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P.
Proof.
- red in |- *; auto.
+ red in |- *; auto.
Qed.
End universal_quantification.
-(** *** Equality *)
+(** * Equality *)
(** [eq x y], or simply [x=y] expresses the equality of [x] and
[y]. Both [x] and [y] must belong to the same type [A].
@@ -202,27 +202,27 @@ Section Logic_lemmas.
Theorem sym_eq : x = y -> y = x.
Proof.
- destruct 1; trivial.
+ destruct 1; trivial.
Defined.
Opaque sym_eq.
Theorem trans_eq : x = y -> y = z -> x = z.
Proof.
- destruct 2; trivial.
+ destruct 2; trivial.
Defined.
Opaque trans_eq.
Theorem f_equal : x = y -> f x = f y.
Proof.
- destruct 1; trivial.
+ destruct 1; trivial.
Defined.
Opaque f_equal.
Theorem sym_not_eq : x <> y -> y <> x.
Proof.
- red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
+ red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
Qed.
-
+
Definition sym_equal := sym_eq.
Definition sym_not_equal := sym_not_eq.
Definition trans_equal := trans_eq.
@@ -231,14 +231,14 @@ Section Logic_lemmas.
Definition eq_ind_r :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
- intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+ intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
Defined.
-
+
Definition eq_rec_r :
forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
Defined.
-
+
Definition eq_rect_r :
forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
@@ -246,34 +246,34 @@ Section Logic_lemmas.
End Logic_lemmas.
Theorem f_equal2 :
- forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
- (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
+ forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
+ (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
Proof.
destruct 1; destruct 1; reflexivity.
Qed.
Theorem f_equal3 :
- forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
- (x2 y2:A2) (x3 y3:A3),
- x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
+ forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
+ (x2 y2:A2) (x3 y3:A3),
+ x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
Proof.
destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
Theorem f_equal4 :
- forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
- (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
- x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
+ forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
+ (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
+ x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
Proof.
destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
Theorem f_equal5 :
- forall (A1 A2 A3 A4 A5 B:Type) (f:A1 -> A2 -> A3 -> A4 -> A5 -> B)
- (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4) (x5 y5:A5),
- x1 = y1 ->
- x2 = y2 ->
- x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
+ forall (A1 A2 A3 A4 A5 B:Type) (f:A1 -> A2 -> A3 -> A4 -> A5 -> B)
+ (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4) (x5 y5:A5),
+ x1 = y1 ->
+ x2 = y2 ->
+ x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
Proof.
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
@@ -294,22 +294,26 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
(at level 200, x ident, right associativity,
- format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope.
+ format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope.
Notation "'exists' ! x : A , P" :=
(ex (unique (fun x:A => P)))
(at level 200, x ident, right associativity,
- format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope.
+ format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope.
Lemma unique_existence : forall (A:Type) (P:A->Prop),
((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
Proof.
-intros A P; split.
+ intros A P; split.
intros ((x,Hx),Huni); exists x; red; auto.
intros (x,(Hx,Huni)); split.
- exists x; assumption.
- intros x' x'' Hx' Hx''; transitivity x.
- symmetry; auto.
- auto.
+ exists x; assumption.
+ intros x' x'' Hx' Hx''; transitivity x.
+ symmetry; auto.
+ auto.
Qed.
+(** Being inhabited *)
+
+Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
+Hint Resolve inhabits: core.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 10:12:28 +0000