The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

> > In system I develop I have all the time lot of (un)prooved
> > subgoals. Proved subgoals are not interesting for me but unproved
> > are. I guess the Coq keep all of them in RAM until I proving the
> > main goal. Is it correct? I need to optimize the time of processing.
> > Is it possible to store unproved subgoals on hard disk and then
> > erase them from memory? Later I will take it from disk as needed.
>
> I don't think Coq has an explicit mechanism for that, but if you
> refrain from any sort of "Show Proof" and you have a sizeable amount
> of swap activated, your OS should do about that automatically... until
> Qed time.

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 ?

   Regards, Eric

--------------------------

Inductive bit:Set:= v0:bit | v1:bit.
Definition bit2nat(b:bit):nat:=match b with v0 => 0 | v1 => 1 end.
Coercion bit2nat:bit>->nat.

Definition comp1(b:bit):bit:=match b with v0 => v1 | v1 => v0 end.
Definition add11(b1 b2 b3:bit):=
match (b1,b2,b3) with (v0,v0,_) => (v0,b3) | (v1,v1,_) => (v1,b3) | _ =>
(b3,comp1 b3) end.

Inductive byte:Set:=bt:bit->bit->bit->bit->bit->bit->bit->bit->byte.
Definition byte2nat(b:byte):nat:=
match b with bt b7 b6 b5 b4 b3 b2 b1 b0 =>
(((((((b7*2+b6)*2+b5)*2+b4)*2+b3)*2+b2)*2+b1)*2+b0) end.
Coercion byte2nat:byte>->nat.

Definition add88(b1 b2:byte):=
match b1 with bt b17 b16 b15 b14 b13 b12 b11 b10 =>
 match b2 with bt b27 b26 b25 b24 b23 b22 b21 b20 =>
  match add11 b10 b20 v0 with (c0,b30) =>
  match add11 b11 b21 c0 with (c1,b31) =>
  match add11 b12 b22 c1 with (c2,b32) =>
  match add11 b13 b23 c2 with (c3,b33) =>
  match add11 b14 b24 c3 with (c4,b34) =>
  match add11 b15 b25 c4 with (c5,b35) =>
  match add11 b16 b26 c5 with (c6,b36) =>
  match add11 b17 b27 c6 with (c7,b37) =>
   (c7,bt b37 b36 b35 b34 b33 b32 b31 b30)
  end end end end end end end end
 end
end
.

Theorem add88_correct:forall (b1 b2:byte),
                        match (add88 b1 b2) with (c,b) => b1+b2=c*256+b
end.
Proof.
induction b1 as [b17 b16 b15 b14 b13 b12 b11 b10];
 induction b10; induction b11; induction b12; induction b13;
 induction b14; induction b15; induction b16; induction b17; (* BP 1 *)
 induction b2 as [b27 b26 b25 b24 b23 b22 b21 b20];
 induction b20; induction b21; induction b22; induction b23;
 induction b24; induction b25; induction b26; induction b27; (* BP 2 *)
 simpl; apply refl_equal.
Qed.