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.v118
1 files changed, 74 insertions, 44 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b95d78a4..d1eabcab 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Set Implicit Arguments.
Require Import Notations.
@@ -64,6 +62,9 @@ Inductive or (A B:Prop) : Prop :=
where "A \/ B" := (or A B) : type_scope.
+Arguments or_introl [A B] _, [A] B _.
+Arguments or_intror [A B] _, A [B] _.
+
(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
@@ -95,53 +96,53 @@ Hint Unfold iff: extcore.
Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
Proof.
-intro A; unfold not; split.
-intro H; split; [exact H | intro H1; elim H1].
-intros [H _]; exact H.
+ intro A; unfold not; split.
+ - intro H; split; [exact H | intro H1; elim H1].
+ - intros [H _]; exact H.
Qed.
Theorem and_cancel_l : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem and_cancel_r : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C.
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_cancel_l : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_cancel_r : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
(** Backward direction of the equivalences above does not need assumptions *)
@@ -149,35 +150,35 @@ Qed.
Theorem and_iff_compat_l : forall A B C : Prop,
(B <-> C) -> (A /\ B <-> A /\ C).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem and_iff_compat_r : forall A B C : Prop,
(B <-> C) -> (B /\ A <-> C /\ A).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_iff_compat_l : forall A B C : Prop,
(B <-> C) -> (A \/ B <-> A \/ C).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Theorem or_iff_compat_r : forall A B C : Prop,
(B <-> C) -> (B \/ A <-> C \/ A).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
Proof.
-intros A B []; split; trivial.
+ intros A B []; split; trivial.
Qed.
Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
@@ -218,11 +219,9 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
(* Rule order is important to give printing priority to fully typed exists *)
-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 ']'")
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+ (at level 200, x binder, right associativity,
+ format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
@@ -271,11 +270,12 @@ Notation "x = y" := (x = y :>_) : type_scope.
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
Notation "x <> y" := (x <> y :>_) : type_scope.
-Implicit Arguments eq [ [A] ].
+Arguments eq {A} x _.
+Arguments eq_refl {A x} , [A] x.
-Implicit Arguments eq_ind [A].
-Implicit Arguments eq_rec [A].
-Implicit Arguments eq_rect [A].
+Arguments eq_ind [A] x P _ y _.
+Arguments eq_rec [A] x P _ y _.
+Arguments eq_rect [A] x P _ y _.
Hint Resolve I conj or_introl or_intror eq_refl: core.
Hint Resolve ex_intro ex_intro2: core.
@@ -334,6 +334,15 @@ Section Logic_lemmas.
Defined.
End Logic_lemmas.
+Module EqNotations.
+ Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
+ (at level 10, H' at level 10).
+ Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
+ (at level 10, H' at level 10).
+ Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
+ (at level 10, H' at level 10, only parsing).
+End EqNotations.
+
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.
@@ -392,26 +401,47 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
(** Unique existence *)
-Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
- (at level 200, x ident, right associativity,
- 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.
+Notation "'exists' ! x .. y , p" :=
+ (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
+ (at level 200, x binder, right associativity,
+ format "'[' 'exists' ! '/ ' x .. y , '/ ' 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 ((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.
+ - 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.
Qed.
+Lemma forall_exists_unique_domain_coincide :
+ forall A (P:A->Prop), (exists! x, P x) ->
+ forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x).
+Proof.
+ intros A P (x & Hp & Huniq); split.
+ - intro; exists x; auto.
+ - intros (x0 & HPx0 & HQx0) x1 HPx1.
+ replace x1 with x0 by (transitivity x; [symmetry|]; auto).
+ assumption.
+Qed.
+
+Lemma forall_exists_coincide_unique_domain :
+ forall A (P:A->Prop),
+ (forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x))
+ -> (exists! x, P x).
+Proof.
+ intros A P H.
+ destruct H with (Q:=P) as ((x & Hx & _),_); [trivial|].
+ exists x. split; [trivial|].
+ destruct H with (Q:=fun x'=>x=x') as (_,Huniq).
+ apply Huniq. exists x; auto.
+Qed.
+
(** * Being inhabited *)
(** The predicate [inhabited] can be used in different contexts. If [A] is
@@ -436,7 +466,7 @@ Qed.
Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
Proof.
-intros A x y z H1 H2. rewrite <- H2; exact H1.
+ intros A x y z H1 H2. rewrite <- H2; exact H1.
Qed.
Declare Left Step eq_stepl.
@@ -444,7 +474,7 @@ Declare Right Step eq_trans.
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
Proof.
-intros; tauto.
+ intros; tauto.
Qed.
Declare Left Step iff_stepl.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 05:08:34 +0000