Le Wed, 14 Apr 2010 04:06:45 +0000,
Adam Megacz a écrit :
>
> Is there any way to have a [Notation] whose definition involves
> parameters of the Record/Class currently being defined?
>
> Example:
>
> Class Monoid (Carrier:Set)(mult:Carrier>Carrier>Carrier) :=
> { neutral : Carrier
> ; identL : forall a, (mult a neutral) = a
> ; identR : forall a, (mult neutral a) = a
> ; assoc : forall a b c, (mult a (mult b c)) = (mult (mult a b) c)
> }.
>
> I would much rather write this (especially for classes which are more
> complicated than a simple Monoid), but Coq won't accept it:
>
> Reserved Notation "a ** b" (at level 50).
> Class Monoid (Carrier:Set)(mult:Carrier>Carrier>Carrier) :=
> { neutral : Carrier
> ; identL : forall a, a**neutral = a
> ; identR : forall a, neutral**a = a
> ; assoc : forall a b c, a**(b**c) = (a**b)**c
> } where "a ** b" := (mult a b).
>
> I tried putting the 'where "a ** b" := (mult a b)' in a few other
> places to no avail. Unfortunately due to other constraints I can't
> just add a new field and a notation for it, like this:
>
> Class Monoid (Carrier:Set)(mult:Carrier>Carrier>Carrier) :=
> { mult_again := mult where "a ** b" := (mult_again a b)
> ...
> }
>
> By the way, the definition above is technically illegal according to
> the Coq manual (you're not supposed to be able to put "where" after a
> ":=" clause according to a strict reading of the BNF) but Coq 8.2pl3
> accepts it anyways. Not sure if the BNF should be more permissive or
> Coq should be stricter.
>
> Thanks,
>
>  a
>
I think, this is half satisfactory...
Reserved Notation "a ** b" (at level 50).
Section Monoid.
Variable Carrier: Set.
Variable mult_monoid: Carrier > Carrier > Carrier.
(* The trick is to put mult_monoid at toplevel,
* as you did with your mult_again, but without
* the need to redefine it
*)
Notation "a ** b" := (mult_monoid a b).
Class Monoid :=
{ neutral : Carrier
; identL : forall a, (a ** neutral) = a
; identR : forall a, (neutral ** a) = a
; assoc : forall a b c, (a ** (b ** c)) = ((a ** b) ** c)
}.
End Monoid.
(* At end of the section all variables are generalized,
* as you whish, but Notation die with it.
* The result is that you have been able to use Notation
* to define Monoids, but you won't use them later.
* Note, that you weren't forced to reserve a Notation,
* but as you will probably redefine it later,
* you won't have to define level each time.
*)
Print Monoid.
(* You can see, you lose your Notation.
*)
