diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-13 22:12:35 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-03 09:51:33 +0100 |
commit | d8f42feb4f4e6c4e062678e256499e03454c7ab2 (patch) | |
tree | 66049d9a8dbe72a01132d4c6ecdd66ad5d2a6f1d /theories/Init | |
parent | 1682d4ed9df64937dfaa162e58233020036ff7b3 (diff) |
Compatibility of iff wrt not and imp.
This completes the series and cannot hurt.
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Datatypes.v | 1 | ||||
-rw-r--r-- | theories/Init/Logic.v | 19 |
2 files changed, 19 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ddaf08bf7..4e3f2e80f 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -326,7 +326,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. Proof. intros. apply CompareSpec2Type; assumption. Defined. - (******************************************************************) (** * Misc Other Datatypes *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc44..fb1a7ab1c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -125,6 +125,25 @@ Proof. [apply Hl | apply Hr]; assumption. Qed. +Theorem imp_iff_compat_l : forall A B C : Prop, + (B <-> C) -> ((A -> B) <-> (A -> C)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption. +Qed. + +Theorem imp_iff_compat_r : forall A B C : Prop, + (B <-> C) -> ((B -> A) <-> (C -> A)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption. +Qed. + +Theorem not_iff_compat : forall A B : Prop, + (A <-> B) -> (~ A <-> ~B). +Proof. + intros; apply imp_iff_compat_r; assumption. +Qed. + + (** Some equivalences *) Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). |