Merge branch 'experimental/upstream' into upstream

1 files changed, 192 insertions, 131 deletions

diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index cdd41647..5bde1008 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,9 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: Nbasic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import Max.
 Require Import DoubleType.
@@ -18,44 +16,64 @@ Require Import DoubleBase.
 Require Import CyclicAxioms.
 Require Import DoubleCyclic.
 
+Arguments mk_zn2z_ops [t] ops.
+Arguments mk_zn2z_ops_karatsuba [t] ops.
+Arguments mk_zn2z_specs [t ops] specs.
+Arguments mk_zn2z_specs_karatsuba [t ops] specs.
+Arguments ZnZ.digits [t] Ops.
+Arguments ZnZ.zdigits [t] Ops.
+
+Lemma Pshiftl_nat_Zpower : forall n p,
+  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
+Proof.
+ intros.
+ rewrite Z.mul_comm.
+ induction n. simpl; auto.
+ transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
+ rewrite <- IHn. auto.
+ rewrite Z.mul_assoc.
+ rewrite Nat2Z.inj_succ.
+ rewrite <- Z.pow_succ_r; auto with zarith.
+Qed.
+
 (* To compute the necessary height *)
 
 Fixpoint plength (p: positive) : positive :=
   match p with
     xH => xH
-  | xO p1 => Psucc (plength p1)
-  | xI p1 => Psucc (plength p1)
+  | xO p1 => Pos.succ (plength p1)
+  | xI p1 => Pos.succ (plength p1)
   end.
 
 Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
-assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
-intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
+assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z).
+intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z.
 rewrite Zpower_exp; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
 intros p; elim p; simpl plength; auto.
-intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
+intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI.
 assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
-intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
+intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1).
 assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
 Qed.
 
-Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
-intros p; case (Psucc_pred p); intros H1.
+Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z.
+intros p; case (Pos.succ_pred_or p); intros H1.
 subst; simpl plength.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
 pattern p at 1; rewrite <- H1.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
-generalize (plength_correct (Ppred p)); auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
+generalize (plength_correct (Pos.pred p)); auto with zarith.
 Qed.
 
 Definition Pdiv p q :=
-  match Zdiv (Zpos p) (Zpos q) with
+  match Z.div (Zpos p) (Zpos q) with
     Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
                  Z0 => q1
-               | _ => (Psucc q1)
+               | _ => (Pos.succ q1)
                end
   |  _ => xH
   end.
@@ -67,20 +85,20 @@ unfold Pdiv.
 assert (H1: Zpos q > 0); auto with zarith.
 assert (H1b: Zpos p >= 0); auto with zarith.
 generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b).
-generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv.
-  intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl.
+generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Z.div.
+  intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl.
 case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
 intros q1 H2.
 replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
   2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
 generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2;
-  case Zmod.
+  case Z.modulo.
   intros HH _; rewrite HH; auto with zarith.
-  intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
-  unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith.
+  intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ.
+  unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith.
   intros r1 _ (HH,_); case HH; auto.
 intros q1 HH; rewrite HH.
-unfold Zge; simpl Zcompare; intros HH1; case HH1; auto.
+unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto.
 Qed.
 
 Definition is_one p := match p with xH => true | _ => false end.
@@ -91,7 +109,7 @@ Qed.
 
 Definition get_height digits p :=
   let r := Pdiv p digits in
-   if is_one r then xH else Psucc (plength (Ppred r)).
+   if is_one r then xH else Pos.succ (plength (Pos.pred r)).
 
 Theorem get_height_correct:
   forall digits N,
@@ -101,13 +119,13 @@ unfold get_height.
 assert (H1 := Pdiv_le N digits).
 case_eq (is_one (Pdiv N digits)); intros H2.
 rewrite (is_one_one _ H2) in H1.
-rewrite Zmult_1_r in H1.
-change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto.
+rewrite Z.mul_1_r in H1.
+change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto.
 clear H2.
-apply Zle_trans with (1 := H1).
-apply Zmult_le_compat_l; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc.
-rewrite Zplus_comm; rewrite Zminus_plus.
+apply Z.le_trans with (1 := H1).
+apply Z.mul_le_mono_nonneg_l; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ.
+rewrite Z.add_comm; rewrite Z.add_simpl_l.
 apply plength_pred_correct.
 Qed.
 
@@ -134,18 +152,18 @@ Open Scope nat_scope.
 
 Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
   match n return  (n + S m = S (n + m))%nat with
