The Coq mailing list

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

I agree with you, there are much more clever way to prove this result, even
using computations (you may also prove it for 4-bit words, then build bytes
combining 4-bit words, etc.). My point is more related to the memory
management question : I've never been as far as getting the 65536 subgoals,
because this is too long, and requires a huge swap.

My question about the possibility to ask Coq to be more "lazy" was to have
quickly the first subgoal (e.g. allowing me to detect if something is
wrong), not generating the other ones until I've completed the first one or
I use the Focus command. Once two subgoals are produced (with a "." to mark
the end of the combined tactic), all the other tactics will be applied to
one and only one of them, so why care about having all them at once ?

A form of deferred generation, combined with a form of "opaque" and
"dont-load-proof", would may be reduce significantly memory requirements, to
the benefit of speed. Of course, not being a developper of Coq (nor being
able to be one), this may be a naive question.

   Regards, Eric

> Frédéric Besson wrote:
> > On my laptop, the whole script takes 300s.
>    Just to go furthermore in the direction of Frederic,
>        You can do the same using N (and not nat) for the computation.
>        In my computer the compilation takes less that 1 second :) .
>      Benjamin


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


> Inductive bit:Set:= v0:bit | v1:bit.
>
> Require Import NArith.
>
> Definition bit2_N0 b := match b with v0 => N0 | v1 => 1%N end.
> Definition bit2_N b := match b with v0 => Ndouble | v1 => Ndouble_plus_one
> end.
>
> Coercion bit2_N0 : bit >-> N.
>
> 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 byte2N b :=
>  match b with
>  | bt b7 b6 b5 b4 b3 b2 b1 b0 =>
>     bit2_N b0 (bit2_N b1 (bit2_N b2 (bit2_N b3 (bit2_N b4 (bit2_N b5
> (bit2_N b6 b7))))))
>  end.
>
> Coercion byte2N : byte >-> N.
>
> 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
> .
>
> Definition one := bt v0 v0 v0 v0 v0 v0 v0 v1.
> Definition zero :=bt v0 v0 v0 v0 v0 v0 v0 v0.
> Definition max_int := bt v1 v1 v1 v1 v1 v1 v1 v1.
>
> Section ForAll.
>
> Variable f : byte -> bool.
>
> Definition prover1 b7 b6 b5 b4 b3 b2 b1 :=
>   andb (f (bt b7 b6 b5 b4 b3 b2 b1 v0)) (f (bt b7 b6 b5 b4 b3 b2 b1 v1)).
>
>  Lemma prover1_spec : forall b7 b6 b5 b4 b3 b2 b1,
>    prover1 b7 b6 b5 b4 b3 b2 b1 = true -> forall b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover1;intros.
>   case_eq (f (bt b7 b6 b5 b4 b3 b2 b1 v0));intros Heq;rewrite Heq in H;try
> discriminate.
>   destruct b0;trivial.
>  Qed.
>
>  Definition prover2 b7 b6 b5 b4 b3 b2 :=
>    andb (prover1 b7 b6 b5 b4 b3 b2 v0) (prover1 b7 b6 b5 b4 b3 b2 v1).
>
>  Lemma prover2_spec : forall b7 b6 b5 b4 b3 b2,
>    prover2 b7 b6 b5 b4 b3 b2 = true -> forall b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover2;intros.
>   apply prover1_spec.
>   case_eq (prover1 b7 b6 b5 b4 b3 b2 v0);intros Heq;rewrite Heq in H;try
> discriminate.
>   destruct b1;trivial.
>  Qed.
>
> Definition prover3 b7 b6 b5 b4 b3 :=
>    andb (prover2 b7 b6 b5 b4 b3 v0) (prover2 b7 b6 b5 b4 b3 v1).
>
>  Lemma prover3_spec : forall b7 b6 b5 b4 b3,
>    prover3 b7 b6 b5 b4 b3 = true -> forall b2 b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover3;intros.
>   apply prover2_spec.
>   case_eq (prover2 b7 b6 b5 b4 b3 v0);intros Heq;rewrite Heq in H;try
> discriminate.
>   destruct b2;trivial.
>  Qed.
>
>  Definition prover4 b7 b6 b5 b4 :=
>    andb (prover3 b7 b6 b5 b4 v0) (prover3 b7 b6 b5 b4 v1).
>
>  Lemma prover4_spec : forall b7 b6 b5 b4,
>    prover4 b7 b6 b5 b4 = true -> forall b3 b2 b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover4;intros.
>   apply prover3_spec.
>   case_eq (prover3 b7 b6 b5 b4 v0);intros Heq;rewrite Heq in H;try
> discriminate.
>   destruct b3;trivial.
>  Qed.
>
>  Definition prover5 b7 b6 b5 :=
>    andb (prover4 b7 b6 b5 v0) (prover4 b7 b6 b5 v1).
>
>  Lemma prover5_spec : forall b7 b6 b5,
>    prover5 b7 b6 b5 = true -> forall b4 b3 b2 b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover5;intros.
>   apply prover4_spec.
>   case_eq (prover4 b7 b6 b5 v0);intros Heq;rewrite Heq in H;try
> discriminate.
>   destruct b4;trivial.
>  Qed.
>
>  Definition prover6 b7 b6 :=
>    andb (prover5 b7 b6 v0) (prover5 b7 b6 v1).
>
>  Lemma prover6_spec : forall b7 b6,
>    prover6 b7 b6 = true -> forall b5 b4 b3 b2 b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover6;intros.
>   apply prover5_spec.
>   case_eq (prover5 b7 b6 v0);intros Heq;rewrite Heq in H;try discriminate.
>   destruct b5;trivial.
>  Qed.
>
> Definition prover7 b7 :=
>    andb (prover6 b7 v0) (prover6 b7 v1).
>
>  Lemma prover7_spec : forall b7,
>    prover7 b7 = true -> forall b6 b5 b4 b3 b2 b1 b0, f (bt b7 b6 b5 b4 b3
> b2 b1 b0) = true.
>  Proof.
>   unfold prover7;intros.
>   apply prover6_spec.
>   case_eq (prover6 b7 v0);intros Heq;rewrite Heq in H;try discriminate.
>   destruct b6;trivial.
>  Qed.
>
>  Definition prover := andb (prover7 v0) (prover7 v1).
>
>  Lemma prover_proves : prover = true -> forall b, f b = true.
>  Proof.
>   unfold prover;intros.
>   destruct b; apply prover7_spec.
>   case_eq (prover7 v0);intros Heq;rewrite Heq in H;try discriminate.
>   destruct b;trivial.
>  Qed.
>
> End ForAll.
>
> Require Import Ndec.
> Open Scope N_scope.
>
> Definition final_test b1 b2 :=
>  match (add88 b1 b2) with
>  | (c,b) => Neqb (b1 + b2) (c*256 + b)
>  end.
>
> Definition checker :=
>   prover (fun b1 => prover (fun b2 => final_test b1 b2)).
>
> Lemma checker_proves : checker = true -> forall b1 b2, match (add88 b1 b2)
> with (c,b) =>
>       b1+b2= c*256+b end.
> Proof.
>  unfold checker;intros.
>  assert (W:=prover_proves _ H b1).
>  assert (W1 := prover_proves _ W b2);simpl in W1.
>  unfold final_test in W1;destruct (add88 b1 b2) as (c,b).
>  rewrite (Neqb_complete _ _ W1);trivial.
> Qed.
>
> Theorem add88_correct_N:forall (b1 b2:byte),
>                        match (add88 b1 b2) with (c,b) => b1+b2=c*256+b
> end.
> Proof.
>  apply checker_proves.
> Time  vm_compute.
>  reflexivity.
> Time Qed.
>
> (* If you really want nat *)
> Require Import Nnat.
> Definition bit2nat(b:bit):nat:=match b with v0 => 0%nat | v1 => 1%nat end.
> Coercion bit2nat:bit>->nat.
>
> 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)%nat end.
> Coercion byte2nat:byte>->nat.
>
> Definition checker_nat :=
>   prover (fun b => Neqb (N_of_nat (byte2nat b)) b).
>
> Lemma checker_nat_proves :  forall b,
>   (N_of_nat (byte2nat b)) = b.
> Proof.
>  cut (prover (fun b => Neqb (N_of_nat (byte2nat b)) b) = true).
>  intros;assert (W:=prover_proves _ H b);simpl in W.
>  apply (Neqb_complete _ _ W);trivial.
>  vm_compute;reflexivity.
> Qed.
>
> Theorem add88_correct:forall (b1 b2:byte),
>                        match (add88 b1 b2) with (c,b) =>
> (b1+b2=c*256+b)%nat end.
> Proof.
>  intros.
>  assert (W:= add88_correct_N b1 b2).
>  destruct (add88 b1 b2) as (c,b).
>  rewrite <- (nat_of_N_of_nat (b1+b2)%nat).
>  rewrite N_of_plus.
>  repeat rewrite checker_nat_proves.
>  rewrite W.
>  rewrite <- (nat_of_N_of_nat  (c * 256 + b)%nat).
>  rewrite N_of_plus.
>  repeat rewrite checker_nat_proves.
>  destruct c;trivial.
> Qed.