The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Can you do

Notation foo' e f := (fun st => foo st e f).

and carry around a (foo' e f)?

On Tue, Jul 8, 2014 at 3:05 PM, Durward McDonell <Durward.McDonell AT jhuapl.edu> wrote:

That's not a bad idea, but we really want to carry around
(foo e f) and apply it to a state. But given a fixed state,
we want to be able to switch e' and f' in for e and f when
appropriate.

Thanks for the reply.

--
Durward

On 07/08/2014 04:05 AM, Cedric Auger wrote:
> Maybe you could define a notation to change the order the arguments are
> parsed/printed and in fact use the expected order for "Parametric Morphism".
>
>
> 2014-07-07 20:32 GMT+02:00 Durward McDonell <Durward.McDonell AT jhuapl.edu

> <mailto:Durward.McDonell AT jhuapl.edu>>:

>
>
>     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 <mailto:durward.mcdonell AT jhuapl.edu>
>     240-228-2690 <tel:240-228-2690> (DC)
>     443-778-2690 <tel:443-778-2690> (Balt.)

>
>
>
>
> --
> .../Sedrikov\...


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