The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Dear Michael,

Not entirely sure whether this is related to your question, but we
developed some setoid based universal algebra in math-classes.
One of the things we prove is that nat is the initial (commutative) semiring.
Our development of universal algebra includes the syntax of a semiring
in the way you describe it.

Type Classes for Mathematics in Type Theory (with Eelis van der Weegen).
http://dx.doi.org/10.1017/S0960129511000119

Best regards,

Bas

On Tue, May 8, 2018 at 7:07 PM, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 wrote:
> Dear Matthieu,
>
>
>
> may I ask a question: what if I don’t have an isomorphism but just a
> homomorphism. To give a concrete example think of nat and an inductive type
> encoding expressions on nat (including variables). I found it very helpful
> to declare typeclass instance like:
>
>
>
> Instance Equivalence_equiv : Equivalence equiv.
>
> Instance Proper_Const : Proper (eq ==> equiv) Const.
>
> Instance Proper_Var : Proper (eq ==> equiv) Var.
>
> Instance Proper_Add : Proper (equiv ==> equiv ==> equiv) Add.
>
> Instance Proper_Mul : Proper (equiv ==> equiv ==> equiv) Mul.
>
> Instance Proper_eval : Proper (state_equiv ==> equiv ==> eq) eval.
>
>
>
> Where equiv is the equivalence of expressions, eval is the evaluation
> function (first argument is the state) and Const Var Add and Mul are
> constructors of the expression type.
>
>
>
> I wonder what it would take to e.g. lift the commutative law for natural
> numbers to expressions such that I can use it with e.g. setoid rewrite to
> swap the arguments of Add? Can I somehow define that + on nat and Add for
> expressions are equivalent operators under the eval transformation?
>
>
>
> Best regards,
>
>
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928