The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Le Wed, 14 Apr 2010 04:06:45 +0000,
Adam Megacz 
<megacz AT cs.berkeley.edu>
 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.
   *)