The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Thank you, Guillaume and Laurent,

I have now several proofs of the same fact, some of them are saved 
almost instantly.

The first one takes more than 2 minutes at Qed.

I'll try to write some tactics for doing the correct abstractions.

Best regards,

Pierre





Le 25/04/2017 à 14:52, Guillaume Melquiond a écrit :
> On 25/04/2017 08:55, Pierre Casteran wrote:
> > Hi,
> >
> >    I wrote a small proof on fast growing functions (Wainer's hierarchy).
> >
> >    The statement is F_3 (2) > F_omega (2). The proof term is not so big,
> > but it contains several occurrences of (f_2 23), which is known as
> > greater than 2^23.
> >
> >    The problem may come from the fact that all these subterms are
> > computed after Qed, thus I had to interrupt after some time. Is there an
> > option for preventing Coq to expand function calls ?
> As Laurent said, the kernel should not compute if computing is not
> needed. The hard part is to convince the kernel that it is indeed not
> needed. Usually, generalizing or abstracting tend to give enough
> information to the kernel to avoid useless computations.
>
> Here is a small example. Suppose you want to prove (fact 100 = 100 *
> fact 99). There is a trivial proof term, which is (eq_refl 100 : fact
> 100 = fact 100). Unfortunately, when comparing the right-hand sides, the
> kernel decides to reduce (fact 99) instead of (fact 100), which causes
> the verification to run forever. To avoid this issue, just generalize
> away 99. This gives a needlessly complicated proof term but at least the
> kernel now checks it instantly.
>
> Goal fact 100 = 100 * fact 99.
> Proof.
>    assert (exists i, i = 99) as [i <-] by now eexists.
>    reflexivity.
> Qed.
>
> Best regards,
>
> Guillaume