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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(** * Relations over pairs *)
Require Import SetoidList.
Require Import Relations Morphisms.
(* NB: This should be system-wide someday, but for that we need to
fix the simpl tactic, since "simpl fst" would be refused for
the moment.
Arguments fst {A B}.
Arguments snd {A B}.
Arguments pair {A B}.
/NB *)
Local Notation Fst := (@fst _ _).
Local Notation Snd := (@snd _ _).
Arguments relation_conjunction A%type (R R')%signature _ _.
Arguments relation_equivalence A%type (_ _)%signature.
Arguments subrelation A%type (R R')%signature.
Arguments Reflexive A%type R%signature.
Arguments Irreflexive A%type R%signature.
Arguments Symmetric A%type R%signature.
Arguments Transitive A%type R%signature.
Arguments PER A%type R%signature.
Arguments Equivalence A%type R%signature.
Arguments StrictOrder A%type R%signature.
Generalizable Variables A B RA RB Ri Ro f.
(** Any function from [A] to [B] allow to obtain a relation over [A]
out of a relation over [B]. *)
Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A :=
fun a a' => R (f a) (f a').
(** Instances on RelCompFun must match syntactically *)
Typeclasses Opaque RelCompFun.
Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope.
Notation "R @@2" := (R @@ Snd)%signature (at level 30) : signature_scope.
(** We declare measures to the system using the [Measure] class.
Otherwise the instances would easily introduce loops,
never instantiating the [f] function. *)
Class Measure {A B} (f : A -> B).
(** Standard measures. *)
Instance fst_measure : @Measure (A * B) A Fst.
Instance snd_measure : @Measure (A * B) B Snd.
(** We define a product relation over [A*B]: each components should
satisfy the corresponding initial relation. *)
Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
Typeclasses Opaque RelProd.
Infix "*" := RelProd : signature_scope.
Section RelCompFun_Instances.
Context {A : Type} {B : Type} (R : relation B).
Global Instance RelCompFun_Reflexive
`(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
Proof. firstorder. Qed.
Global Instance RelCompFun_Symmetric
`(Measure A B f, Symmetric _ R) : Symmetric (R@@f).
Proof. firstorder. Qed.
Global Instance RelCompFun_Transitive
`(Measure A B f, Transitive _ R) : Transitive (R@@f).
Proof. firstorder. Qed.
Global Instance RelCompFun_Irreflexive
`(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
Proof. firstorder. Qed.
Global Program Instance RelCompFun_Equivalence
`(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
Global Program Instance RelCompFun_StrictOrder
`(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
End RelCompFun_Instances.
Section RelProd_Instances.
Context {A : Type} {B : Type} (RA : relation A) (RB : relation B).
Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
Proof. firstorder. Qed.
Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB)
: Symmetric (RA*RB).
Proof. firstorder. Qed.
Global Instance RelProd_Transitive
`(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
Proof. firstorder. Qed.
Global Program Instance RelProd_Equivalence
`(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
Lemma FstRel_ProdRel :
relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
Proof. firstorder. Qed.
Lemma SndRel_ProdRel :
relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
Proof. firstorder. Qed.
Global Instance FstRel_sub :
subrelation (RA*RB) (RA @@1).
Proof. firstorder. Qed.
Global Instance SndRel_sub :
subrelation (RA*RB) (RB @@2).
Proof. firstorder. Qed.
Global Instance pair_compat :
Proper (RA==>RB==> RA*RB) (@pair _ _).
Proof. firstorder. Qed.
Global Instance fst_compat :
Proper (RA*RB ==> RA) Fst.
Proof.
intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
Qed.
Global Instance snd_compat :
Proper (RA*RB ==> RB) Snd.
Proof.
intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
Qed.
Global Instance RelCompFun_compat (f:A->B)
`(Proper _ (Ri==>Ri==>Ro) RB) :
Proper (Ri@@f==>Ri@@f==>Ro) (RB@@f)%signature.
Proof. unfold RelCompFun; firstorder. Qed.
End RelProd_Instances.
Hint Unfold RelProd RelCompFun.
Hint Extern 2 (RelProd _ _ _ _) => split.
|
