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 |
|||