Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: AUGER =?ISO-8859-1?B?Q+lkcmlj?= <Cedric.Auger <at> lri.fr>
Subject: Re: Notation which uses parameters of a Record/Class?
Newsgroups: gmane.science.mathematics.logic.coq.club
Date: Wednesday 14th April 2010 07:14:01 UTC (over 7 years ago)
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.
   *)
 
CD: 3ms