Add related_sigT_by_eq proper lemmas

1 files changed, 65 insertions, 0 deletions

diff --git a/src/Util/Sigma/Related.v b/src/Util/Sigma/Related.v
index ac98f7629..bc3bacb90 100644
--- a/src/Util/Sigma/Related.v
+++ b/src/Util/Sigma/Related.v
@@ -1,3 +1,6 @@
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
 Import EqNotations.
 
 Definition related_sigT_by_eq {A P1 P2} (R : forall x : A, P1 x -> P2 x -> Prop)
@@ -14,3 +17,65 @@ Proof using Type.
   destruct x, y; cbv [related_sigT_by_eq projT1 projT2].
   intro H; exists (proj1_sig H); apply HR, (proj2_sig H).
 Qed.
+
+Global Instance related_sigT_by_eq_Reflexive {A P}
+       {R : forall x : A, relation (P x)}
+       {R_Reflexive : forall x : A, Reflexive (R x)}
+  : Reflexive (@related_sigT_by_eq A P P R) | 10.
+Proof.
+  cbv [related_sigT_by_eq Reflexive projT1 projT2]; intros [? ?].
+  exists eq_refl; cbn; reflexivity.
+Qed.
+
+Lemma related_sigT_by_eq_sym_gen {A P1 P2 R1 R2 x y}
+      (HR : forall x X Y, (R1 x X Y : Prop) -> (R2 x Y X : Prop))
+  : @related_sigT_by_eq A P1 P2 R1 x y
+    -> @related_sigT_by_eq A P2 P1 R2 y x.
+Proof.
+  destruct x, y; cbv [related_sigT_by_eq projT1 projT2].
+  intros [? H]; subst; exists eq_refl; cbn in *.
+  apply HR; assumption.
+Qed.
+
+Lemma related_sigT_by_eq_sym_flip_iff {A P1 P2 R x y}
+  : @related_sigT_by_eq A P1 P2 R x y
+    <-> @related_sigT_by_eq A P2 P1 (fun x => Basics.flip (R x)) y x.
+Proof.
+  split; apply related_sigT_by_eq_sym_gen; cbv [Basics.flip]; trivial.
+Qed.
+
+Lemma related_sigT_by_eq_sym_iff {A P R x y}
+      (R_sym : forall x, Symmetric (R x))
+  : @related_sigT_by_eq A P P R x y
+    <-> @related_sigT_by_eq A P P R y x.
+Proof.
+  split; apply related_sigT_by_eq_sym_gen; trivial.
+Qed.
+
+Global Instance related_sigT_by_eq_Symmetric {A P R}
+       {R_Symmetric : forall x, Symmetric (R x)}
+  : Symmetric (@related_sigT_by_eq A P P R) | 10
+  := fun x y => proj1 (related_sigT_by_eq_sym_iff _).
+
+Lemma related_sigT_by_eq_trans {A P1 P2 P3 R1 R2 R3 x y z}
+      (R_trans : forall a x y z, (R1 a x y : Prop) -> (R2 a y z : Prop) -> (R3 a x z : Prop))
+  : @related_sigT_by_eq A P1 P2 R1 x y
+    -> @related_sigT_by_eq A P2 P3 R2 y z
+    -> @related_sigT_by_eq A P1 P3 R3 x z.
+Proof.
+  destruct x, y, z; cbv [related_sigT_by_eq projT1 projT2];
+    intros [? ?] [? ?]; subst; exists eq_refl; cbn in *.
+  eauto.
+Qed.
+
+Global Instance related_sigT_by_eq_Transitive {A P R}
+       {R_Transitive : forall x : A, Transitive (R x)}
+  : Transitive (@related_sigT_by_eq A P P R) | 10
+  := fun x y z => related_sigT_by_eq_trans R_Transitive.
+
+Global Instance existT_Proper_related_sigT_by_eq {A P R x}
+  : Proper (R x ==> @related_sigT_by_eq A P P R) (@existT A P x) | 10.
+Proof.
+  cbv [Proper respectful related_sigT_by_eq projT1 projT2].
+  exists eq_refl; assumption.
+Qed.