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.v232
1 files changed, 181 insertions, 51 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index e5f7a78b..d2971552 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,17 +8,23 @@
Set Implicit Arguments.
-Require Import Notations.
+Require Export Notations.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
(** * Propositional connectives *)
(** [True] is the always true proposition *)
+
Inductive True : Prop :=
I : True.
(** [False] is the always false proposition *)
Inductive False : Prop :=.
+(** [proof_admitted] is used to implement the admit tactic *)
+Axiom proof_admitted : False.
+
(** [not A], written [~A], is the negation of [A] *)
Definition not (A:Prop) := A -> False.
@@ -92,6 +98,36 @@ End Equivalence.
Hint Unfold iff: extcore.
+(** Backward direction of the equivalences above does not need assumptions *)
+
+Theorem and_iff_compat_l : forall A B C : Prop,
+ (B <-> C) -> (A /\ B <-> A /\ C).
+Proof.
+ intros ? ? ? [Hl Hr]; split; intros [? ?]; (split; [ assumption | ]);
+ [apply Hl | apply Hr]; assumption.
+Qed.
+
+Theorem and_iff_compat_r : forall A B C : Prop,
+ (B <-> C) -> (B /\ A <-> C /\ A).
+Proof.
+ intros ? ? ? [Hl Hr]; split; intros [? ?]; (split; [ | assumption ]);
+ [apply Hl | apply Hr]; assumption.
+Qed.
+
+Theorem or_iff_compat_l : forall A B C : Prop,
+ (B <-> C) -> (A \/ B <-> A \/ C).
+Proof.
+ intros ? ? ? [Hl Hr]; split; (intros [?|?]; [left; assumption| right]);
+ [apply Hl | apply Hr]; assumption.
+Qed.
+
+Theorem or_iff_compat_r : forall A B C : Prop,
+ (B <-> C) -> (B \/ A <-> C \/ A).
+Proof.
+ intros ? ? ? [Hl Hr]; split; (intros [?|?]; [left| right; assumption]);
+ [apply Hl | apply Hr]; assumption.
+Qed.
+
(** Some equivalences *)
Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
@@ -104,73 +140,62 @@ Qed.
Theorem and_cancel_l : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
Proof.
- intros; tauto.
+ intros A B C Hl Hr.
+ split; [ | apply and_iff_compat_l]; intros [HypL HypR]; split; intros.
+ + apply HypL; split; [apply Hl | ]; assumption.
+ + apply HypR; split; [apply Hr | ]; assumption.
Qed.
Theorem and_cancel_r : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
Proof.
- intros; tauto.
+ intros A B C Hl Hr.
+ split; [ | apply and_iff_compat_r]; intros [HypL HypR]; split; intros.
+ + apply HypL; split; [ | apply Hl ]; assumption.
+ + apply HypR; split; [ | apply Hr ]; assumption.
Qed.
Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
Proof.
- intros; tauto.
+ intros; split; intros [? ?]; split; assumption.
Qed.
Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C.
Proof.
- intros; tauto.
+ intros; split; [ intros [[? ?] ?]| intros [? [? ?]]]; repeat split; assumption.
Qed.
Theorem or_cancel_l : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
Proof.
- intros; tauto.
+ intros ? ? ? Fl Fr; split; [ | apply or_iff_compat_l]; intros [Hl Hr]; split; intros.
+ { destruct Hl; [ right | destruct Fl | ]; assumption. }
+ { destruct Hr; [ right | destruct Fr | ]; assumption. }
Qed.
Theorem or_cancel_r : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
Proof.
- intros; tauto.
+ intros ? ? ? Fl Fr; split; [ | apply or_iff_compat_r]; intros [Hl Hr]; split; intros.
+ { destruct Hl; [ left | | destruct Fl ]; assumption. }
+ { destruct Hr; [ left | | destruct Fr ]; assumption. }
Qed.
Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
Proof.
- intros; tauto.
+ intros; split; (intros [? | ?]; [ right | left ]; assumption).
Qed.
Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
Proof.
- intros; tauto.
-Qed.
-
-(** Backward direction of the equivalences above does not need assumptions *)
-
-Theorem and_iff_compat_l : forall A B C : Prop,
- (B <-> C) -> (A /\ B <-> A /\ C).
-Proof.
- intros; tauto.
-Qed.
-
-Theorem and_iff_compat_r : forall A B C : Prop,
- (B <-> C) -> (B /\ A <-> C /\ A).
-Proof.
- intros; tauto.
-Qed.
-
-Theorem or_iff_compat_l : forall A B C : Prop,
- (B <-> C) -> (A \/ B <-> A \/ C).
-Proof.
- intros; tauto.
-Qed.
-
-Theorem or_iff_compat_r : forall A B C : Prop,
- (B <-> C) -> (B \/ A <-> C \/ A).
-Proof.
- intros; tauto.
+ intros; split; [ intros [[?|?]|?]| intros [?|[?|?]]].
+ + left; assumption.
+ + right; left; assumption.
+ + right; right; assumption.
+ + left; left; assumption.
+ + left; right; assumption.
+ + right; assumption.
Qed.
-
Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
Proof.
intros A B []; split; trivial.
@@ -178,7 +203,7 @@ Qed.
Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
Proof.
- intros; tauto.
+ intros; split; intros [Hl Hr]; (split; intros; [ apply Hl | apply Hr]); assumption.
Qed.
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
@@ -204,11 +229,6 @@ 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,
- 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.
@@ -277,7 +297,8 @@ 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 I conj or_introl or_intror : core.
+Hint Resolve eq_refl: core.
Hint Resolve ex_intro ex_intro2: core.
Section Logic_lemmas.
@@ -297,19 +318,16 @@ Section Logic_lemmas.
Proof.
destruct 1; trivial.
Defined.
- Opaque eq_sym.
Theorem eq_trans : x = y -> y = z -> x = z.
Proof.
destruct 2; trivial.
Defined.
- Opaque eq_trans.
Theorem f_equal : x = y -> f x = f y.
Proof.
destruct 1; trivial.
Defined.
- Opaque f_equal.
Theorem not_eq_sym : x <> y -> y <> x.
Proof.
@@ -320,7 +338,7 @@ 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 eq_sym with (1 := H0); assumption.
+ intros A x P H y H0. elim eq_sym with (1 := H0); assumption.
Defined.
Definition eq_rec_r :
@@ -336,13 +354,40 @@ End Logic_lemmas.
Module EqNotations.
Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
- (at level 10, H' at level 10).
+ (at level 10, H' at level 10,
+ format "'[' 'rew' H in '/' H' ']'").
+ Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+ (at level 10, H' at level 10,
+ format "'[' 'rew' [ P ] '/ ' H in '/' H' ']'").
Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
- (at level 10, H' at level 10).
+ (at level 10, H' at level 10,
+ format "'[' 'rew' <- H in '/' H' ']'").
+ Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H)
+ (at level 10, H' at level 10,
+ format "'[' 'rew' <- [ P ] '/ ' H in '/' H' ']'").
Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
(at level 10, H' at level 10, only parsing).
+ Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+ (at level 10, H' at level 10, only parsing).
+
End EqNotations.
+Import EqNotations.
+
+Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
+Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
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.
@@ -376,6 +421,91 @@ Proof.
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
+Theorem f_equal_compose : forall A B C (a b:A) (f:A->B) (g:B->C) (e:a=b),
+ f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e.
+Proof.
+ destruct e. reflexivity.
+Defined.
+
+(** The goupoid structure of equality *)
+
+Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e.
+Proof.
+ destruct e. reflexivity.
+Defined.
+
+Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e.
+Proof.
+ destruct e. reflexivity.
+Defined.
+
+Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e.
+Proof.
+ destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl.
+Proof.
+ destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl.
+Proof.
+ destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_assoc : forall A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t),
+ eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''.
+Proof.
+ destruct e''; reflexivity.
+Defined.
+
+(** Extra properties of equality *)
+
+Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a).
+Proof.
+ intros.
+ unfold f_equal.
+ rewrite <- (eq_trans_sym_inv_l (Hf a)).
+ destruct (Hf a) at 1 2.
+ destruct (Hf a).
+ reflexivity.
+Defined.
+
+Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a).
+Proof.
+ intros.
+ unfold f_equal.
+ rewrite <- (eq_trans_sym_inv_l (Hf (f (f a)))).
+ set (Hfsymf := fun a => eq_sym (Hf a)).
+ change (eq_sym (Hf (f (f a)))) with (Hfsymf (f (f a))).
+ pattern (Hfsymf (f (f a))).
+ destruct (eq_id_comm_l f Hfsymf (f a)).
+ destruct (eq_id_comm_l f Hfsymf a).
+ unfold Hfsymf.
+ destruct (Hf a). simpl.
+ rewrite eq_trans_refl_l.
+ reflexivity.
+Defined.
+
+Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e').
+Proof.
+destruct e'.
+reflexivity.
+Defined.
+
+Lemma eq_sym_map_distr : forall A B (x y:A) (f:A->B) (e:x=y), eq_sym (f_equal f e) = f_equal f (eq_sym e).
+Proof.
+destruct e.
+reflexivity.
+Defined.
+
+Lemma eq_trans_sym_distr : forall A (x y z:A) (e:x=y) (e':y=z), eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e).
+Proof.
+destruct e, e'.
+reflexivity.
+Defined.
+
(* Aliases *)
Notation sym_eq := eq_sym (compat "8.3").
@@ -474,7 +604,7 @@ Declare Right Step eq_trans.
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
Proof.
- intros; tauto.
+ intros ? ? ? [? ?] [? ?]; split; intros; auto.
Qed.
Declare Left Step iff_stepl.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 01:56:24 +0000