Compatibility of iff wrt not and imp.

This completes the series and cannot hurt.

2 files changed, 19 insertions, 1 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index ddaf08bf71..4e3f2e80f3 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 85123cc444..fb1a7ab1c1 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).