Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Bas Spitters <spitters <at> 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 7 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: 4ms