path: root/theories/Numbers/Natural/BigN/NMake_gen.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
(************************************************************************)

(*S NMake_gen.ml : this file generates NMake.v *)


(*s The two parameters that control the generation: *)

let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
                process before relying on a generic construct *)
let gen_proof = true  (* should we generate proofs ? *)


(*s Some utilities *)

let t = "t"
let c = "N"
let pz n = if n == 0 then "ZnZ.zero" else "W0"
let rec gen2 n = if n == 0 then "1" else if n == 1 then "2"
                 else "2 * " ^ (gen2 (n - 1))
let rec genxO n s =
  if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"

let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ s

let rec iter_name i j base sep =
  if i >= j then base^(string_of_int i)
  else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j)

(* Standard printer, with a final newline *)
let pr s = Printf.printf (s^^"\n")
(* Printing to /dev/null *)
let pn s = Printf.ifprintf stdout s
(* Proof printer : prints iff gen_proof is true *)
let pp = if gen_proof then pr else pn
(* Printer for admitted parts : prints iff gen_proof is false *)
let pa = if not gen_proof then pr else pn
(* Same as before, but without the final newline *)
let pr0 = Printf.printf
let pp0 = if gen_proof then pr0 else pn


(*s The actual printing *)

let _ =

  pr "(************************************************************************)";
  pr "(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)";
  pr "(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)";
  pr "(*   \\VV/  **************************************************************)";
  pr "(*    //   *      This file is distributed under the terms of the       *)";
  pr "(*         *       GNU Lesser General Public License Version 2.1        *)";
  pr "(************************************************************************)";
  pr "(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)";
  pr "(************************************************************************)";
  pr "";
  pr "(** * NMake_gen *)";
  pr "";
  pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
  pr "";
  pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
  pr "";
  pr "Require Import BigNumPrelude ZArith CyclicAxioms";
  pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic";
  pr " Wf_nat StreamMemo.";
  pr "";
  pr "Module Make (W0:CyclicType) <: NAbstract.";
  pr "";

  pr " (** * The word types *)";
  pr "";

  pr " Local Notation w0 := W0.t.";
  for i = 1 to size do
    pr " Definition w%i := zn2z w%i." i (i-1)
  done;
  pr "";

  pr " (** * The operation type classes for the word types *)";
  pr "";

  pr " Local Notation w0_op := W0.ops.";
  for i = 1 to min 3 size do
    pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
  done;
  for i = 4 to size do
    pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
  done;
  for i = size+1 to size+3 do
    pr " Instance w%i_op : ZnZ.Ops (word w%i %i%%nat) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
  done;
  pr "";

  pr " Section Make_op.";
  pr "  Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w').";
  pr "";
  pr "  Fixpoint make_op_aux (n:nat) : ZnZ.Ops (word w%i (S n)):=" size;
  pr "   match n return ZnZ.Ops (word w%i (S n)) with" size;
  pr "   | O => w%i_op" (size+1);
  pr "   | S n1 =>";
  pr "     match n1 return ZnZ.Ops (word w%i (S (S n1))) with" size;
  pr "     | O => w%i_op" (size+2);
  pr "     | S n2 =>";
  pr "       match n2 return ZnZ.Ops (word w%i (S (S (S n2)))) with" size;
  pr "       | O => w%i_op" (size+3);
  pr "       | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))";
  pr "       end";
  pr "     end";
  pr "   end.";
  pr "";
  pr " End Make_op.";
  pr "";
  pr " Definition omake_op := make_op_aux mk_zn2z_ops_karatsuba.";
  pr "";
  pr "";
  pr " Definition make_op_list := dmemo_list _ omake_op.";
  pr "";
  pr " Instance make_op n : ZnZ.Ops (word w%i (S n))" size;
  pr "  := dmemo_get _ omake_op n make_op_list.";
  pr "";

  pr "";
  pr " Lemma make_op_omake: forall n, make_op n = omake_op n.";
  pr " intros n; unfold make_op, make_op_list.";
  pr " refine (dmemo_get_correct _ _ _).";
  pr " Qed.";
  pr "";


  pr " (** * The main type [t], isomorphic with [exists n, word w0 n] *)";
  pr "";

  pr " Inductive %s_ :=" t;
  for i = 0 to size do
    pr "  | %s%i : w%i -> %s_" c i i t
  done;
  pr "  | %sn : forall n, word w%i (S n) -> %s_." c size t;
  pr "";
  pr " Definition %s := %s_." t t;
  pr "";

  pr " (** * A generic toolbox for building and deconstructing [t] *)";
  pr "";

  pr " Local Notation SizePlus n := %sn%s."
    (iter_str size "(S ") (iter_str size ")");
  pr "";

  pr " Definition dom_t n := match n with";
  for i = 0 to size do
    pr "  | %i => w%i" i i;
  done;
  pr "  | %sn => word w%i n" (if size=0 then "" else "SizePlus ") size;
  pr " end.";
  pr "";

  pr " Instance dom_op n : ZnZ.Ops (dom_t n) | 10.";
  pa " Admitted.";
  pp " Proof.";
  pp "  do %i (destruct n; [simpl;auto with *|])." (size+1);
  pp "  unfold dom_t. auto with *.";
  pp " Defined.";
  pr "";

  pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A)(x:t) : A :=";
  pr "  match x with";
  for i = 0 to size do
    pr "   | %s%i wx => f %i wx" c i i;
  done;
  pr "   | %sn n wx => f (SizePlus (S n)) wx" c;
  pr "  end.";
  pr "";

  pr " Definition mk_t (n:nat) : dom_t n -> t :=";
  pr "  match n as n' return dom_t n' -> t with";
  for i = 0 to size do
    pr "   | %i => %s%i" i c i;
  done;
  pr "   | %s(S n) => %sn n" (if size=0 then "" else "SizePlus ") c;
  pr "  end.";
  pr "";

pr "
 Definition level := iter_t (fun n _ => n).

 Inductive View_t : t -> Prop :=
  Mk_t : forall n (x : dom_t n), View_t (mk_t n x).

 Lemma destr_t : forall x, View_t x.
 Proof.
 intros x. generalize (Mk_t (level x)). destruct x; simpl; auto.
 Qed.
";

pr "
 Lemma iter_mk_t : forall A (f:forall n, dom_t n -> A),
 forall n x, iter_t f (mk_t n x) = f n x.
 Proof.
 do %i (destruct n; try reflexivity).
 Qed.
" (size+1);

pr "
 (** * Projection to ZArith *)

 Definition to_Z : t -> Z :=
  Eval lazy beta iota delta [iter_t dom_t dom_op] in
  iter_t (fun _ x => ZnZ.to_Z x).
";

  pr " Open Scope Z_scope.";
  pr " Notation \"[ x ]\" := (to_Z x).";
  pr "";

pr "
 Theorem spec_mk_t : forall n (x:dom_t n), [mk_t n x] = ZnZ.to_Z x.
 Proof.
 intros. change to_Z with (iter_t (fun _ x => ZnZ.to_Z x)).
 rewrite iter_mk_t; auto.
 Qed.
