The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Guillaume Melquiond wrote:
>
> So I have two choices. Either I bound the number of iterations with an
> arbitrary low value and my functions are no longer guaranteed to return
> the correct result in Coq. Or I bound it with the proved value (which
> don't even exist for all the functions) and Coq will probably die while
> computing this value.
>
>   
Hi Guillaume,
why not bounding with a large value ? (I don't think anyone is patient
enough to wait 10^100 iterations, even with a very fast computer.)
If the counter is coded as a positive (binary representation), then it
is not very big.

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:

Require Import NArith.

Variable A: Type.
Variable R: A->A->Prop.

Fixpoint guard (p:positive) : well_founded R -> well_founded R :=
  match p with
  | xH => fun wfR x => Acc_intro x (fun y _ => wfR y)
  | xO p' => let F := guard p' in fun wfR => F (F wfR)
  | xI p' => let F := guard p' in
     fun wfR x => Acc_intro x (fun y _ => F (F wfR) y)
  end.

Definition big : positive := ...

Then "guard big well" will let the fixpoint expand without time penalty
for 10^100 iterations then it will give the "well" proof, so it will
suddendly slow down, if you ever get to that point (which I doubt since
the nat 10^100 will not fit in the memory of your computer). You don't
even have any memory space problem since this "big" proof is computed
lazily:
at every step, the next constructor is always under an abstraction, so
it is computed only once the previous constructor has been matched.

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.

> 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.

Bruno.