The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

On 6 mars 08, at 17:20, JAEGER, Eric (SGDN) wrote:
> Preferring the computer computing rather than me thinking, I've  
> developped
> this very stupid proof, with as a stunning result the correctness  
> of the
> addition of two bytes. I guess this illustrates the question about
> optimizing space and time.
>
> Generating 256 subgoals (breaking the proof at BP 1) takes 3-5  
> seconds on my
> PC. I've never been patient enough the see the 65536 subgoals  
> (breaking the
> proof at BP 2) but this seems to be far more than 256*5 seconds,  
> and my swap
> has been expanded by more than 1GB. I cannot imagine ever being  
> able to
> compile the proof as provided. It may be possible to optimize the
> definitions (yet I think e.g. that b7*2 is more efficient than  
> 2*b7), but
> this would not help regarding the generation of subgoals. Is there  
> a way,
> may be, to ask Coq to be more "lazy" when generating subgoals ?

Even if subgoal generation were lazy, the proof tree is nonetheless  
huge.
Using proof-by-reflection (Coq'Art Chap 16), I have a solution
that is still using brute-force but which proof-term is small.

Of course, this is a solution that is domain-specific and not a  
generic solution for reducing the memory footprint.

The idea is to program a "prover" which enumerates over all the pairs  
of bytes, computes the sum and compare the results.
Using the vm_compute tactic, this computation takes 39s.

(BTW, the prover has to be proved correct -- but it is reusable...
To do that,  I've developped a "very stupid proof" that enumerates  
over all the bytes (256 cases).
It takes a long time but eventually terminates -- clever guys could  
think of a clever inductive argument.)

On my laptop, the whole script takes 300s.

Attachment: prover.v
Description: Binary data

--
Frédéric