The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

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 
<megacz AT cs.berkeley.edu>
 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
>
>