-  | 0 => refl_equal (S m)
+  | 0 => eq_refl (S m)
   | S n1 =>
       let v := S (S n1 + m) in
-      eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
+      eq_ind_r (fun n => S n = v) (eq_refl v) (plusnS n1 m)
   end.
 
 Fixpoint plusn0 n : n + 0 = n :=
   match n return (n + 0 = n) with
-  | 0 => refl_equal 0
+  | 0 => eq_refl 0
   | S n1 =>
       let v := S n1 in
-      eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
+      eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1)
   end.
 
  Fixpoint diff (m n: nat) {struct m}: nat * nat :=
@@ -159,8 +177,8 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
   match m return fst (diff m n) + n = max m n with
   | 0 =>
       match n return (n = max 0 n) with
-      | 0 => refl_equal _
-      | S n0 => refl_equal _
+      | 0 => eq_refl _
+      | S n0 => eq_refl _
       end
   | S m1 =>
       match n return (fst (diff (S m1) n) + n = max (S m1) n)
@@ -170,7 +188,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
           let v := fst (diff m1 n1) + n1 in
           let v1 := fst (diff m1 n1) + S n1 in
           eq_ind v (fun n => v1 = S n)
-            (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
+            (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _))
             _ (diff_l _ _)
       end
   end.
@@ -179,17 +197,17 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
   match m return (snd (diff m n) + m = max m n) with
   | 0 =>
       match n return (snd (diff 0 n) + 0 = max 0 n) with
-      | 0 => refl_equal _
+      | 0 => eq_refl _
       | S _ => plusn0 _
       end
   | S m =>
       match n return (snd (diff (S m) n) + S m = max (S m) n) with
-      | 0 => refl_equal (snd (diff (S m) 0) + S m)
+      | 0 => eq_refl (snd (diff (S m) 0) + S m)
       | S n1 =>
           let v := S (max m n1) in
           eq_ind_r (fun n => n = v)
             (eq_ind_r (fun n => S n = v)
-               (refl_equal v) (diff_r _ _)) (plusnS _ _)
+               (eq_refl v) (diff_r _ _)) (plusnS _ _)
       end
   end.
 
@@ -198,7 +216,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
  Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
      (word w (S n)) :=
  match H in (_ = y) return (word w (S y)) with
- | refl_equal => x
+ | eq_refl => x
  end.
 
 Variable m: nat.
@@ -212,8 +230,8 @@ Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
 
 End ExtendMax.
 
-Implicit Arguments extend_tr[w m].
-Implicit Arguments castm[w m n].
+Arguments extend_tr [w m] v n.
+Arguments castm     [w m n] H x.
 
 
 
@@ -287,11 +305,7 @@ Section CompareRec.
  Variable w_to_Z: w -> Z.
  Variable w_to_Z_0: w_to_Z w_0 = 0.
  Variable spec_compare0_m: forall x,
-    match compare0_m x with
-      Eq => w_to_Z w_0 = wm_to_Z x
-    | Lt => w_to_Z w_0 < wm_to_Z x
-    | Gt => w_to_Z w_0 > wm_to_Z x
-    end.
+   compare0_m x = (w_to_Z w_0 ?= wm_to_Z x).
  Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.
 
  Let double_to_Z := double_to_Z wm_base wm_to_Z.
@@ -300,7 +314,7 @@ Section CompareRec.
  Lemma base_xO: forall n, base (xO n) = (base n)^2.
  Proof.
  intros n1; unfold base.
- rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
+ rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith.
  Qed.
 
  Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
@@ -308,29 +322,25 @@ Section CompareRec.
 
 
  Lemma spec_compare0_mn: forall n x,
-    match compare0_mn n x with
-      Eq => 0 = double_to_Z n x
-    | Lt => 0 < double_to_Z n x
-    | Gt => 0 > double_to_Z n x
-    end.
-  Proof.
+   compare0_mn n x = (0 ?= double_to_Z n x).
+ Proof.
   intros n; elim n; clear n; auto.
-  intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto.
+  intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto.
   intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
+  fold word in *.
   intros xh xl.
-  generalize (Hrec xh); case compare0_mn; auto.
-  generalize (Hrec xl); case compare0_mn; auto.
-  simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto.
-  simpl double_to_Z; intros H1 H2; rewrite <- H2; auto.
+  rewrite 2 Hrec.
+  simpl double_to_Z.
+  set (wB := DoubleBase.double_wB wm_base n).
+  case Z.compare_spec; intros Cmp.
+  rewrite <- Cmp. reflexivity.
+  symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *)
+  assert (0 < wB).
+   unfold wB, DoubleBase.double_wB, base; auto with zarith.
+  change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith.
+  apply Z.mul_pos_pos; auto with zarith.
   case (double_to_Z_pos n xl); auto with zarith.
