The Coq mailing list

[Morrisett <morrisett AT gmail.com>]

You might look at Abhishek Anand’s parametricity plug in. This lets you do 
this.  

-Greg

> On May 6, 2018, at 10: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
>