1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
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)
(x : @sigT A P1) (y : @sigT A P2)
: Prop
:= { pf : projT1 x = projT1 y
| R _ (rew pf in projT2 x) (projT2 y) }.
Definition map_related_sigT_by_eq {A P1 P2} {R1 R2 : forall x : A, P1 x -> P2 x -> Prop}
(HR : forall x v1 v2, R1 x v1 v2 -> R2 x v1 v2)
(x : @sigT A P1) (y : @sigT A P2)
: @related_sigT_by_eq A P1 P2 R1 x y -> @related_sigT_by_eq A P1 P2 R2 x y.
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.
|
