The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  You might be interested in Equivalences for free!

https://hal.inria.fr/hal-01559073

  We study how ideas inspired by homotopy type theory and parametricity can be used to automate transport of definitions and proofs between equivalent structures, e.g nat and N « after the fact », i.e without relying as much on an abstraction mechanism like modules or records. 

  There is also the CoqEAL library which allows more general development by refinement where the structures involved might not be isomorphic.

Best,
— Matthieu

Le lun. 7 mai 2018 à 21:08, James Lottes <jlottes AT gmail.com> a écrit :

Inductive types are initial algebras, and the definition of initial algebra works as an interface. For nat, you can spell out the definition of "natural numbers object" to get the interface:

t : Type

o : t

s : t -> t

f : forall a (z:a) (i: a -> a), t -> a

f_preserves_0 : forall a (z:a) (i: a -> a), f o = z

f_preserves_succ : forall a (z:a) (i: a -> a) x, f (s x) = i (f x)

f_unique :  forall a (z:a) (i: a -> a) (g : t -> a),

  (forall a (z:a) (i: a -> a), g o = z) ->

  (forall a (z:a) (i: a -> a) x, g (s x) = i (g x)) ->

  forall t, f t = g t

The math-classes library takes a similar approach, defining a Naturals interface as the initial semiring (so that it also specifies the addition and multiplication functions); it includes implementations for nat, N, and a few more I think, and all of the theorems for "Naturals" apply "for free" to all the implementations. However, it's not entirely trivial to transfer theorems about one of the implementations (say nat) to the interface: there's a fair bit of boilerplate involved (which tactics can take of).

On Sun, May 6, 2018 at 7:24 AM, Fred Smith <fsmith1024 AT gmail.com> wrote:

Hi,

I have thoroughly confused myself, and hope someone can help straighten me out.  I started down this question trying to understand how to abstract an interface away from the actual implementation, and it occurred to me that the question is very general.

Suppose I define my own "natx" that is in every way equivalent to "nat" except I rename the constructors "Sx" and "Ox".  It is straightforward to write coercions from natx into and out of nat and prove these form a  bijection.  I would like to think that I can now "import" all of the rich theory surrounding nat and make it available for my type natx.  

I have half-convinced myself that this is possible through writing trivial wrappers.  My first question is: is there a hole?  Is there something I cannot import nearly for free?  I expect problems around higher-order arguments but it looks like it works out?

Still, all this work to write wrappers seems unnecessary.  Conceptually the unique thing about nat is not the name "S" and "O" but its structure.  Therefore, I ought to be able to write a Module Type interface hiding this detail.  Then if all of the proofs about "nat" were parameterized by this interface, I could very easily get all the theory for "nat" for free for natx.

My contrived example does not seem so interesting, but suppose I found some sub-structure that was isomorphic to nat then suddenly this might be much more interesting. (I don't have an actual example, just imagining one)

Where I am stuck is writing this Module Type interface.   I can't seem to come up with anything that can serve as a computational replacement for nat without effectively exporting an inductive type exactly like nat.  My interface can contain nat_ind which is fine for reasoning about propositions (at least it seems fine), but I have been unable to produce any useful definition that will let me define "plus".  I guess I need the equivalent of nat_rect but if the definition isn't transparent, I don't think you can prove anything about it.  

Thanks for your help,

Fred