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
|
(***********************************************************************)
(* 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 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}(R:relation B)(f:A->B) : relation A :=
fun a a' => R (f a) (f a').
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 B}(RA:relation A)(RB:relation B) : relation (A*B) :=
relation_conjunction (RA @@1) (RB @@2).
Infix "*" := RelProd : signature_scope.
Section RelCompFun_Instances.
Context {A 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.
Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
`(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
Proof. firstorder. Qed.
Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B)
`(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB).
Proof. firstorder. Qed.
Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B)
`(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
Proof. firstorder. Qed.
Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
`(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
Lemma FstRel_ProdRel {A B}(RA:relation A) :
relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
Proof. firstorder. Qed.
Lemma SndRel_ProdRel {A B}(RB:relation B) :
relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
Proof. firstorder. Qed.
Instance FstRel_sub {A B} (RA:relation A)(RB:relation B):
subrelation (RA*RB) (RA @@1).
Proof. firstorder. Qed.
Instance SndRel_sub {A B} (RA:relation A)(RB:relation B):
subrelation (RA*RB) (RB @@2).
Proof. firstorder. Qed.
Instance pair_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA==>RB==> RA*RB) (@pair _ _).
Proof. firstorder. Qed.
Instance fst_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA*RB ==> RA) Fst.
Proof.
intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
Qed.
Instance snd_compat { A B } (RA:relation A)(RB:relation B) :
Proper (RA*RB ==> RB) Snd.
Proof.
intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
Qed.
Instance RelCompFun_compat {A B}(f:A->B)(R : relation B)
`(Proper _ (Ri==>Ri==>Ro) R) :
Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature.
Proof. unfold RelCompFun; firstorder. Qed.
Hint Unfold RelProd RelCompFun.
Hint Extern 2 (RelProd _ _ _ _) => split.
|
