Home Reading Searching Subscribe Sponsors Statistics Posting Contact Spam Lists Links About Hosting Filtering Features Download Marketing Archives FAQ Blog From: Bas Spitters cs.ru.nl> Subject: Re: Notation which uses parameters of a Record/Class? Newsgroups: gmane.science.mathematics.logic.coq.club Date: Wednesday 14th April 2010 07:17:54 UTC (over 8 years ago) ```Our solution is to first define an "operational type class" E.g. Class SemiGroupOp A := sg_op: A → A → A. Infix "&" := sg_op (at level 50, left associativity). [ It would be nicer to write: Class SemiGroupOp A := (&) : A → A → A. Like in haskell. ] and then: Context A {e: Equiv A}. Class Setoid: Prop := setoid_eq:> Equivalence (@equiv A e). Class SemiGroup {op: SemiGroupOp A}: Prop := { sg_setoid:> Setoid ; sg_ass:> Associative sg_op ; sg_mor:> Proper (e ==> e ==> e)%signature sg_op }. Class Monoid {op: SemiGroupOp A} {unit: MonoidUnit A}: Prop := { monoid_semigroup:> SemiGroup ; monoid_left_id:> LeftIdentity sg_op mon_unit ; monoid_right_id:> RightIdentity sg_op mon_unit }. Class Group {op: SemiGroupOp A} {unit: MonoidUnit A} {inv: GroupInv A}: Prop := { group_monoid:> Monoid ; inv_proper:> Proper (e ==> e) inv ; ginv_l: `(- x & x = mon_unit) ; ginv_r: `(x & - x = mon_unit) }. This is described in our ITP "rough diamond" which, together with the sources, is available at: http://www.xs4all.nl/~weegen/eelis/research/math-classes/ We are currently working on a fuller version of this paper and the development. Bas On Wed, Apr 14, 2010 at 6:06 AM, Adam Megacz wrote: > > 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 > >```
CD: 12ms