The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

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.