";

  pp " (* Regular make op (no karatsuba) *)";
  pp " Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) :";
  pp "       ZnZ.Ops (word ww n) :=";
  pp "  match n return ZnZ.Ops (word ww n) with";
  pp "   O => ww_op";
  pp "  | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)";
  pp "  end.";
  pp "";
  pp " (* Simplification by rewriting for nmake_op *)";
  pp " Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,";
  pp "   nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).";
  pp " auto.";
  pp " Qed.";
  pp "";


  pr " (* Eval and extend functions for each level *)";
  for i = 0 to size do
    pp " Let nmake_op%i := nmake_op _ w%i_op." i i;
    pp " Let eval%in n := ZnZ.to_Z (Ops:=nmake_op%i n)." i i;
    if i == 0 then
      pr " Let extend%i := DoubleBase.extend (WW (ZnZ.zero:w0))." i
    else
      pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i;
  done;
  pr "";


  pp " Theorem digits_doubled:forall n ww (w_op: ZnZ.Ops ww),";
  pp "    ZnZ.digits (nmake_op _ w_op n) =";
  pp "    DoubleBase.double_digits (ZnZ.digits w_op) n.";
  pp " Proof.";
  pp " intros n; elim n; auto; clear n.";
  pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits.";
  pp " rewrite <- Hrec; auto.";
  pp " Qed.";
  pp "";
  pp " Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),";
  pp "    ZnZ.to_Z (Ops:=nmake_op _ w_op n) =";
  pp "    @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n.";
  pp " Proof.";
  pp " intros n; elim n; auto; clear n.";
  pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.";
  pp " rewrite <- Hrec; auto.";
  pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto.";
  pp " Qed.";
  pp "";


  pp " Theorem digits_nmake:forall n ww (w_op: ZnZ.Ops ww),";
  pp "    ZnZ.digits (nmake_op _ w_op (S n)) =";
  pp "    xO (ZnZ.digits (nmake_op _ w_op n)).";
  pp " Proof.";
  pp " auto.";
  pp " Qed.";
  pp "";


  pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,";
  pp "  ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) =";
  pp "   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh *";
  pp "    base (ZnZ.digits (nmake_op ww ww_op n)) +";
  pp "   ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl.";
  pp " Proof.";
  pp " auto.";
  pp " Qed.";
  pp "";

  pp " Theorem make_op_S: forall n,";
  pp "   make_op (S n) = mk_zn2z_ops_karatsuba (make_op n).";
  pp " intro n.";
  pp " do 2 rewrite make_op_omake.";
  pp " pattern n; apply lt_wf_ind; clear n.";
  pp " intros n; case n; clear n.";
  pp "   intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2);
  pp " intros n; case n; clear n.";
  pp "   intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3);
  pp " intros n; case n; clear n.";
  pp "   intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2);
  pp " intros n Hrec.";
  pp "   change (omake_op (S (S (S (S n))))) with";
  pp "          (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op (S n))))).";
  pp "   change (omake_op (S (S (S n)))) with";
  pp "         (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op n)))).";
  pp "   rewrite Hrec; auto with arith.";
  pp " Qed.";
  pp "";

pr "
 Lemma dom_t_S : forall n, zn2z (dom_t n) = dom_t (S n).
 Proof.
  do %i (destruct n; try reflexivity).
 Defined.

 Definition cast w w' (H:w=w') (x:w) : w' :=
   match H in _=y return y with
   | eq_refl => x
   end.

 Definition mk_t_S n (x:zn2z (dom_t n)) : t :=
  Eval lazy beta delta [cast dom_t_S] in
  mk_t (S n) (cast _ _ (dom_t_S n) x).

 Theorem spec_mk_t_S : forall n (x:zn2z (dom_t n)),
  [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
 Proof.
 intros.
 do %i (destruct n; [reflexivity|]).
 simpl. rewrite !make_op_S. reflexivity.
 Qed.

 Lemma mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
 Proof.
 do %i (destruct n; try reflexivity).
 Qed.
" (size+1) (size+1) (size+1);

  pr " (** * The specification proofs for the word operators *)";
  pr "";

  if size <> 0 then
  pr " Typeclasses Opaque %s." (iter_name 1 size "w" " ");
  pr "";

  pp " Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
  for i = 1 to min 3 size do
    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
  done;
  for i = 4 to size do
    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
  done;
  for i = size+1 to size+3 do
    pp " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
  done;
  pp "";

  pp " Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).";
  pp " Proof.";
  pp "  intros n; elim n; clear n.";
  pp "    exact w%i_spec." (size + 1);
  pp "  intros n Hrec; rewrite make_op_S.";
  pp "  exact (mk_zn2z_specs_karatsuba Hrec).";
  pp " Qed.";
  pp "";

pr "
 Instance dom_spec n : ZnZ.Specs (dom_op n) | 10.
 Proof.
  do %i (destruct n; auto with *). apply wn_spec.
 Qed.
" (size+1);

  for i = 1 to size + 2 do
    pp " Let to_Z_%i: forall x y," i;
    pp "   ZnZ.to_Z (Ops:=w%i_op) (WW x y) =" i;
    pp "    ZnZ.to_Z (Ops:=w%i_op) x * base (ZnZ.digits w%i_op) + ZnZ.to_Z (Ops:=w%i_op) y." (i-1) (i-1) (i-1);
    pp " Proof.";
    pp " auto.";
    pp " Qed.";
    pp "";
  done;

  pp " Let to_Z_n: forall n x y,";
  pp "   ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =";
  pp "    ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n)) + ZnZ.to_Z (Ops:=make_op n) y.";
  pp " Proof.";
  pp " intros n x y; rewrite make_op_S; auto.";
  pp " Qed.";
  pp "";

  for i = 0 to size do
    pp " Theorem digits_w%i:  ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w0_op %i)." i i i;
    if i == 0 then
      pp " auto."
    else
      pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1);
    pp " Qed.";
    pp "";
    pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (ZnZ.digits w%i_op) (ZnZ.to_Z (Ops:=w%i_op)) n." i i i i;
    pp " Proof.";
    pp "  intros n; exact (nmake_double n w%i w%i_op)." i i;
    pp " Qed.";
    pp "";
  done;

  for i = 0 to size do
    for j = 0 to (size - i) do
      pp " Theorem digits_w%in%i: ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w%i_op %i)." i j (i + j) i j;
      pp " Proof.";
      if j == 0 then
        if i == 0 then
          pp " auto."
        else
          begin
            pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1);
            pp "  auto.";
            pp "  unfold nmake_op; auto.";
          end
      else
        begin
          pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1);
          pp "  auto.";
          pp " rewrite digits_nmake.";
          pp " rewrite digits_w%in%i." i (j - 1);
          pp " auto.";
        end;
      pp " Qed.";
      pp "";
      pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
      pp " Proof.";
      if j == 0 then
        pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
      else
        begin
          pp " intros x; case x.";
          pp "   auto.";
          pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (i + j);
          pp " rewrite digits_w%in%i." i (j - 1);
          pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1);
          pp " unfold eval%in, nmake_op%i." i i;
          pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1);
        end;
      pp " Qed.";
      if i + j <> size  then
        begin
          pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j;
          if j == 0 then
            begin
              pp " intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." i (i + j);
              pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1);
              pp " rewrite ZnZ.spec_0; auto.";
            end
          else
            begin
              pp " intros x; change (extend%i %i x) with (WW (ZnZ.zero (Ops:=w%i_op)) (extend%i %i x))." i j (i + j) i (j - 1);
              pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1);
              pp " rewrite ZnZ.spec_0.";
              pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j);
              pp " intros HH; rewrite <- HH; auto.";
            end;
          pp " Qed.";
          pp "";
        end;
    done;

    pp " Theorem digits_w%in%i: ZnZ.digits w%i_op = ZnZ.digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1);
    pp " Proof.";
    pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." size;
    pp "  auto.";
    pp " rewrite digits_nmake.";
    pp " rewrite digits_w%in%i." i (size - i);
    pp " auto.";
    pp " Qed.";
    pp "";

    pp " Let spec_eval%in%i: forall x, [%sn 0  x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
    pp " Proof.";
    pp " intros x; case x.";
    pp "   auto.";
    pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 1);
    pp " rewrite digits_w%in%i." i (size - i);
    pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i);
    pp " unfold eval%in, nmake_op%i." i i;
    pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i);
    pp " Qed.";
    pp "";

    pp " Let spec_eval%in%i: forall x, [%sn 1  x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
    pp " intros x; case x.";
    pp "   auto.";
    pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 2);
    pp " rewrite digits_w%in%i." i (size + 1 - i);
    pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1);
    pp " unfold eval%in, nmake_op%i." i i;
    pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i);
    pp " Qed.";
    pp "";
  done;

  pp " Let digits_w%in: forall n," size;
  pp "   ZnZ.digits (make_op n) = ZnZ.digits (nmake_op _ w%i_op (S n))." size;
  pp " intros n; elim n; clear n.";
  pp "  change (ZnZ.digits (make_op 0)) with (xO (ZnZ.digits w%i_op))." size;
  pp "  rewrite nmake_op_S; apply sym_equal; auto.";
  pp "  intros  n Hrec.";
  pp "  replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n))).";
  pp "  rewrite Hrec.";
  pp "  rewrite nmake_op_S; apply sym_equal; auto.";
  pp "  rewrite make_op_S; apply sym_equal; auto.";
  pp " Qed.";
  pp "";

  pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
  pp " intros n; elim n; clear n.";
  pp "   exact spec_eval%in1." size;
  pp " intros n Hrec x; case x; clear x.";
  pp "  unfold to_Z, eval%in, nmake_op%i." size size;
  pp "    rewrite make_op_S; rewrite nmake_op_S; auto.";
  pp " intros xh xl.";
  pp "  unfold to_Z in Hrec |- *.";
  pp "  rewrite to_Z_n.";
  pp "  rewrite digits_w%in." size;
  pp "  repeat rewrite Hrec.";
  pp "  unfold eval%in, nmake_op%i." size size;
  pp "  apply sym_equal; rewrite nmake_op_S; auto.";
  pp " Qed.";
  pp "";

  pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
  pp " intros n; elim n; clear n.";
  pp "   intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." size size;
  pp "   unfold to_Z.";
  pp "   change (make_op 0) with w%i_op." (size + 1);
  pp "   rewrite to_Z_%i; rewrite ZnZ.spec_0; auto." (size + 1);
  pp " intros n Hrec x.";
  pp "   change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size;
  pp "   unfold to_Z in Hrec |- *; rewrite to_Z_n; auto.";
  pp "   rewrite <- Hrec.";
  pp "  replace (ZnZ.to_Z (Ops:=make_op n) W0) with 0; auto.";
  pp "  case n; auto; intros; rewrite make_op_S; auto.";
  pp " Qed.";
  pp "";

