The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/31/2016 11:41 PM, Jonathan Leivent wrote:
> On 08/31/2016 11:18 PM, Jason Gross wrote:
> > Actually, I think it's possible to do better; you should only need
> > AtoB_BtoA specialized to the point you care about.  This should be a
> > relatively simple transformation to make, and, I think, should be 
> > powerful
> > enough to let you handle recursive types
>
> I think you are right that AtoB_BtoA only needs to be at a point. But, 
> if AtoB is always a ctor and BtoA is always a proj, then I'm not sure 
> that this specialization helps much, if at all.
>
> -- Jonathan

Oops - it is needed. I just tried using UIP_iso_pointed to prove UIP on 
nat, and got:

|- forall b : nat, S (pred b) = b

which is obviously not true at b=0.  OK - how to make it only need 
AtoB_BtoA at a point?  Obviously, f_equal_cancel needs to be reworked, 
but the obvious way "(e : x=x)" doesn't work.  It always seems peculiar 
to me that in some circumstances in Coq, one can do more to x=y than to 
x=x - as in this case.

-- Jonathan