more definitions!

Author: Gregory Malecha

theories/Data/Option.v

@@ -1,5 +1,6 @@
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
 Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Reducible.
@@ -67,6 +68,37 @@ Section relation.
     destruct H0; auto.
     inversion H1. constructor; auto. subst. eapply H; eassumption.
   Qed.
+
+  Global Instance Injective_Roption_None
+  : Injective (Roption None None) :=
+    { result := True }.
+  auto.
+  Defined.
+
+  Global Instance Injective_Roption_None_Some a
+  : Injective (Roption None (Some a)) :=
+    { result := False }.
+  inversion 1.
+  Defined.
+
+  Global Instance Injective_Roption_Some_None a
+  : Injective (Roption (Some a) None) :=
+    { result := False }.
+  inversion 1.
+  Defined.
+
+  Global Instance Injective_Roption_Some_Some a b
+  : Injective (Roption (Some a) (Some b)) :=
+    { result := R a b }.
+  inversion 1. auto.
+  Defined.
+
+  Global Instance Injective_Proper_Roption_Some x
+  : Injective (Proper Roption (Some x)) :=
+    { result := R x x }.
+  abstract (inversion 1; assumption).
+  Defined.
+
 End relation.
 
 Section type.

theories/Data/Pair.v

@@ -1,10 +1,36 @@
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.RelationClasses.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Tactics.Injection.
 
 Set Implicit Arguments.
 Set Strict Implicit.
 
+Section Eqpair.
+  Context {T U} (rT : relation T) (rU : relation U).
+
+  Inductive Eqpair : relation (T * U) :=
+  | Eqpair_both : forall a b c d, rT a b -> rU c d -> Eqpair (a,c) (b,d).
+
+  Global Instance Reflexive_Eqpair {RrT : Reflexive rT} {RrU : Reflexive rU}
+  : Reflexive Eqpair.
+  Proof. red. destruct x. constructor; reflexivity. Qed.
+
+  Global Instance Symmetric_Eqpair {RrT : Symmetric rT} {RrU : Symmetric rU}
+  : Symmetric Eqpair.
+  Proof. red. inversion 1; constructor; symmetry; assumption. Qed.
+
+  Global Instance Transitive_Eqpair {RrT : Transitive rT} {RrU : Transitive rU}
+  : Transitive Eqpair.
+  Proof. red. inversion 1; inversion 1; constructor; etransitivity; eauto. Qed.
+
+  Global Instance Injective_Eqpair a b c d : Injective (Eqpair (a,b) (c,d)) :=
+  { result := rT a c /\ rU b d }.
+  abstract (inversion 1; auto).
+  Defined.
+End Eqpair.
+
 Section PairWF.
   Variables T U : Type.
   Variable RT : T -> T -> Prop.

theories/Data/Prop.v

@@ -47,6 +47,25 @@ Proof. intuition. Qed.
 Lemma Or_True_iff : forall P, (P \/ True) <-> True.
 Proof. intuition. Qed.
 
+Lemma Impl_iff
+: forall P Q R S : Prop,
+    (P <-> R) ->
+    (P -> (Q <-> S)) ->
+    ((P -> Q) <-> (R -> S)).
+Proof. clear. intuition. Qed.
+
+Lemma And_iff
+: forall P Q R S : Prop,
+    (P <-> R) ->
+    (P -> (Q <-> S)) ->
+    ((P /\ Q) <-> (R /\ S)).
+Proof. clear; intuition. Qed.
+
+Lemma Impl_True_iff : forall (P : Prop), (True -> P) <-> P.
+Proof.
+  clear; intros; tauto.
+Qed.
+
 (** Forall **)
 Lemma forall_iff : forall T P Q,
                      (forall x,