pr "
 Lemma digits_dom_op : forall n,
  Zpos (ZnZ.digits (dom_op n)) = Zpos (ZnZ.digits W0.ops) * 2 ^ Z_of_nat n.
 Proof.
 intros. rewrite Zmult_comm.
 do %i (destruct n; try reflexivity).
 simpl.
 rewrite <- shift_pos_correct. f_equal.
 rewrite shift_pos_nat.
 rewrite ?nat_of_P_succ_morphism, nat_of_P_o_P_of_succ_nat_eq_succ.
 unfold shift_nat. simpl.
 generalize (digits_w%in n); simpl; intros ->.
 rewrite digits_doubled.
 rewrite digits_w%i, ?digits_nmake. simpl.
 induction n; simpl; congruence.
 Qed.
" (size+1) size size;

  pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c;
  pp " intros n; elim n; auto.";
  pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.";
  pp " unfold to_Z.";
  pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
  pp " Qed.";
  pp "";
  pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
  pp " Proof.";
  pp " intros n x; unfold to_Z.";
  pp " rewrite to_Z_n.";
  pp " rewrite <- (Zplus_0_l (ZnZ.to_Z (Ops:=make_op n) x)).";
  pp " apply (f_equal2 Zplus); auto.";
  pp " case n; auto.";
  pp " intros n1; rewrite make_op_S; auto.";
  pp " Qed.";
  pp "";
  pp " Let spec_extend_tr: forall m n (w: word _ (S n)),";
  pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c;
  pp " Proof.";
  pp " induction m; auto.";
  pp " intros n x; simpl extend_tr.";
  pp " simpl plus; rewrite spec_extendn0_0; auto.";
  pp " Qed.";
  pp "";
  pp " Let spec_cast_l: forall n m x1,";
  pp " [%sn (Max.max n m)" c;
  pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =";
  pp " [%sn n x1]." c;
  pp " Proof.";
  pp " intros n m x1; case (diff_r n m); simpl castm.";
  pp " rewrite spec_extend_tr; auto.";
  pp " Qed.";
  pp "";
  pp " Let spec_cast_r: forall n m x1,";
  pp " [%sn (Max.max n m)" c;
  pp "  (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =";
  pp " [%sn m x1]." c;
  pp " Proof.";
  pp " intros n m x1; case (diff_l n m); simpl castm.";
  pp " rewrite spec_extend_tr; auto.";
  pp " Qed.";
  pp "";

  pr " Section SameLevel.";
  pr "";
  pr "  Variable res: Type.";
  pr "  Variable P : Z -> Z -> res -> Prop.";
  pr "  Variable f : forall n, dom_t n -> dom_t n -> res.";
  pr "  Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).";
  pr "";
  for i = 0 to size do
    pr "  Let f%i : w%i -> w%i -> res := f %i." i i i i;
  done;
  pr "  Let fn n := f (SizePlus (S n)).";
  pr "";
  for i = 0 to size do
    pr "  Let Pf%i : forall x y : w%i, P [%s%i x] [%s%i y] (f%i x y) := Pf %i." i i c i c i i i;
  done;
  pr "  Let Pfn n : forall x y, P [%sn n x] [%sn n y] (fn n x y) := Pf (SizePlus (S n))." c c;
  pr "";
  pr "  (* We level the two arguments before applying *)";
  pr "  (* the functions at each level                *)";
  pr "";
  pr "  Definition same_level (x y: t_): res := Eval lazy zeta beta iota delta";
  pr "   [ DoubleBase.extend DoubleBase.extend_aux %s ]" (iter_name 0 (size-1) "extend" "");
  pr "  in match x, y with";
  for i = 0 to size do
    for j = 0 to i - 1 do
      pr "  | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1);
    done;
    pr "  | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
    for j = i + 1 to size do
      pr "  | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1);
    done;
    if i == size then
      pr "  | %s%i wx, %sn m wy => fn m (extend%i m wx) wy" c size c size
    else
      pr "  | %s%i wx, %sn m wy => fn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1);
  done;
  for i = 0 to size do
    if i == size then
      pr "  | %sn n wx, %s%i wy => fn n wx (extend%i n wy)" c c size size
    else
      pr "  | %sn n wx, %s%i wy => fn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1);
  done;
  pr "  | %sn n wx, Nn m wy =>" c;
  pr "    let mn := Max.max n m in";
  pr "    let d := diff n m in";
  pr "     fn mn";
  pr "       (castm (diff_r n m) (extend_tr wx (snd d)))";
  pr "       (castm (diff_l n m) (extend_tr wy (fst d)))";
  pr "  end.";
  pr "";

  pp "  Lemma spec_same_level_0: forall x y, P [x] [y] (same_level x y).";
  pp "  Proof.";
  pp "  intros x; case x; clear x; unfold same_level.";
  for i = 0 to size do
    pp "    intros x y; case y; clear y.";
    for j = 0 to i - 1 do
      pp "     intros y; rewrite spec_extend%in%i; apply Pf%i." j i i;
    done;
    pp "     intros y; apply Pf%i." i;
    for j = i + 1 to size do
      pp "     intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
    done;
    if i == size then
      pp "     intros m y; rewrite (spec_extend%in m); apply (Pfn m)." size
    else
      pp "     intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply (Pfn m)." i size size;
  done;
  pp "    intros n x y; case y; clear y.";
  for i = 0 to size do
    if i == size then
      pp "    intros y; rewrite (spec_extend%in n); apply (Pfn n)." size
    else
      pp "    intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply (Pfn n)." i size size;
  done;
  pp "    intros m y; rewrite <- (spec_cast_l n m x);";
  pp "          rewrite <- (spec_cast_r n m y); apply (Pfn (Max.max n m)).";
  pp "  Qed.";
  pp "";

  pr " End SameLevel.";
  pr "";
  pr " Implicit Arguments same_level [res].";

