The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 24/01/2014 19:54, Andrew Rodriguez wrote:
> Out of curiosity, would it be possible to use UIP to "hide" the opaque
> proof? My idea, which I haven't been able to implement, would be to use
> UIP to replace the plus_n_O with eq_refl and then the existing match
> with eq_refl would go be able to go through. It would avoid the only
> downside that cast: that it has to recreate the list just to appease the
> typechecker.

UIP on any type is an axiom, so it'll only make things about reduction
worse. If you consider it over nat, which has a decidable equality, I am
afraid it essentially does something similar on the naturals it
manipulates, recreating the equality by induction over them.

If your ultimate goal is extraction, well, yes, UIP (either as an axiom
or proved) will result in something better behaved, but otherwise, I am
afraid that there ain't no free lunch.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature