The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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