Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Parametric Morphisms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Parametric Morphisms


Chronological Thread 
  • From: Durward McDonell <Durward.McDonell AT jhuapl.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Parametric Morphisms
  • Date: Tue, 08 Jul 2014 10:33:06 -0400

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.)

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




Archive powered by MHonArc 2.6.18.

Top of Page