-  intros H1; simpl double_to_Z.
-  set (u := DoubleBase.double_wB wm_base n).
-  case (double_to_Z_pos n xl); intros H2 H3.
-  assert (0 < u); auto with zarith.
-  unfold u, DoubleBase.double_wB, base; auto with zarith.
-  change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith.
-  apply Zmult_lt_0_compat; auto with zarith.
-  case (double_to_Z_pos n xh); auto with zarith.
+  case (double_to_Z_pos n xh); intros; exfalso; omega.
   Qed.
 
  Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
@@ -348,17 +358,9 @@ Section CompareRec.
   end.
 
  Variable spec_compare: forall x y,
-   match compare x y with
-     Eq => w_to_Z x = w_to_Z y
-   | Lt => w_to_Z x < w_to_Z y
-   | Gt => w_to_Z x > w_to_Z y
-   end.
+   compare x y = Z.compare (w_to_Z x) (w_to_Z y).
  Variable spec_compare_m: forall x y,
-   match compare_m x y with
-     Eq => wm_to_Z x = w_to_Z y
-   | Lt => wm_to_Z x < w_to_Z y
-   | Gt => wm_to_Z x > w_to_Z y
-   end.
+   compare_m x y = Z.compare (wm_to_Z x) (w_to_Z y).
  Variable wm_base_lt: forall x,
    0 <= w_to_Z x < base (wm_base).
 
@@ -367,39 +369,36 @@ Section CompareRec.
  Proof.
  intros n x; elim n; simpl; auto; clear n.
  intros n (H0, H); split; auto.
- apply Zlt_le_trans with (1:= H).
+ apply Z.lt_le_trans with (1:= H).
  unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite base_xO.
- set (u := base (double_digits wm_base n)).
+ rewrite Pshiftl_nat_S, base_xO.
+ set (u := base (Pos.shiftl_nat wm_base n)).
  assert (0 < u).
   unfold u, base; auto with zarith.
  replace (u^2) with (u * u); simpl; auto with zarith.
- apply Zle_trans with (1 * u); auto with zarith.
- unfold Zpower_pos; simpl; ring.
+ apply Z.le_trans with (1 * u); auto with zarith.
+ unfold Z.pow_pos; simpl; ring.
  Qed.
 
 
  Lemma spec_compare_mn_1: forall n x y,
-   match compare_mn_1 n x y with
-     Eq => double_to_Z n x = w_to_Z y
-   | Lt => double_to_Z n x < w_to_Z y
-   | Gt => double_to_Z n x > w_to_Z y
-   end.
+   compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y).
  Proof.
  intros n; elim n; simpl; auto; clear n.
  intros n Hrec x; case x; clear x; auto.
- intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto.
- intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b.
- rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto.
- apply Hrec.
- apply Zlt_gt.
+ intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity.
+ intros xh xl y; simpl;
+ rewrite spec_compare0_mn, Hrec. case Z.compare_spec.
+ intros H1b.
+ rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto.
+ symmetry. apply Z.lt_gt.
  case (double_wB_lt n y); intros _ H0.
- apply Zlt_le_trans with (1:= H0).
+ apply Z.lt_le_trans with (1:= H0).
  fold double_wB.
  case (double_to_Z_pos n xl); intros H1 H2.
- apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith.
- apply Zle_trans with (1 * double_wB n); auto with zarith.
- case (double_to_Z_pos n xh); auto with zarith.
+ apply Z.le_trans with (double_to_Z n xh * double_wB n); auto with zarith.
+ apply Z.le_trans with (1 * double_wB n); auto with zarith.
+ case (double_to_Z_pos n xh); intros; exfalso; omega.
  Qed.
 
 End CompareRec.
@@ -433,22 +432,6 @@ Section AddS.
 
 End AddS.
 
-
- Lemma spec_opp: forall u x y,
-  match u with
-  | Eq => y = x
-  | Lt => y < x
-  | Gt => y > x
-  end ->
-  match CompOpp u with
-  | Eq => x = y
-  | Lt => x < y
-  | Gt => x > y
-  end.
- Proof.
- intros u x y; case u; simpl; auto with zarith.
- Qed.
-
  Fixpoint length_pos x :=
   match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.
 
