Library Coq.Classes.RelationPairs
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').
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.
Standard measures.
We define a product relation over A*B: each components should
satisfy the corresponding initial relation.