The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le lundi 02 juillet 2007 à 16:12 +0200, Bruno Barras a écrit :

> You need to change very little code. You just have to encapsulate your
> "well" proof with a function that adds 10^100 constructors on top of it:
> 
> Having "well" opaque is probably safer in call-by-value. As a final
> remark, the lazy strategy is maybe slightly faster because it will not
> compute the proofs of (order (S n) n), but this is probably not a big
> deal.
> 
> I have never actually tried this solution, so I am interested to know if
> it behaves like I think it should.

You are great! It works just fine, even when the termination criteria is
provided by classical logic.

I would not have used a value as large as 10^100, but you got me
curious. So I tested some large values. As expected, it has no impact on
"lazy". For "compute" and "vm_compute", it starts to be noticeable at
10^20; and at 10^30, Coq is lost in hell.

I'm surprised Coq is able to go that far with the call-by-value
evaluation scheme. I must be missing something about the way your
"guard" function is expanded. How many constructors are explicitly
created for 10^20 in call-by-value?

> > This is really interesting, as I didn't expect that this problem could
> > actually occur. Do you know of such an occurrence in a real body of Coq
> > proofs, e.g. the standard library of Coq?
> >   
> Omega.
> To prove formula F, it proves ~~F (if F is Presburger then it is
> decidable, so ~~F implies F). Then it introduces ~F, and tries to derive
> False.
> So, all the complex work is done in an inconsistent context.

I was talking about a useful term that would require an infinite amount
of time to check for convertibility in an inconsistent context, if the
evaluation strategy were to be changed. I'm not sure Omega contains such
terms. But now I see that the strategy does not have to be changed, so I
guess my question was ill-formed and it may not have any answer.

Best regards,

Guillaume