@@ -457,8 +440,8 @@ End AddS.
  Proof.
  intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
    intros y; case y; clear y; intros y1 H || intros H; simpl length_pos;
-   try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
-   try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
+   try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1));
+   try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1));
    try (inversion H; fail);
    try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith);
    assert (0 < Zpos y1); auto with zarith; red; auto.
@@ -474,34 +457,112 @@ End AddS.
 
  Variable w: Type.
 
- Theorem digits_zop: forall w (x: znz_op w),
-  znz_digits (mk_zn2z_op x) = xO (znz_digits x).
+ Theorem digits_zop: forall t (ops : ZnZ.Ops t),
+  ZnZ.digits (mk_zn2z_ops ops) = xO (ZnZ.digits ops).
+ Proof.
  intros ww x; auto.
  Qed.
 
- Theorem digits_kzop: forall w (x: znz_op w),
-  znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x).
+ Theorem digits_kzop: forall t (ops : ZnZ.Ops t),
+  ZnZ.digits (mk_zn2z_ops_karatsuba ops) = xO (ZnZ.digits ops).
+ Proof.
  intros ww x; auto.
  Qed.
 
- Theorem make_zop: forall w (x: znz_op w),
-  znz_to_Z (mk_zn2z_op x) =
+ Theorem make_zop: forall t (ops : ZnZ.Ops t),
+  @ZnZ.to_Z _ (mk_zn2z_ops ops) =
     fun z => match z with
-                W0 => 0
-             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
-                                + znz_to_Z x xl
+             | W0 => 0
+             | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops)
+                                + ZnZ.to_Z xl
              end.
+ Proof.
  intros ww x; auto.
  Qed.
 
- Theorem make_kzop: forall w (x: znz_op w),
-  znz_to_Z (mk_zn2z_op_karatsuba x) =
+ Theorem make_kzop: forall t (ops: ZnZ.Ops t),
+  @ZnZ.to_Z _ (mk_zn2z_ops_karatsuba ops) =
     fun z => match z with
-                W0 => 0
-             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
-                                + znz_to_Z x xl
+             | W0 => 0
+             | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops)
+                                + ZnZ.to_Z xl
              end.
+ Proof.
  intros ww x; auto.
  Qed.
 
  End SimplOp.
+
+(** Abstract vision of a datatype of arbitrary-large numbers.
+    Concrete operations can be derived from these generic
+    fonctions, in particular from [iter_t] and [same_level].
+*)
+
+Module Type NAbstract.
+
+(** The domains: a sequence of [Z/nZ] structures *)
+
+Parameter dom_t : nat -> Type.
+Declare Instance dom_op n : ZnZ.Ops (dom_t n).
+Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
+
+Axiom digits_dom_op : forall n,
+  ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op 0)) n.
+
+(** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t]
+    and destructor [destr_t] and iterator [iter_t] *)
+
+Parameter t : Type.
+
+Parameter mk_t : forall (n:nat), dom_t n -> t.
+
+Inductive View_t : t -> Prop :=
+ Mk_t : forall n (x : dom_t n), View_t (mk_t n x).
+
+Axiom destr_t : forall x, View_t x. (* i.e. every x is a (mk_t n xw) *)
+
+Parameter iter_t : forall {A:Type}(f : forall n, dom_t n -> A), t -> A.
+
+Axiom 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.
+
+(** Conversion to [ZArith] *)
+
+Parameter to_Z : t -> Z.
+Local Notation "[ x ]" := (to_Z x).
+
+Axiom spec_mk_t : forall n x, [mk_t n x] = ZnZ.to_Z x.
+
+(** [reduce] is like [mk_t], but try to minimise the level of the number *)
+
+Parameter reduce : forall (n:nat), dom_t n -> t.
+Axiom spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
+
+(** Number of level in the tree representation of a number.
+    NB: This function isn't a morphism for setoid [eq]. *)
+
+Definition level := iter_t (fun n _ => n).
+
+(** [same_level] and its rich specification, indexed by [level] *)
+
+Parameter same_level : forall {A:Type}
+ (f : forall n, dom_t n -> dom_t n -> A), t -> t -> A.
+
+Axiom 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 x) [x] [y] (same_level f x y).
+
+(** [mk_t_S] : building a number of the next level *)
+
+Parameter mk_t_S : forall (n:nat), zn2z (dom_t n) -> t.
+
+Axiom 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.
+
+Axiom mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
+
+End NAbstract.