Library Coq.Classes.RelationPairs
Any function from A to B allow to obtain a relation over A
out of a relation over B.
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.
Standard measures.
We define a product relation over A*B: each components should
satisfy the corresponding initial relation.