diff options
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r-- | theories/Init/Logic.v | 232 |
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. |