pr "
 Theorem spec_same_level_dep :
  forall res
   (P : nat -> Z -> Z -> res -> Prop)
   (Pantimon : forall n m z z' r, (n <= m)%%nat -> P m z z' r -> P n z z' r)
   (f : forall n, dom_t n -> dom_t n -> res)
   (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
   forall x y, P (level y) [x] [y] (same_level f x y).
 Proof.
 intros res P Pantimon f Pf.
 set (f' := fun n x y => (n, f n x y)).
 set (P' := fun z z' r => P (fst r) z z' (snd r)).
 assert (FST : forall x y, (level y <= fst (same_level f' x y))%%nat)
  by (destruct x, y; simpl; omega with * ).
 assert (SND : forall x y, same_level f x y = snd (same_level f' x y))
  by (destruct x, y; reflexivity).
 intros. eapply Pantimon; [eapply FST|].
 rewrite SND. eapply (@spec_same_level_0 _ P' f'); eauto.
 Qed.
";

  pr "";
  pr " Section Iter.";
  pr "";
  pr "  Variable res: Type.";
  pr "  Variable P: Z -> Z -> res -> Prop.";
  pr "  (* Abstraction function for each level *)";
  for i = 0 to size do
    pr "  Variable f%i: w%i -> w%i -> res." i i i;
    pr "  Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i;
    pr "  Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i;
    pp "  Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i;
    if i == size then
      begin
        pp "  Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i;
        pp "  Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i;
      end
    else
      begin
        pp "  Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i;
        pp "  Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i;
      end;
    pr "";
  done;
  pr "  Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size;
  pp "  Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c;
  pr "  Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size;
  pp "  Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c;
  pr "";

  pr "  (* We iter the smaller argument with the bigger  *)";
  pr "";
  pr "  Definition iter (x y: t_): res :=";
  pr0 "    Eval lazy zeta beta iota delta [";
  for i = 0 to size do
    pr0 "extend%i " i;
  done;
  pr "";
  pr "                                         DoubleBase.extend DoubleBase.extend_aux";
  pr "                                         ] in";
  pr "  match x, y with";
  for i = 0 to size do
    for j = 0 to i - 1 do
      pr "  | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1);
    done;
    pr "  | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
    for j = i + 1 to size do
      pr "  | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1);
    done;
    if i == size then
      pr "  | %s%i wx, %sn m wy => f%in m wx wy" c size c size
    else
      pr "  | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1);
  done;
  for i = 0 to size do
    if i == size then
      pr "  | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
    else
      pr "  | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1);
  done;
  pr "  | %sn n wx, %sn m wy => fnm n m wx wy" c c;
  pr "  end.";
  pr "";
  let break_eq0 v =
    pp "    generalize (ZnZ.spec_eq0 %s); case ZnZ.eq0; intros H." v;
    pp "      intros; simpl [N0 %s]; rewrite H; trivial." v;
    pp "    clear H."
  in
  pp "  Ltac zg_tac := try";
  pp "    (red; simpl Zcompare; auto;";
  pp "     let t := fresh \"H\" in (intros t; discriminate t)).";
  pp "";
  pp "  Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
  pp "  Proof.";
  pp "  intros x; case x; clear x; unfold iter.";
  for i = 0 to size do
    pp "    intros x y; case y; clear y.";
    for j = 0 to i - 1 do
      pp "     intros y; rewrite spec_eval%in%i;  apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
    done;
    pp "     intros y; apply Pf%i." i;
    for j = i + 1 to size do
      pp "     intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
    done;
    if i == size then
      pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
    else
      pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
  done;
  pp "    intros n x y; case y; clear y.";
  for i = 0 to size do
    if i == size then
      pp "     intros y; rewrite spec_eval%in; apply Pfn%i." size size
    else
      pp "      intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
  done;
  pp "  intros m y; apply Pfnm.";
  pp "  Qed.";
  pp "";


  pr "  (* We iter the smaller argument with the bigger *)";
  pr "  (* with special zero functions *)";
  pr "";
  pr "  Variable f0t:  t_ -> res.";
  pp "  Variable Pf0t: forall x, P 0 [x] (f0t x).";
  pr "  Variable ft0:  t_ -> res.";
  pp "  Variable Pft0: forall x, P [x] 0 (ft0 x).";
  pr "";
  pr "  Definition iter0 (x y: t_): res :=";
  pr0 "    Eval lazy zeta beta iota delta [";
  for i = 0 to size do
    pr0 "extend%i " i;
  done;
  pr "";
  pr "                                         DoubleBase.extend DoubleBase.extend_aux";
  pr "                                         ] in";
  pr "  match x with";
  for i = 0 to size do
    pr "  | %s%i wx =>" c i;
    if i == 0 then
      pr "    if ZnZ.eq0 wx then f0t y else";
    pr "    match y with";
    for j = 0 to i - 1 do
      pr "    | %s%i wy =>" c j;
      if j == 0 then
        pr "       if ZnZ.eq0 wy then ft0 x else";
      pr "       fn%i %i wx wy" j (i - j - 1);
    done;
    pr "    | %s%i wy => f%i wx wy" c i i;
    for j = i + 1 to size do
      pr "    | %s%i wy => f%in %i wx wy" c j i (j - i - 1);
    done;
    if i == size then
      pr "    | %sn m wy => f%in m wx wy" c size
    else
      pr "    | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1);
    pr "    end";
  done;
  pr "  | %sn n wx =>" c;
  pr "    match y with";
  for i = 0 to size do
    pr "    | %s%i wy =>" c i;
    if i == 0 then
      pr "      if ZnZ.eq0 wy then ft0 x else";
    if i == size then
      pr "      fn%i n wx wy" size
    else
      pr "      fn%i n wx (extend%i %i wy)" size i (size - i - 1);
  done;
  pr "    | %sn m wy => fnm n m wx wy" c;
  pr "    end";
  pr "  end.";
  pr "";

  pp "  Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y).";
  pp "  Proof.";
  pp "  intros x; case x; clear x; unfold iter0.";
  for i = 0 to size do
    pp "    intros x.";
    if i == 0 then break_eq0 "x";
    pp "    intros y; case y; clear y.";
    for j = 0 to i - 1 do
      pp "     intros y.";
      if j == 0 then break_eq0 "y";
      pp "     rewrite spec_eval%in%i;  apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
    done;
    pp "     intros y; apply Pf%i." i;
    for j = i + 1 to size do
      pp "     intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
    done;
    if i == size then
      pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
    else
      pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
  done;
  pp "    intros n x y; case y; clear y.";
  for i = 0 to size do
    pp "    intros y.";
    if i = 0 then break_eq0 "y";
    if i == size then
      pp "     rewrite spec_eval%in; apply Pfn%i." size size
    else
      pp "      rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
  done;
  pp "  intros m y; apply Pfnm.";
  pp "  Qed.";
  pp "";


  pr "  End Iter.";
  pr "";


  pr " (***************************************************************)";
  pr " (*                                                             *)";
  pr " (** *                        Reduction                         *)";
  pr " (*                                                             *)";
  pr " (***************************************************************)";
  pr "";

  pr " Definition reduce_0 (x:w0) := %s0 x." c;
  for i = 1 to size do
   pr " Definition reduce_%i :=" i;
   pr "  Eval lazy beta iota delta[reduce_n1] in";
   pr "   reduce_n1 _ _ (N0 ZnZ.zero) (ZnZ.eq0 (Ops:=w%i_op)) %s%i %s%i."
      (i-1) (if i = 1 then c else "reduce_") (i-1) c i
  done;
  pr " Definition reduce_%i :=" (size+1);
  pr "  Eval lazy beta iota delta[reduce_n1] in";
  pr "   reduce_n1 _ _ (N0 ZnZ.zero) (ZnZ.eq0 (Ops:=w%i_op)) reduce_%i (%sn 0)."
    size size c;

  pr " Definition reduce_n n :=";
  pr "  Eval lazy beta iota delta[reduce_n] in";
  pr "   reduce_n _ _ (N0 ZnZ.zero) reduce_%i %sn n." (size + 1) c;
  pr "";

  pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c;
  pp " Proof.";
  pp " intros x; unfold to_Z, reduce_0.";
  pp " auto.";
  pp " Qed.";
  pp "";

  for i = 1 to size + 1 do
    if i == size + 1 then
      pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c
    else
      pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i;
    pp " Proof.";
    pp " intros x; case x; unfold reduce_%i." i;
    pp " exact ZnZ.spec_0.";
    pp " intros x1 y1.";
    pp " generalize (ZnZ.spec_eq0 x1);";
    pp "   case ZnZ.eq0; intros H1; auto.";
    if i <> 1 then
      pp " rewrite spec_reduce_%i." (i - 1);
    pp " unfold to_Z; rewrite to_Z_%i." i;
    pp " unfold to_Z in H1; rewrite H1; auto.";
    pp " Qed.";
    pp "";
  done;

  pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c;
  pp " Proof.";
  pp " intros n; elim n; simpl reduce_n.";
  pp "   intros x; rewrite <- spec_reduce_%i; auto." (size + 1);
  pp " intros n1 Hrec x; case x.";
  pp " unfold to_Z; rewrite make_op_S; auto.";
  pp " exact ZnZ.spec_0.";
  pp " intros x1 y1; case x1; auto.";
  pp " rewrite Hrec.";
  pp " rewrite spec_extendn0_0; auto.";
  pp " Qed.";
  pp "";

pr " Definition reduce n : dom_t n -> t :=";
pr "  match n with";
for i = 0 to size do
pr "   | %i => reduce_%i" i i;
 done;
pr "   | %s(S n) => reduce_n n" (if size=0 then "" else "SizePlus ");
pr "  end%%nat.";
pr "";

pr " Lemma spec_reduce : forall n (x:dom_t n), [reduce n x] = ZnZ.to_Z x.";
pa " Admitted";
pp " Proof.";
for i = 0 to size do
pp "  destruct n. apply spec_reduce_%i." i;
done;
pp "  apply spec_reduce_n.";
pp " Qed.";
pr "";

  pr " (***************************************************************)";
  pr " (*                                                             *)";
  pr " (** *                        Comparison                        *)";
  pr " (*                                                             *)";
  pr " (***************************************************************)";
  pr "";

  for i = 0 to size do
    pr " Definition compare_%i := ZnZ.compare (Ops:=w%i_op)." i i;
    pr " Definition comparen_%i :=" i;
    pr "  compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i
  done;
  pr "";

  pr " Definition comparenm n m wx wy :=";
  pr "    let mn := Max.max n m in";
  pr "    let d := diff n m in";
  pr "    let op := make_op mn in";
  pr "    ZnZ.compare";
  pr "       (castm (diff_r n m) (extend_tr wx (snd d)))";
  pr "       (castm (diff_l n m) (extend_tr wy (fst d))).";
  pr "";

  pr " Local Notation compare_folded :=";
  pr "   (iter _";
  for i = 0 to size do
    pr "      compare_%i" i;
    pr "      (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
    pr "      (fun n => comparen_%i (S n))" i;
  done;
  pr "      comparenm).";
  pr " Definition compare : t -> t -> comparison :=";
  pr "  Eval lazy beta delta [iter] in compare_folded.";
  pr "";

  for i = 0 to size do
    pp " Let spec_compare_%i: forall x y," i;
    pp "  compare_%i x y = Zcompare [%s%i x] [%s%i y]." i c i c i;
    pp " Proof.";
    pp "  unfold compare_%i, to_Z; exact ZnZ.spec_compare." i;
    pp " Qed.";
    pp "";

    pp "  Let spec_comparen_%i:" i;
    pp "  forall (n : nat) (x : word w%i n) (y : w%i)," i i;
    pp "   comparen_%i n x y = Zcompare (eval%in n x) [%s%i y]." i i c i;
    pp "  Proof.";
    pp "  intros n x y.";
    pp "  unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i;
    pp "  apply spec_compare_mn_1.";
    pp "  exact ZnZ.spec_0.";
    pp "  intros x1; exact (ZnZ.spec_compare %s x1)." (pz i);
    pp "  exact ZnZ.spec_to_Z.";
    pp "  exact ZnZ.spec_compare.";
    pp "  exact ZnZ.spec_compare.";
    pp "  exact ZnZ.spec_to_Z.";
    pp "  Qed.";
    pp "";
  done;

  pr " Theorem spec_compare : forall x y,";
  pr "   compare x y = Zcompare [x] [y].";
  pa " Admitted.";
  pp " Proof.";
  pp "  intros x y. change compare with compare_folded. apply spec_iter; clear x y.";
  for i = 0 to size - 1 do
    pp "  exact spec_compare_%i." i;
    pp "  intros n x y H; rewrite spec_comparen_%i; apply Zcompare_antisym." i;
    pp "  intros n x y H; exact (spec_comparen_%i (S n) x y)." i;
  done;
  pp "  exact spec_compare_%i." size;
  pp "  intros n x y; rewrite spec_comparen_%i; apply Zcompare_antisym." size;
  pp "  intros n; exact (spec_comparen_%i (S n))." size;
  pp "  intros n m x y; unfold comparenm.";
  pp "  rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y).";
  pp "  unfold to_Z; apply ZnZ.spec_compare.";
  pp " Qed.";
  pr "";

  pr " (***************************************************************)";
  pr " (*                                                             *)";
  pr " (** *                        Multiplication                    *)";
  pr " (*                                                             *)";
  pr " (***************************************************************)";
  pr "";

  for i = 0 to size do
    pr " Definition w%i_mul_add :=" i;
    pr "   Eval lazy beta delta [w_mul_add] in";
    pr "     @w_mul_add w%i %s ZnZ.succ ZnZ.add_c ZnZ.mul_c." i (pz i)
  done;
  pr "";

  for i = 0 to size do
    pr " Definition w%i_0W := ZnZ.OW (ops:=w%i_op)." i i
  done;
  pr "";

  for i = 0 to size do
    pr " Definition w%i_WW := ZnZ.WW (ops:=w%i_op)." i i
  done;
  pr "";

  for i = 0 to size do
    pr " Definition w%i_mul_add_n1 :=" i;
    pr "  @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add."  i (pz i) i i i
  done;
  pr "";

  for i = 0 to size - 1 do
    pr "  Let to_Z%i n :=" i;
    pr "  match n return word w%i (S n) -> t_ with" i;
    for j = 0 to size - i do
      if (i + j) == size then
        begin
          pr "  | %i%s => fun x => %sn 0 x" j "%nat" c;
          pr "  | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
        end
      else
        pr "  | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1)
    done;
    pr   "  | _   => fun _ => N0 ZnZ.zero";
    pr "  end.";
    pr "";
  done;


  for i = 0 to size - 1 do
    pp "Theorem to_Z%i_spec:" i;
    pp "  forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i;
    for j = 1 to size + 2 - i do
      pp " intros n; case n; clear n.";
      pp "   unfold to_Z%i." i;
      pp "   intros x H; rewrite spec_eval%in%i; auto." i j;
    done;
    pp " intros n x.";
    pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
    pp " Qed.";
    pp "";
  done;


  for i = 0 to size do
    pr " Definition w%i_mul n x y :=" i;
    pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i);
    if i == size then
      begin
        pr " if ZnZ.eq0 w then %sn n r" c;
        pr " else %sn (S n) (WW (extend%i n w) r)." c i;
      end
    else
      begin
        pr " if ZnZ.eq0 w then to_Z%i n r" i;
        pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i;
      end;
    pr "";
  done;

  pr " Definition mulnm n m x y :=";
  pr "    let mn := Max.max n m in";
  pr "    let d := diff n m in";
  pr "    let op := make_op mn in";
  pr "     reduce_n (S mn) (ZnZ.mul_c";
  pr "       (castm (diff_r n m) (extend_tr x (snd d)))";
  pr "       (castm (diff_l n m) (extend_tr y (fst d)))).";
  pr "";

  pr " Local Notation mul_folded :=";
  pr "  (iter0 t_";
  for i = 0 to size do
    pr "    (fun x y => reduce_%i (ZnZ.mul_c x y))" (i + 1);
    pr "    (fun n x y => w%i_mul n y x)" i;
    pr "    w%i_mul" i;
  done;
  pr "    mulnm";
  pr "    (fun _ => N0 ZnZ.zero)";
  pr "    (fun _ => N0 ZnZ.zero)";
  pr "  ).";
  pr " Definition mul : t -> t -> t :=";
  pr "  Eval lazy beta delta [iter0] in mul_folded.";
  pr "";
  for i = 0 to size do
    pp " Let spec_w%i_mul_add: forall x y z," i;
    pp "  let (q,r) := w%i_mul_add x y z in" i;
    pp "  ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits w%i_op))  +  ZnZ.to_Z (Ops:=w%i_op) r =" i i i;
    pp "  ZnZ.to_Z (Ops:=w%i_op) x * ZnZ.to_Z (Ops:=w%i_op) y + ZnZ.to_Z (Ops:=w%i_op) z :=" i i i ;
    pp "   spec_mul_add.";
    pp "";
  done;

  for i = 0 to size do
    pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i;
    pp "  let (q,r) := w%i_mul_add_n1 n x y z in" i;
    pp "  ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits (nmake_op _ w%i_op n)))  +" i i;
    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) r =" i;
    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) x * ZnZ.to_Z (Ops:=w%i_op) y +" i i;
    pp "  ZnZ.to_Z (Ops:=w%i_op) z." i;
    pp " Proof.";
    pp " intros n x y z; unfold w%i_mul_add_n1." i;
    pp " rewrite nmake_double.";
    pp " rewrite digits_doubled.";
    pp " change (base (DoubleBase.double_digits (ZnZ.digits w%i_op) n)) with" i;
    pp "        (DoubleBase.double_wB (ZnZ.digits w%i_op) n)." i;
    pp " apply spec_double_mul_add_n1; auto.";
    if i == 0 then pp " exact ZnZ.spec_0.";
    pp " exact ZnZ.spec_WW.";
    pp " exact ZnZ.spec_OW.";
    pp " exact spec_mul_add.";
    pp " Qed.";
    pp "";
  done;

  pp "  Lemma nmake_op_WW: forall ww ww1 n x y,";
  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 (S n)) (WW x y) =";
  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 n) x * base (ZnZ.digits (nmake_op ww ww1 n)) +";
  pp "    ZnZ.to_Z (Ops:=nmake_op ww ww1 n) y.";
  pp "  Proof.";
  pp "    auto.";
  pp "  Qed.";
  pp "";

  for i = 0 to size do
    pp "  Lemma extend%in_spec: forall n x1," i;
    pp "  ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i;
    pp "  ZnZ.to_Z (Ops:=w%i_op) x1." i;
    pp "  Proof.";
    pp "    intros n1 x2; rewrite nmake_double.";
    pp "    unfold extend%i." i;
    pp "    rewrite DoubleBase.spec_extend; auto.";
    if i == 0 then
      pp "    intros l; simpl; rewrite ZnZ.spec_0; ring.";
    pp "  Qed.";
    pp "";
  done;

  pp "  Lemma spec_muln:";
  pp "    forall n (x: word _ (S n)) y,";
  pp "     [%sn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [%sn n x] * [%sn n y]." c c c;
  pp "  Proof.";
  pp "    intros n x y; unfold to_Z.";
  pp "    rewrite <- ZnZ.spec_mul_c.";
  pp "    rewrite make_op_S.";
  pp "    case ZnZ.mul_c; auto.";
  pp "  Qed.";
  pr "";

  pr "  Theorem spec_mul: forall x y, [mul x y] = [x] * [y].";
  pa "  Admitted.";
  pp "  Proof.";
  for i = 0 to size do
    pp "    assert(F%i:" i;
    pp "    forall n x y,";
    if i <> size then
      pp0 "    Z_of_nat n <= %i -> "   (size - i);
    pp "    [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i;
    if i == size then
      pp "    intros n x y; unfold w%i_mul." i
    else
      pp "    intros n x y H; unfold w%i_mul." i;
    pp "    generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i);
    pp "    case w%i_mul_add_n1; intros x1 y1." i;
    pp "    change (ZnZ.to_Z x) with (eval%in (S n) x)." i;
    pp "    change (ZnZ.to_Z y) with ([%s%i y])." c i;
    if i == 0 then
      pp "    rewrite ZnZ.spec_0; rewrite Zplus_0_r."
    else
      pp "    change (ZnZ.to_Z W0) with 0; rewrite Zplus_0_r.";
    pp "    intros H1; rewrite <- H1; clear H1.";
    pp "    generalize (ZnZ.spec_eq0 x1); case ZnZ.eq0; intros HH.";
    pp "    unfold to_Z in HH; rewrite HH by trivial.";
    if i == size then
      begin
        pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i;
        pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i
      end
    else
      begin
        pp "    rewrite to_Z%i_spec; auto with zarith." i;
        pp "    rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i
      end;
    pp "    rewrite nmake_op_WW; rewrite extend%in_spec; auto." i;
  done;
  pp "    intros x y. change mul with mul_folded. apply spec_iter0; clear x y.";
  for i = 0 to size do
    pp "    intros x y; rewrite spec_reduce_%i." (i + 1);
    pp "    unfold to_Z.";
    pp "    generalize (ZnZ.spec_mul_c x y).";
    pp "    intros HH; rewrite <- HH; clear HH; auto.";
    if i == size then
      begin
        pp "    intros n x y; rewrite F%i; auto with zarith." i;
        pp "    intros n x y; rewrite F%i; auto with zarith." i;
      end
    else
      begin
        pp "    intros n x y H; rewrite F%i; auto with zarith." i;
        pp "    intros n x y H; rewrite F%i; auto with zarith." i;
      end;
  done;
  pp "    intros n m x y; unfold mulnm.";
  pp "    rewrite spec_reduce_n.";
  pp "    rewrite <- (spec_cast_l n m x).";
  pp "    rewrite <- (spec_cast_r n m y).";
  pp "    rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto.";
  pp "    intros x; simpl; rewrite ZnZ.spec_0; ring.";
  pp "    intros x; simpl; rewrite ZnZ.spec_0; ring.";
  pp "  Qed.";
  pr "";

  pr " (***************************************************************)";
  pr " (*                                                             *)";
  pr " (** *                        Division                          *)";
  pr " (*                                                             *)";
  pr " (***************************************************************)";
  pr "";

  pp " Let spec_divn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs ww_op) :=";
  pp "   (spec_double_divn1";
  pp "    (ZnZ.zdigits ww_op) ZnZ.zero";
  pp "    ZnZ.WW ZnZ.head0";
  pp "    ZnZ.add_mul_div ZnZ.div21";
  pp "    ZnZ.compare ZnZ.sub ZnZ.to_Z";
  pp "    ZnZ.spec_to_Z";
  pp "    ZnZ.spec_zdigits";
  pp "    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0";
  pp "    ZnZ.spec_add_mul_div ZnZ.spec_div21";
  pp "    ZnZ.spec_compare ZnZ.spec_sub).";
  pp "";

  for i = 0 to size do
    pr " Definition w%i_divn1 n x y :="  i;
    pr "  let (u, v) :=";
    pr "  double_divn1 (ZnZ.zdigits w%i_op) ZnZ.zero" i;
    pr "    ZnZ.WW ZnZ.head0";
    pr "    ZnZ.add_mul_div ZnZ.div21";
    pr "    ZnZ.compare ZnZ.sub (S n) x y in";
    if i == size then
      pr "   (%sn _ u, %s%i v)." c c i
    else
      pr "   (to_Z%i _ u, %s%i v)." i c i;
    pr "";
  done;

  for i = 0 to size do
    pp " Lemma spec_get_end%i: forall n x y," i;
    pp "    eval%in n x  <= [%s%i y] ->" i c i;
    pp "     [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i;
    pp " Proof.";
    pp " intros n x y H.";
    pp " rewrite spec_double_eval%in; unfold to_Z." i;
    pp " apply DoubleBase.spec_get_low.";
    pp " exact ZnZ.spec_0.";
    pp " exact ZnZ.spec_to_Z.";
    pp " apply Zle_lt_trans with [%s%i y]; auto." c i;
    pp "   rewrite <- spec_double_eval%in; auto." i;
    pp " unfold to_Z; case (ZnZ.spec_to_Z y); auto.";
    pp " Qed.";
    pp "";
  done;

  for i = 0 to size do
    pr " Let div_gt%i (x y:w%i) := let (u,v) := ZnZ.div_gt x y in (reduce_%i u, reduce_%i v)." i i i i;
  done;
  pr "";


  pr " Let div_gtnm n m wx wy :=";
  pr "    let mn := Max.max n m in";
  pr "    let d := diff n m in";
  pr "    let op := make_op mn in";
  pr "    let (q, r):= ZnZ.div_gt";
  pr "         (castm (diff_r n m) (extend_tr wx (snd d)))";
  pr "         (castm (diff_l n m) (extend_tr wy (fst d))) in";
  pr "    (reduce_n mn q, reduce_n mn r).";
  pr "";

  pr " Local Notation div_gt_folded :=";
  pr "   (iter _";
  for i = 0 to size do
    pr "      div_gt%i" i;
    pr "      (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
    pr "      w%i_divn1" i;
  done;
  pr "      div_gtnm).";
  pr " Definition div_gt := Eval lazy beta delta [iter] in div_gt_folded.";
  pr "";

  pr " Theorem spec_div_gt: forall x y,";
  pr "       [x] > [y] -> 0 < [y] ->";
  pr "      let (q,r) := div_gt x y in";
  pr "      [q] = [x] / [y] /\\ [r] = [x] mod [y].";
  pa " Admitted.";
  pp " Proof.";
  pp " assert (FO:";
  pp "   forall x y, [x] > [y] -> 0 < [y] ->";
  pp "      let (q,r) := div_gt x y in";
  pp "      [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y]).";
  pp "   intros x y. change div_gt with div_gt_folded. apply spec_iter; clear x y.";
  for i = 0 to size do
    pp "   (* %i *)" i;
    pp "   intros x y H1 H2; unfold div_gt%i." i;
    pp "    generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt.";
    pp "    intros xx yy; repeat rewrite spec_reduce_%i; auto." i;
    if i == size then
     pp "   intros n x y H2 H3; unfold div_gt%i." i
    else
     pp "   intros n x y H1 H2 H3; unfold div_gt%i." i;
    pp "    generalize (ZnZ.spec_div_gt x";
    pp "                (DoubleBase.get_low %s (S n) y))." (pz i);
    pp "    case ZnZ.div_gt.";
    pp "    intros xx yy H4; repeat rewrite spec_reduce_%i." i;
    pp "    generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i;
    pp "    unfold to_Z in H2; rewrite H5 in H4; auto with zarith.";
    if i == size then
     pp "   intros n x y H2 H3."
    else
     pp "   intros n x y H1 H2 H3.";
    pp "    generalize";
    pp "     (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i;
    pp "    unfold w%i_divn1; case double_divn1." i;
    pp "    intros xx yy H4.";
    if i == size then
      begin
        pp "    repeat rewrite <- spec_double_eval%in in H4; auto." i;
        pp "    rewrite spec_eval%in; auto." i;
      end
    else
      begin
        pp "    rewrite to_Z%i_spec; auto with zarith." i;
        pp "    repeat rewrite <- spec_double_eval%in in H4; auto." i;
      end;
  done;
  pp "    intros n m x y H1 H2; unfold div_gtnm.";
  pp "    generalize (ZnZ.spec_div_gt";
  pp "                   (castm (diff_r n m)";
  pp "                     (extend_tr x (snd (diff n m))))";
  pp "                   (castm (diff_l n m)";
  pp "                     (extend_tr y (fst (diff n m))))).";
  pp "    case ZnZ.div_gt.";
  pp "    intros xx yy HH.";
  pp "    repeat rewrite spec_reduce_n.";
  pp "    rewrite <- (spec_cast_l n m x).";
  pp "    rewrite <- (spec_cast_r n m y).";
  pp "    unfold to_Z; apply HH.";
  pp "    rewrite <- (spec_cast_l n m x) in H1; auto.";
  pp "    rewrite <- (spec_cast_r n m y) in H1; auto.";
  pp "    rewrite <- (spec_cast_r n m y) in H2; auto.";
  pp "  intros x y H1 H2; generalize (FO x y H1 H2); case div_gt.";
  pp "  intros q r (H3, H4); split.";
  pp "  apply (Zdiv_unique [x] [y] [q] [r]); auto.";
  pp "  rewrite Zmult_comm; auto.";
  pp "  apply (Zmod_unique [x] [y] [q] [r]); auto.";
  pp "  rewrite Zmult_comm; auto.";
  pp "  Qed.";
  pr "";

  pr " (***************************************************************)";
  pr " (*                                                             *)";
  pr " (** *                        Modulo                            *)";
  pr " (*                                                             *)";
  pr " (***************************************************************)";
  pr "";

  for i = 0 to size do
    pr " Definition w%i_modn1 :=" i;
    pr "  double_modn1 (ZnZ.zdigits w%i_op) (ZnZ.zero (Ops:=w%i_op))" i i;
    pr "    ZnZ.head0 ZnZ.add_mul_div ZnZ.div21";
    pr "    ZnZ.compare ZnZ.sub.";
  done;
  pr "";

  pr " Let mod_gtnm n m wx wy :=";
  pr "    let mn := Max.max n m in";
  pr "    let d := diff n m in";
  pr "    let op := make_op mn in";
  pr "    reduce_n mn (ZnZ.modulo_gt";
  pr "         (castm (diff_r n m) (extend_tr wx (snd d)))";
  pr "         (castm (diff_l n m) (extend_tr wy (fst d)))).";
  pr "";

  pr " Local Notation mod_gt_folded :=";
  pr "   (iter _";
  for i = 0 to size do
    pr "      (fun x y => reduce_%i (ZnZ.modulo_gt x y))" i;
    pr "      (fun n x y => reduce_%i (ZnZ.modulo_gt x (DoubleBase.get_low %s (S n) y)))" i (pz i);
    pr "      (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i;
  done;
  pr "      mod_gtnm).";
  pr " Definition mod_gt := Eval lazy beta delta[iter] in mod_gt_folded.";
  pr "";

  pp " Let spec_modn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs ww_op) :=";
  pp "   spec_double_modn1";
  pp "    (ZnZ.zdigits ww_op) ZnZ.zero";
  pp "    ZnZ.WW ZnZ.head0";
  pp "    ZnZ.add_mul_div ZnZ.div21";
  pp "    ZnZ.compare ZnZ.sub ZnZ.to_Z";
  pp "    ZnZ.spec_to_Z";
  pp "    ZnZ.spec_zdigits";
  pp "    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0";
  pp "    ZnZ.spec_add_mul_div ZnZ.spec_div21";
  pp "    ZnZ.spec_compare ZnZ.spec_sub.";
  pp "";

  pr " Theorem spec_mod_gt:";
  pr "   forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].";
  pa " Admitted.";
  pp " Proof.";
  pp " intros x y. change mod_gt with mod_gt_folded. apply spec_iter; clear x y.";
  for i = 0 to size do
    pp " intros x y H1 H2; rewrite spec_reduce_%i." i;
    pp "   exact (ZnZ.spec_modulo_gt x y H1 H2).";
    if i == size then
      pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
    else
      pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
    pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i;
    pp " unfold to_Z; apply ZnZ.spec_modulo_gt; auto.";
    pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i;
    pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i;
    if i == size then
      pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
    else
      pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
    pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i;
    pp " apply (spec_modn1 _ _ w%i_spec); auto." i;
  done;
  pp " intros n m x y H1 H2; unfold mod_gtnm.";
  pp "    repeat rewrite spec_reduce_n.";
  pp "    rewrite <- (spec_cast_l n m x).";
  pp "    rewrite <- (spec_cast_r n m y).";
  pp "    unfold to_Z; apply ZnZ.spec_modulo_gt.";
  pp "    rewrite <- (spec_cast_l n m x) in H1; auto.";
  pp "    rewrite <- (spec_cast_r n m y) in H1; auto.";
  pp "    rewrite <- (spec_cast_r n m y) in H2; auto.";
  pp " Qed.";
  pr "";

  pr "End Make.";
  pr "";