Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Parametric Morphisms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Parametric Morphisms


Chronological Thread 
  • From: Durward McDonell <Durward.McDonell AT jhuapl.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Parametric Morphisms
  • Date: Mon, 07 Jul 2014 14:32:34 -0400


Hello.

Here's what I understand: suppose you have two types, "expr" and
"state". Also suppose you have

eq_expr : state -> expr -> expr -> Prop

and that you Add (eq_expr st) as a reflexive, symmetric, and
transitive Parametric Relation for all (st : state). Finally, suppose
you have

foo : state -> expr -> expr -> Prop

that respects eq_expr on both of its expr arguments. Then you can
do

Add Parametric Morphism (st : state) :
(foo st)
with signature ((eq_expr st) ==> (eq_expr st) ==> impl)
as foo_mor.

Subsequently, if you have

H : foo st e f
G : eq_expr st e e'

you can use "rewrite G in H" to get

H : foo st e' f

So far, so good, I hope. My question is what if, for some perverse
reason, you really, really want foo to be

foo' : expr -> expr -> state -> Prop

that is, you just want to reorder the arguments to foo. What do you do
about the Parametric Morphism statement? I've tried a couple of things
that were either unsatisfactory, or simply didn't work. Any suggestion
would be welcome.

--
Durward McDonell
durward.mcdonell AT jhuapl.edu
240-228-2690 (DC)
443-778-2690 (Balt.)

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature




Archive powered by MHonArc 2.6.18.

Top of Page