The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Using Notation makes rewriting almost transparent; you may need to [cbv beta] or [cbv beta in *] in a bunch of places.  (You can make a notation (only parsing) if you want to see what you actually end up getting.)  If plain rewriting doesn't work, you can use ltac to make a special variant of rewrite that will pose a lemma as a hypothesis, run [cbv beta in *], rewrite with the hypothesis, and then clear it.

-Jason

On Jul 8, 2014 3:31 PM, "Durward McDonell" <Durward.McDonell AT jhuapl.edu> wrote:

On 07/08/2014 10:18 AM, Jason Gross wrote:
>
> Can you do
>
> Notation foo' e f := (fun st => foo st e f).
>
> and carry around a (foo' e f)?

Yes! That was one of my solutions. It works, but the drawback is
always having to convert between foo and foo' when you want to do
rewrites. Or wait -- you said use Notation, while my solution was
to define foo' as an auxiliary function. Does Notation make rewriting
transparent? In any case, maybe there's a clever way to us ltac for
whatever's needed? I'm not that great with ltac yet.

I'll have to go fiddle with this and see if it does what I want.
Thanks!

--
Durward


> On Tue, Jul 8, 2014 at 3:05 PM, Durward McDonell
> <Durward.McDonell AT jhuapl.edu <mailto: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>
>     > <mailto: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>
>     <mailto:durward.mcdonell AT jhuapl.edu
>     <mailto:durward.mcdonell AT jhuapl.edu>>
>     >     240-228-2690 <tel:240-228-2690> <tel:240-228-2690
>     <tel:240-228-2690>> (DC)
>     >     443-778-2690 <tel:443-778-2690> <tel:443-778-2690
>     <tel:443-778-2690>> (Balt.)
>     >
>     >
>     >
>     >
>     > --
>     > .../Sedrikov\...
>
>
>     --
>     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.)
>
>


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