Use the Int31 library with coq-8.5

7 files changed, 0 insertions, 3144 deletions

diff --git a/src/configure.sh b/src/configure.sh
index d83e20a..6e044a8 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -10,9 +10,6 @@ else
     cp versions/standard/Makefile Makefile
     cp versions/standard/smtcoq_plugin_standard.ml4 smtcoq_plugin.ml4
     cp versions/standard/Int63/Int63_standard.v versions/standard/Int63/Int63.v
-    cp versions/standard/Int63/Int63Lib_standard.v versions/standard/Int63/Int63Lib.v
-    cp versions/standard/Int63/Cyclic63_standard.v versions/standard/Int63/Cyclic63.v
-    cp versions/standard/Int63/Ring63_standard.v versions/standard/Int63/Ring63.v
     cp versions/standard/Int63/Int63Native_standard.v versions/standard/Int63/Int63Native.v
     cp versions/standard/Int63/Int63Op_standard.v versions/standard/Int63/Int63Op.v
     cp versions/standard/Int63/Int63Axioms_standard.v versions/standard/Int63/Int63Axioms.v
diff --git a/src/versions/standard/Int63/Cyclic63_standard.v b/src/versions/standard/Int63/Cyclic63_standard.v
deleted file mode 100644
index 3033781..0000000
--- a/src/versions/standard/Int63/Cyclic63_standard.v
+++ /dev/null
@@ -1,2522 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2016                                          *)
-(*                                                                        *)
-(*     Chantal Keller                                                     *)
-(*                                                                        *)
-(*       from the Int31 library                                           *)
-(*         by Arnaud Spiwack and Pierre Letouzey                          *)
-(*       and the Int63 library of native-coq                              *)
-(*         by Benjamin Gregoire and Laurent Thery                         *)
-(*                                                                        *)
-(*     Inria - École Polytechnique - Université Paris-Sud                 *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-(** * Int63 numbers defines indeed a cyclic structure : Z/(2^63)Z *)
-
-(* Add LoadPath "." as SMTCoq.versions.standard.Int63. *)
-Require Import List.
-Require Import Min.
-(* Require Export SMTCoq.versions.standard.Int63.Int63Lib. *)
-Require Export Int63Lib.
-Require Import Znumtheory.
-Require Import Zgcd_alt.
-Require Import Zpow_facts.
-Require Import BigNumPrelude.
-Require Import CyclicAxioms.
-Require Import ROmega.
-
-Local Open Scope nat_scope.
-Local Open Scope int63_scope.
-
-Section Basics.
-
- (** * Basic results about [iszero], [shiftl], [shiftr] *)
-
- Lemma iszero_eq0 : forall x, iszero x = true -> x=0.
- Proof.
- destruct x; simpl; intros.
- repeat
-   match goal with H:(if ?d then _ else _) = true |- _ =>
-     destruct d; try discriminate
-   end.
- reflexivity.
- Qed.
-
- Lemma iszero_not_eq0 : forall x, iszero x = false -> x<>0.
- Proof.
- intros x H Eq; rewrite Eq in H; simpl in *; discriminate.
- Qed.
-
- Lemma sneakl_shiftr : forall x,
-  x = sneakl (firstr x) (shiftr x).
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- Lemma sneakr_shiftl : forall x,
-  x = sneakr (firstl x) (shiftl x).
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- Lemma twice_zero : forall x,
-  twice x = 0 <-> twice_plus_one x = 1.
- Proof.
- destruct x; simpl in *; split;
- intro H; injection H; intros; subst; auto.
- Qed.
-
- Lemma twice_or_twice_plus_one : forall x,
-  x = twice (shiftr x) \/ x = twice_plus_one (shiftr x).
- Proof.
- intros; case_eq (firstr x); intros.
- destruct x; simpl in *; rewrite H; auto.
- destruct x; simpl in *; rewrite H; auto.
- Qed.
-
-
-
- (** * Iterated shift to the right *)
-
- Definition nshiftr x := nat_rect _ x (fun _ => shiftr).
-
- Lemma nshiftr_S :
-  forall n x, nshiftr x (S n) = shiftr (nshiftr x n).
- Proof.
- reflexivity.
- Qed.
-
- Lemma nshiftr_S_tail :
-  forall n x, nshiftr x (S n) = nshiftr (shiftr x) n.
- Proof.
- intros n; elim n; simpl; auto.
- intros; now f_equal.
- Qed.
-
- Lemma nshiftr_n_0 : forall n, nshiftr 0 n = 0.
- Proof.
- induction n; simpl; auto.
- rewrite IHn; auto.
- Qed.
-
- Lemma nshiftr_size : forall x, nshiftr x size = 0.
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- Lemma nshiftr_above_size : forall k x, size<=k ->
-  nshiftr x k = 0.
- Proof.
- intros.
- replace k with ((k-size)+size)%nat by omega.
- induction (k-size)%nat; auto.
-  rewrite nshiftr_size; auto.
-  simpl; rewrite IHn; auto.
- Qed.
-
- (** * Iterated shift to the left *)
-
- Definition nshiftl x := nat_rect _ x (fun _ => shiftl).
-
- Lemma nshiftl_S :
-  forall n x, nshiftl x (S n) = shiftl (nshiftl x n).
- Proof.
- reflexivity.
- Qed.
-
- Lemma nshiftl_S_tail :
-  forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof. 
- intros n; elim n; simpl; intros; now f_equal.
- Qed.
-
- Lemma nshiftl_n_0 : forall n, nshiftl 0 n = 0.
- Proof.
- induction n; simpl; auto.
- rewrite IHn; auto.
- Qed.
-
- Lemma nshiftl_size : forall x, nshiftl x size = 0.
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- Lemma nshiftl_above_size : forall k x, size<=k ->
-  nshiftl x k = 0.
- Proof.
- intros.
- replace k with ((k-size)+size)%nat by omega.
- induction (k-size)%nat; auto.
-  rewrite nshiftl_size; auto.
-  simpl; rewrite IHn; auto.
- Qed.
-
- Lemma firstr_firstl :
-  forall x, firstr x = firstl (nshiftl x (pred size)).
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- Lemma firstl_firstr :
-  forall x, firstl x = firstr (nshiftr x (pred size)).
- Proof.
- destruct x; simpl; auto.
- Qed.
-
- (** More advanced results about [nshiftr] *)
-
- Lemma nshiftr_predsize_0_firstl : forall x,
-  nshiftr x (pred size) = 0 -> firstl x = D0.
- Proof.
- destruct x; compute; intros H; injection H; intros; subst; auto.
- Qed.
-
- Lemma nshiftr_0_propagates : forall n p x, n <= p ->
-  nshiftr x n = 0 -> nshiftr x p = 0.
- Proof.
- intros.
- replace p with ((p-n)+n)%nat by omega.
- induction (p-n)%nat.
- simpl; auto.
- simpl; rewrite IHn0; auto.
- Qed.
-
- Lemma nshiftr_0_firstl : forall n x, n < size ->
-  nshiftr x n = 0 -> firstl x = D0.
- Proof.
- intros.
- apply nshiftr_predsize_0_firstl.
- apply nshiftr_0_propagates with n; auto; omega.
- Qed.
-
- (** * Some induction principles over [int63] *)
-
- (** Not used for the moment. Are they really useful ? *)
-
- Lemma int63_ind_sneakl : forall P : int63->Prop,
-  P 0 ->
-  (forall x d, P x -> P (sneakl d x)) ->
-  forall x, P x.
- Proof.
- intros.
- assert (forall n, n<=size -> P (nshiftr x (size - n))).
- induction n; intros.
- rewrite nshiftr_size; auto.
- rewrite sneakl_shiftr.
- apply H0.
- change (P (nshiftr x (S (size - S n)))).
- replace (S (size - S n))%nat with (size - n)%nat by omega.
- apply IHn; omega.
- change x with (nshiftr x (size-size)); auto.
- Qed.
-
- Lemma int63_ind_twice : forall P : int63->Prop,
-  P 0 ->
-  (forall x, P x -> P (twice x)) ->
-  (forall x, P x -> P (twice_plus_one x)) ->
-  forall x, P x.
- Proof.
- induction x using int63_ind_sneakl; auto.
- destruct d; auto.
- Qed.
-
-
- (** * Some generic results about [recr] *)
-
- Section Recr.
-
- (** [recr] satisfies the fixpoint equation used for its definition. *)
-
- Variable (A:Type)(case0:A)(caserec:digits->int63->A->A).
-
- Lemma recr_aux_eqn : forall n x, iszero x = false ->
-   recr_aux (S n) A case0 caserec x =
-   caserec (firstr x) (shiftr x) (recr_aux n A case0 caserec (shiftr x)).
- Proof.
- intros; simpl; rewrite H; auto.
- Qed.
-
- Lemma recr_aux_converges :
-  forall n p x, n <= size -> n <= p ->
-  recr_aux n A case0 caserec (nshiftr x (size - n)) =
-  recr_aux p A case0 caserec (nshiftr x (size - n)).
- Proof.
- induction n.
- simpl minus; intros.
- rewrite nshiftr_size; destruct p; simpl; auto.
- intros.
- destruct p.
- inversion H0.
- unfold recr_aux; fold recr_aux.
- destruct (iszero (nshiftr x (size - S n))); auto.
- f_equal.
- change (shiftr (nshiftr x (size - S n))) with (nshiftr x (S (size - S n))).
- replace (S (size - S n))%nat with (size - n)%nat by omega.
- apply IHn; auto with arith.
- Qed.
-
- Lemma recr_eqn : forall x, iszero x = false ->
-  recr A case0 caserec x =
-  caserec (firstr x) (shiftr x) (recr A case0 caserec (shiftr x)).
- Proof.
- intros.
- unfold recr.
- change x with (nshiftr x (size - size)).
- rewrite (recr_aux_converges size (S size)); auto with arith.
- rewrite recr_aux_eqn; auto.
- Qed.
-
- (** [recr] is usually equivalent to a variant [recrbis]
-     written without [iszero] check. *)
-
- Fixpoint recrbis_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
- (i:int63) : A :=
-  match n with
-  | O => case0
-  | S next =>
-      let si := shiftr i in
-      caserec (firstr i) si (recrbis_aux next A case0 caserec si)
-  end.
-
- Definition recrbis := recrbis_aux size.
-
- Hypothesis case0_caserec : caserec D0 0 case0 = case0.
-
- Lemma recrbis_aux_equiv : forall n x,
-   recrbis_aux n A case0 caserec x = recr_aux n A case0 caserec x.
- Proof.
- induction n; simpl; auto; intros.
- case_eq (iszero x); intros; [ | f_equal; auto ].
- rewrite (iszero_eq0 _ H); simpl; fold 0; auto.
- replace (recrbis_aux n A case0 caserec 0) with case0; auto.
- clear H IHn; induction n; simpl; fold 0; congruence.
- Qed.
-
- Lemma recrbis_equiv : forall x,
-   recrbis A case0 caserec x = recr A case0 caserec x.
- Proof.
- intros; apply recrbis_aux_equiv; auto.
- Qed.
-
- End Recr.
-
- (** * Incrementation *)
-
- Section Incr.
-
- (** Variant of [incr] via [recrbis] *)
-
- Let Incr (b : digits) (si rec : int63) :=
-  match b with
-   | D0 => sneakl D1 si
-   | D1 => sneakl D0 rec
-  end.
-
- Definition incrbis_aux n x := recrbis_aux n _ In Incr x.
-
- Lemma incrbis_aux_equiv : forall x, incrbis_aux size x = incr x.
- Proof.
- unfold incr, recr, incrbis_aux; fold Incr; intros.
- apply recrbis_aux_equiv; auto.
- Qed.
-
- (** Recursive equations satisfied by [incr] *)
-
- Lemma incr_eqn1 :
-  forall x, firstr x = D0 -> incr x = twice_plus_one (shiftr x).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H0); simpl; auto.
- unfold incr; rewrite recr_eqn; fold incr; auto.
- rewrite H; auto.
- Qed.
-
- Lemma incr_eqn2 :
-  forall x, firstr x = D1 -> incr x = twice (incr (shiftr x)).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H0) in H; simpl in H; discriminate.
- unfold incr; rewrite recr_eqn; fold incr; auto.
- rewrite H; auto.
- Qed.
-
- Lemma incr_twice : forall x, incr (twice x) = twice_plus_one x.
- Proof.
- intros.
- rewrite incr_eqn1; destruct x; simpl; auto.
- Qed.
-
- Lemma incr_twice_plus_one_firstl :
-  forall x, firstl x = D0 -> incr (twice_plus_one x) = twice (incr x).
- Proof.
- intros.
- rewrite incr_eqn2; [ | destruct x; simpl; auto ].
- f_equal; f_equal.
- destruct x; simpl in *; rewrite H; auto.
- Qed.
-
- (** The previous result is actually true even without the
-     constraint on [firstl], but this is harder to prove
-     (see later). *)
-
- End Incr.
-
- (** * Conversion to [Z] : the [phi] function *)
-
- Section Phi.
-
- (** Variant of [phi] via [recrbis] *)
-
- Let Phi := fun b (_:int63) =>
-       match b with D0 => Z.double | D1 => Z.succ_double end.
-
- Definition phibis_aux n x := recrbis_aux n _ Z0 Phi x.
-
- Lemma phibis_aux_equiv : forall x, phibis_aux size x = phi x.
- Proof.
- unfold phi, recr, phibis_aux; fold Phi; intros.
- apply recrbis_aux_equiv; auto.
- Qed.
-
- (** Recursive equations satisfied by [phi] *)
-
- Lemma phi_eqn1 : forall x, firstr x = D0 ->
-  phi x = Z.double (phi (shiftr x)).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H0); simpl; auto.
- intros; unfold phi; rewrite recr_eqn; fold phi; auto.
- rewrite H; auto.
- Qed.
-
- Lemma phi_eqn2 : forall x, firstr x = D1 ->
-  phi x = Z.succ_double (phi (shiftr x)).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H0) in H; simpl in H; discriminate.
- intros; unfold phi; rewrite recr_eqn; fold phi; auto.
- rewrite H; auto.
- Qed.
-
- Lemma phi_twice_firstl : forall x, firstl x = D0 ->
-  phi (twice x) = Z.double (phi x).
- Proof.
- intros.
- rewrite phi_eqn1; auto; [ | destruct x; auto ].
- f_equal; f_equal.
- destruct x; simpl in *; rewrite H; auto.
- Qed.
-
- Lemma phi_twice_plus_one_firstl : forall x, firstl x = D0 ->
-  phi (twice_plus_one x) = Z.succ_double (phi x).
- Proof.
- intros.
- rewrite phi_eqn2; auto; [ | destruct x; auto ].
- f_equal; f_equal.
- destruct x; simpl in *; rewrite H; auto.
- Qed.
-
- End Phi.
-
- (** [phi x] is positive and lower than [2^63] *)
-
- Lemma phibis_aux_pos : forall n x, (0 <= phibis_aux n x)%Z.
- Proof.
- induction n.
- simpl; unfold phibis_aux; simpl; auto with zarith.
- intros.
- unfold phibis_aux, recrbis_aux; fold recrbis_aux;
-  fold (phibis_aux n (shiftr x)).
- destruct (firstr x).
- specialize IHn with (shiftr x); rewrite Z.double_spec; omega.
- specialize IHn with (shiftr x); rewrite Z.succ_double_spec; omega.
- Qed.
-
- Lemma phibis_aux_bounded :
-  forall n x, n <= size ->
-  (phibis_aux n (nshiftr x (size-n)) < 2 ^ (Z.of_nat n))%Z.
- Proof.
- induction n.
- simpl minus; unfold phibis_aux; simpl; auto with zarith.
- intros.
- unfold phibis_aux, recrbis_aux; fold recrbis_aux;
-  fold (phibis_aux n (shiftr (nshiftr x (size - S n)))).
- assert (shiftr (nshiftr x (size - S n)) =  nshiftr x (size-n)).
-  replace (size - n)%nat with (S (size - (S n))) by omega.
-  simpl; auto.
- rewrite H0.
- assert (H1 : n <= size) by omega.
- specialize (IHn x H1).
- set (y:=phibis_aux n (nshiftr x (size - n))) in *.
- rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
- case_eq (firstr (nshiftr x (size - S n))); intros.
- rewrite Z.double_spec; auto with zarith.
- rewrite Z.succ_double_spec; auto with zarith.
- Qed.
-
- Lemma phi_bounded  : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z.
- Proof.
- intros.
- rewrite <- phibis_aux_equiv.
- split.
- apply phibis_aux_pos.
- change x with (nshiftr x (size-size)).
- apply phibis_aux_bounded; auto.
- Qed.
-
- Lemma phibis_aux_lowerbound :
-  forall n x, firstr (nshiftr x n) = D1 ->
-  (2 ^ Z.of_nat n <= phibis_aux (S n) x)%Z.
- Proof.
- induction n.
- intros.
- unfold nshiftr in H; simpl in *.
- unfold phibis_aux, recrbis_aux.
- rewrite H, Z.succ_double_spec; omega.
-
- intros.
- remember (S n) as m.
- unfold phibis_aux, recrbis_aux; fold recrbis_aux;
-  fold (phibis_aux m (shiftr x)).
- subst m.
- rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
- assert (2^(Z.of_nat n) <= phibis_aux (S n) (shiftr x))%Z.
-  apply IHn.
-  rewrite <- nshiftr_S_tail; auto.
- destruct (firstr x).
- change (Z.double (phibis_aux (S n) (shiftr x))) with
-        (2*(phibis_aux (S n) (shiftr x)))%Z.
- omega.
- rewrite Z.succ_double_spec; omega.
- Qed.
-
- Lemma phi_lowerbound :
-  forall x, firstl x = D1 -> (2^(Z.of_nat (pred size)) <= phi x)%Z.
- Proof.
- intros.
- generalize (phibis_aux_lowerbound (pred size) x).
- rewrite <- firstl_firstr.
- change (S (pred size)) with size; auto.
- rewrite phibis_aux_equiv; auto.
- Qed.
-
- (** * Equivalence modulo [2^n] *)
-
- Section EqShiftL.
-
- (** After killing [n] bits at the left, are the numbers equal ?*)
-
- Definition EqShiftL n x y :=
-  nshiftl x n = nshiftl y n.
-
- Lemma EqShiftL_zero : forall x y, EqShiftL O x y <-> x = y.
- Proof.
- unfold EqShiftL; intros; unfold nshiftl; simpl; split; auto.
- Qed.
-
- Lemma EqShiftL_size : forall k x y, size<=k -> EqShiftL k x y.
- Proof.
- red; intros; rewrite 2 nshiftl_above_size; auto.
- Qed.
-
- Lemma EqShiftL_le : forall k k' x y, k <= k' ->
-   EqShiftL k x y -> EqShiftL k' x y.
- Proof.
- unfold EqShiftL; intros.
- replace k' with ((k'-k)+k)%nat by omega.
- remember (k'-k)%nat as n.
- clear Heqn H k'.
- induction n; simpl; auto.
- f_equal; auto.
- Qed.
-
- Lemma EqShiftL_firstr : forall k x y, k < size ->
-  EqShiftL k x y -> firstr x = firstr y.
- Proof.
- intros.
- rewrite 2 firstr_firstl.
- f_equal.
- apply EqShiftL_le with k; auto.
- unfold size.
- auto with arith.
- Qed.
-
- Lemma EqShiftL_twice : forall k x y,
-  EqShiftL k (twice x) (twice y) <-> EqShiftL (S k) x y.
- Proof.
- intros; unfold EqShiftL.
- rewrite 2 nshiftl_S_tail; split; auto.
- Qed.
-
- (** * From int63 to list of digits. *)
-
- (** Lower (=rightmost) bits comes first. *)
-
- Definition i2l := recrbis _ nil (fun d _ rec => d::rec).
-
- Lemma i2l_length : forall x, length (i2l x) = size.
- Proof.
- intros; reflexivity.
- Qed.
-
- Fixpoint lshiftl l x :=
-   match l with
-     | nil => x
-     | d::l => sneakl d (lshiftl l x)
-   end.
-
- Definition l2i l := lshiftl l On.
-
- Lemma l2i_i2l : forall x, l2i (i2l x) = x.
- Proof.
- destruct x; compute; auto.
- Qed.
-
- Lemma i2l_sneakr : forall x d,
-   i2l (sneakr d x) = tail (i2l x) ++ d::nil.
- Proof.
- destruct x; compute; auto.
- Qed.
-
- Lemma i2l_sneakl : forall x d,
-   i2l (sneakl d x) = d :: removelast (i2l x).
- Proof.
- destruct x; compute; auto.
- Qed.
-
- Lemma i2l_l2i : forall l, length l = size ->
-  i2l (l2i l) = l.
- Proof.
- repeat (destruct l as [ |? l]; [intros; discriminate | ]).
- destruct l; [ | intros; discriminate].
- intros _; compute; auto.
- Qed.
-
- Fixpoint cstlist (A:Type)(a:A) n :=
-  match n with
-   | O => nil
-   | S n => a::cstlist _ a n
-  end.
-
- Lemma i2l_nshiftl : forall n x, n<=size ->
-  i2l (nshiftl x n) = cstlist _ D0 n ++ firstn (size-n) (i2l x).
- Proof.
- induction n.
- intros.
- assert (firstn (size-0) (i2l x) = i2l x).
-  rewrite <- minus_n_O, <- (i2l_length x).
-  induction (i2l x); simpl; f_equal; auto.
- rewrite H0; clear H0.
- reflexivity.
-
- intros.
- rewrite nshiftl_S.
- unfold shiftl; rewrite i2l_sneakl.
- simpl cstlist.
- rewrite <- app_comm_cons; f_equal.
- rewrite IHn; [ | omega].
- rewrite removelast_app.
- apply f_equal.
- replace (size-n)%nat with (S (size - S n))%nat by omega.
- rewrite removelast_firstn; auto.
- rewrite i2l_length; omega.
- generalize (firstn_length (size-n) (i2l x)).
- rewrite i2l_length.
- intros H0 H1. rewrite H1 in H0.
- rewrite min_l in H0 by omega.
- simpl length in H0.
- omega.
- Qed.
-
- (** [i2l] can be used to define a relation equivalent to [EqShiftL] *)
-
- Lemma EqShiftL_i2l : forall k x y,
-   EqShiftL k x y  <-> firstn (size-k) (i2l x) = firstn (size-k) (i2l y).
- Proof.
- intros.
- destruct (le_lt_dec size k) as [Hle|Hlt].
- split; intros.
- replace (size-k)%nat with O by omega.
- unfold firstn; auto.
- apply EqShiftL_size; auto.
-
- unfold EqShiftL.
- assert (k <= size) by omega.
- split; intros.
- assert (i2l (nshiftl x k) = i2l (nshiftl y k)) by (f_equal; auto).
- rewrite 2 i2l_nshiftl in H1; auto.
- eapply app_inv_head; eauto.
- assert (i2l (nshiftl x k) = i2l (nshiftl y k)).
-  rewrite 2 i2l_nshiftl; auto.
-  f_equal; auto.
- rewrite <- (l2i_i2l (nshiftl x k)), <- (l2i_i2l (nshiftl y k)).
- f_equal; auto.
- Qed.
-
- (** This equivalence allows proving easily the following delicate
-     result *)
-
- Lemma EqShiftL_twice_plus_one : forall k x y,
-  EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y.
- Proof.
- intros.
- destruct (le_lt_dec size k) as [Hle|Hlt].
- split; intros; apply EqShiftL_size; auto.
-
- rewrite 2 EqShiftL_i2l.
- unfold twice_plus_one.
- rewrite 2 i2l_sneakl.
- replace (size-k)%nat with (S (size - S k))%nat by omega.
- remember (size - S k)%nat as n.
- remember (i2l x) as lx.
- remember (i2l y) as ly.
- simpl.
- rewrite 2 firstn_removelast.
- split; intros.
- injection H; auto.
- f_equal; auto.
- subst ly n; rewrite i2l_length; omega.
- subst lx n; rewrite i2l_length; omega.
- Qed.
-
- Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y ->
-  EqShiftL (S k) (shiftr x) (shiftr y).
- Proof.
- intros.
- destruct (le_lt_dec size (S k)) as [Hle|Hlt].
- apply EqShiftL_size; auto.
- case_eq (firstr x); intros.
- rewrite <- EqShiftL_twice.
- unfold twice; rewrite <- H0.
- rewrite <- sneakl_shiftr.
- rewrite (EqShiftL_firstr k x y); auto.
- rewrite <- sneakl_shiftr; auto.
- omega.
- rewrite <- EqShiftL_twice_plus_one.
- unfold twice_plus_one; rewrite <- H0.
- rewrite <- sneakl_shiftr.
- rewrite (EqShiftL_firstr k x y); auto.
- rewrite <- sneakl_shiftr; auto.
- omega.
- Qed.
-
- Lemma EqShiftL_incrbis : forall n k x y, n<=size ->
-  (n+k=S size)%nat ->
-  EqShiftL k x y ->
-  EqShiftL k (incrbis_aux n x) (incrbis_aux n y).
- Proof.
- induction n; simpl; intros.
- red; auto.
- destruct (eq_nat_dec k size).
-  subst k; apply EqShiftL_size; auto.
- unfold incrbis_aux; simpl;
-  fold (incrbis_aux n (shiftr x)); fold (incrbis_aux n (shiftr y)).
-
- rewrite (EqShiftL_firstr k x y); auto; try omega.
- case_eq (firstr y); intros.
- rewrite EqShiftL_twice_plus_one.
- apply EqShiftL_shiftr; auto.
-
- rewrite EqShiftL_twice.
- apply IHn; try omega.
- apply EqShiftL_shiftr; auto.
- Qed.
-
- Lemma EqShiftL_incr : forall x y,
-  EqShiftL 1 x y -> EqShiftL 1 (incr x) (incr y).
- Proof.
- intros.
- rewrite <- 2 incrbis_aux_equiv.
- apply EqShiftL_incrbis; auto.
- Qed.
-
- End EqShiftL.
-
- (** * More equations about [incr] *)
-
- Lemma incr_twice_plus_one :
-  forall x, incr (twice_plus_one x) = twice (incr x).
- Proof.
- intros.
- rewrite incr_eqn2; [ | destruct x; simpl; auto].
- apply EqShiftL_incr.
- red; destruct x; simpl; auto.
- Qed.
-
- Lemma incr_firstr : forall x, firstr (incr x) <> firstr x.
- Proof.
- intros.
- case_eq (firstr x); intros.
- rewrite incr_eqn1; auto.
- destruct (shiftr x); simpl; discriminate.
- rewrite incr_eqn2; auto.
- destruct (incr (shiftr x)); simpl; discriminate.
- Qed.
-
- Lemma incr_inv : forall x y,
-  incr x = twice_plus_one y -> x = twice y.
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H0) in *; simpl in *.
- change (incr 0) with 1 in H.
- symmetry; rewrite twice_zero; auto.
- case_eq (firstr x); intros.
- rewrite incr_eqn1 in H; auto.
- clear H0; destruct x; destruct y; simpl in *.
- injection H; intros; subst; auto.
- elim (incr_firstr x).
- rewrite H1, H; destruct y; simpl; auto.
- Qed.
-
- (** * Conversion from [Z] : the [phi_inv] function *)
-
- (** First, recursive equations *)
-
- Lemma phi_inv_double_plus_one : forall z,
-   phi_inv (Z.succ_double z) = twice_plus_one (phi_inv z).
- Proof.
- destruct z; simpl; auto.
- induction p; simpl.
- rewrite 2 incr_twice; auto.
- rewrite incr_twice, incr_twice_plus_one.
- f_equal.
- apply incr_inv; auto.
- auto.
- Qed.
-
- Lemma phi_inv_double : forall z,
-   phi_inv (Z.double z) = twice (phi_inv z).
- Proof.
- destruct z; simpl; auto.
- rewrite incr_twice_plus_one; auto.
- Qed.
-
- Lemma phi_inv_incr : forall z,
-  phi_inv (Z.succ z) = incr (phi_inv z).
- Proof.
- destruct z.
- simpl; auto.
- simpl; auto.
- induction p; simpl; auto.
- rewrite <- Pos.add_1_r, IHp, incr_twice_plus_one; auto.
- rewrite incr_twice; auto.
- simpl; auto.
- destruct p; simpl; auto.
- rewrite incr_twice; auto.
- f_equal.
- rewrite incr_twice_plus_one; auto.
- induction p; simpl; auto.
- rewrite incr_twice; auto.
- f_equal.
- rewrite incr_twice_plus_one; auto.
- Qed.
-
- (** [phi_inv o inv], the always-exact and easy-to-prove trip :
-     from int63 to Z and then back to int63. *)
-
- Lemma phi_inv_phi_aux :
-  forall n x, n <= size ->
-   phi_inv (phibis_aux n (nshiftr x (size-n))) =
-   nshiftr x (size-n).
- Proof.
- induction n.
- intros; simpl minus.
- rewrite nshiftr_size; auto.
- intros.
- unfold phibis_aux, recrbis_aux; fold recrbis_aux;
-  fold (phibis_aux n (shiftr (nshiftr x (size-S n)))).
- assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)).
-  replace (size - n)%nat with (S (size - (S n))); auto; omega.
- rewrite H0.
- case_eq (firstr (nshiftr x (size - S n))); intros.
-
- rewrite phi_inv_double.
- rewrite IHn by omega.
- rewrite <- H0.
- remember (nshiftr x (size - S n)) as y.
- destruct y; simpl in H1; rewrite H1; auto.
-
- rewrite phi_inv_double_plus_one.
- rewrite IHn by omega.
- rewrite <- H0.
- remember (nshiftr x (size - S n)) as y.
- destruct y; simpl in H1; rewrite H1; auto.
- Qed.
-
- Lemma phi_inv_phi : forall x, phi_inv (phi x) = x.
- Proof.
- intros.
- rewrite <- phibis_aux_equiv.
- replace x with (nshiftr x (size - size)) by auto.
- apply phi_inv_phi_aux; auto.
- Qed.
-
- (** The other composition [phi o phi_inv] is harder to prove correct.
-     In particular, an overflow can happen, so a modulo is needed.
-     For the moment, we proceed via several steps, the first one
-     being a detour to [positive_to_in63]. *)
-
- (** * [positive_to_int63] *)
-
- (** A variant of [p2i] with [twice] and [twice_plus_one] instead of
-     [2*i] and [2*i+1] *)
-
- Fixpoint p2ibis n p : (N*int63)%type :=
-  match n with
-    | O => (Npos p, On)
-    | S n => match p with
-               | xO p => let (r,i) := p2ibis n p in (r, twice i)
-               | xI p => let (r,i) := p2ibis n p in (r, twice_plus_one i)
-               | xH => (N0, In)
-             end
-  end.
-
- Lemma p2ibis_bounded : forall n p,
-  nshiftr (snd (p2ibis n p)) n = 0.
- Proof.
- induction n.
- simpl; intros; auto.
- simpl p2ibis; intros.
- destruct p; simpl snd.
-
- specialize IHn with p.
- destruct (p2ibis n p). simpl @snd in *.
- rewrite nshiftr_S_tail.
- destruct (le_lt_dec size n) as [Hle|Hlt].
- rewrite nshiftr_above_size; auto.
- assert (H:=nshiftr_0_firstl _ _ Hlt IHn).
- replace (shiftr (twice_plus_one i)) with i; auto.
- destruct i; simpl in *. rewrite H; auto.
-
- specialize IHn with p.
- destruct (p2ibis n p); simpl @snd in *.
- rewrite nshiftr_S_tail.
- destruct (le_lt_dec size n) as [Hle|Hlt].
- rewrite nshiftr_above_size; auto.
- assert (H:=nshiftr_0_firstl _ _ Hlt IHn).
- replace (shiftr (twice i)) with i; auto.
- destruct i; simpl in *; rewrite H; auto.
-
- rewrite nshiftr_S_tail; auto.
- replace (shiftr In) with 0; auto.
- apply nshiftr_n_0.
- Qed.
-
- Local Open Scope Z_scope.
-
- Lemma p2ibis_spec : forall n p, (n<=size)%nat ->
-    Zpos p = (Z.of_N (fst (p2ibis n p)))*2^(Z.of_nat n) +
-             phi (snd (p2ibis n p)).
- Proof.
- induction n; intros.
- simpl; rewrite Pos.mul_1_r; auto.
- replace (2^(Z.of_nat (S n)))%Z with (2*2^(Z.of_nat n))%Z by
-  (rewrite <- Z.pow_succ_r, <- Zpos_P_of_succ_nat;
-   auto with zarith).
- rewrite (Z.mul_comm 2).
- assert (n<=size)%nat by omega.
- destruct p; simpl; [ | | auto];
-  specialize (IHn p H0);
-  generalize (p2ibis_bounded n p);
-  destruct (p2ibis n p) as (r,i); simpl in *; intros.
-
- change (Zpos p~1) with (2*Zpos p + 1)%Z.
- rewrite phi_twice_plus_one_firstl, Z.succ_double_spec.
- rewrite IHn; ring.
- apply (nshiftr_0_firstl n); auto; try omega.
-
- change (Zpos p~0) with (2*Zpos p)%Z.
- rewrite phi_twice_firstl.
- change (Z.double (phi i)) with (2*(phi i))%Z.
- rewrite IHn; ring.
- apply (nshiftr_0_firstl n); auto; try omega.
- Qed.
-
- (** We now prove that this [p2ibis] is related to [phi_inv_positive] *)
-
- Lemma phi_inv_positive_p2ibis : forall n p, (n<=size)%nat ->
-  EqShiftL (size-n) (phi_inv_positive p) (snd (p2ibis n p)).
- Proof.
- induction n.
- intros.
- apply EqShiftL_size; auto.
- intros.
- simpl p2ibis; destruct p; [ | | red; auto];
-  specialize IHn with p;
-  destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive;
-  rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice;
-  replace (S (size - S n))%nat with (size - n)%nat by omega;
-  apply IHn; omega.
- Qed.
-
- (** This gives the expected result about [phi o phi_inv], at least
-     for the positive case. *)
-
- Lemma phi_phi_inv_positive : forall p,
-  phi (phi_inv_positive p) = (Zpos p) mod (2^(Z.of_nat size)).
- Proof.
- intros.
- replace (phi_inv_positive p) with (snd (p2ibis size p)).
- rewrite (p2ibis_spec size p) by auto.
- rewrite Z.add_comm, Z_mod_plus.
- symmetry; apply Zmod_small.
- apply phi_bounded.
- auto with zarith.
- symmetry.
- rewrite <- EqShiftL_zero.
- apply (phi_inv_positive_p2ibis size p); auto.
- Qed.
-
- (** Moreover, [p2ibis] is also related with [p2i] and hence with
-    [positive_to_int63]. *)
-
- Lemma double_twice_firstl : forall x, firstl x = D0 ->
-  (Twon*x = twice x)%int.
- Proof.
- intros.
- unfold mul63.
- rewrite <- Z.double_spec, <- phi_twice_firstl, phi_inv_phi; auto.
- Qed.
-
- Lemma double_twice_plus_one_firstl : forall x, firstl x = D0 ->
-  (Twon*x+In = twice_plus_one x)%int.
- Proof.
- intros.
- rewrite double_twice_firstl; auto.
- unfold add63.
- rewrite phi_twice_firstl, <- Z.succ_double_spec,
-   <- phi_twice_plus_one_firstl, phi_inv_phi; auto.
- Qed.
-
- Lemma p2i_p2ibis : forall n p, (n<=size)%nat ->
-  p2i n p = p2ibis n p.
- Proof.
- induction n; simpl; auto; intros.
- destruct p; auto; specialize IHn with p;
-  generalize (p2ibis_bounded n p);
-  rewrite IHn; try omega; destruct (p2ibis n p); simpl; intros;
-  f_equal; auto.
- apply double_twice_plus_one_firstl.
- apply (nshiftr_0_firstl n); auto; omega.
- apply double_twice_firstl.
- apply (nshiftr_0_firstl n); auto; omega.
- Qed.
-
- Lemma positive_to_int63_phi_inv_positive : forall p,
-   snd (positive_to_int63 p) = phi_inv_positive p.
- Proof.
- intros; unfold positive_to_int63.
- rewrite p2i_p2ibis; auto.
- symmetry.
- rewrite <- EqShiftL_zero.
- apply (phi_inv_positive_p2ibis size); auto.
- Qed.
-
- Lemma positive_to_int63_spec : forall p,
-    Zpos p = (Z.of_N (fst (positive_to_int63 p)))*2^(Z.of_nat size) +
-               phi (snd (positive_to_int63 p)).
- Proof.
- unfold positive_to_int63.
- intros; rewrite p2i_p2ibis; auto.
- apply p2ibis_spec; auto.
- Qed.
-
- (** Thanks to the result about [phi o phi_inv_positive], we can
-     now establish easily the most general results about
-     [phi o twice] and so one. *)
-
- Lemma phi_twice : forall x,
-   phi (twice x) = (Z.double (phi x)) mod 2^(Z.of_nat size).
- Proof.
- intros.
- pattern x at 1; rewrite <- (phi_inv_phi x).
- rewrite <- phi_inv_double.
- assert (0 <= Z.double (phi x)).
-  rewrite Z.double_spec; generalize (phi_bounded x); omega.
- destruct (Z.double (phi x)).
- simpl; auto.
- apply phi_phi_inv_positive.
- compute in H; elim H; auto.
- Qed.
-
- Lemma phi_twice_plus_one : forall x,
-   phi (twice_plus_one x) = (Z.succ_double (phi x)) mod 2^(Z.of_nat size).
- Proof.
- intros.
- pattern x at 1; rewrite <- (phi_inv_phi x).
- rewrite <- phi_inv_double_plus_one.
- assert (0 <= Z.succ_double (phi x)).
-  rewrite Z.succ_double_spec; generalize (phi_bounded x); omega.
- destruct (Z.succ_double (phi x)).
- simpl; auto.
- apply phi_phi_inv_positive.
- compute in H; elim H; auto.
- Qed.
-
- Lemma phi_incr : forall x,
-   phi (incr x) = (Z.succ (phi x)) mod 2^(Z.of_nat size).
- Proof.
- intros.
- pattern x at 1; rewrite <- (phi_inv_phi x).
- rewrite <- phi_inv_incr.
- assert (0 <= Z.succ (phi x)).
-  change (Z.succ (phi x)) with ((phi x)+1)%Z;
-   generalize (phi_bounded x); omega.
- destruct (Z.succ (phi x)).
- simpl; auto.
- apply phi_phi_inv_positive.
- compute in H; elim H; auto.
- Qed.
-
- (** With the previous results, we can deal with [phi o phi_inv] even
-    in the negative case *)
-
- Lemma phi_phi_inv_negative :
-  forall p, phi (incr (complement_negative p)) = (Zneg p) mod 2^(Z.of_nat size).
- Proof.
- induction p.
-
- simpl complement_negative.
- rewrite phi_incr in IHp.
- rewrite incr_twice, phi_twice_plus_one.
- remember (phi (complement_negative p)) as q.
- rewrite Z.succ_double_spec.
- replace (2*q+1) with (2*(Z.succ q)-1) by omega.
- rewrite <- Zminus_mod_idemp_l, <- Zmult_mod_idemp_r, IHp.
- rewrite Zmult_mod_idemp_r, Zminus_mod_idemp_l; auto with zarith.
-
- simpl complement_negative.
- rewrite incr_twice_plus_one, phi_twice.
- remember (phi (incr (complement_negative p))) as q.
- rewrite Z.double_spec, IHp, Zmult_mod_idemp_r; auto with zarith.
-
- simpl; auto.
- Qed.
-
- Lemma phi_phi_inv :
-  forall z, phi (phi_inv z) = z mod 2 ^ (Z.of_nat size).
- Proof.
- destruct z.
- simpl; auto.
- apply phi_phi_inv_positive.
- apply phi_phi_inv_negative.
- Qed.
-
-End Basics.
-
-Definition zdigits := Eval vm_compute in (phi_inv 63).
-Notation "63" := zdigits : int63_scope.
-
-Instance int63_ops : ZnZ.Ops int63 :=
-{
- digits      := 63%positive; (* number of digits *)
- zdigits     := 63%int; (* number of digits *)
- to_Z        := phi; (* conversion to Z *)
- of_pos      := positive_to_int63; (* positive -> N*int63 :  p => N,i
-                                      where p = N*2^63+phi i *)
- head0       := head063;  (* number of head 0 *)
- tail0       := tail063;  (* number of tail 0 *)
- zero        := 0;
- one         := 1;
- minus_one   := Tn; (* 2^63 - 1 *)
- compare     := compare63;
- eq0         := fun i => match i ?= 0 with Eq => true | _ => false end;
- opp_c       := fun i => 0 -c i;
- opp         := opp63;
- opp_carry   := fun i => 0-i-1;
- succ_c      := fun i => i +c 1;
- add_c       := add63c;
- add_carry_c := add63carryc;
- succ        := fun i => i + 1;
- add         := add63;
- add_carry   := fun i j => i + j + 1;
- pred_c      := fun i => i -c 1;
- sub_c       := sub63c;
- sub_carry_c := sub63carryc;
- pred        := fun i => i - 1;
- sub         := sub63;
- sub_carry   := fun i j => i - j - 1;
- mul_c       := mul63c;
- mul         := mul63;
- square_c    := fun x => x *c x;
- div21       := div6321;
- div_gt      := div63; (* this is supposed to be the special case of
-                         division a/b where a > b *)
- div         := div63;
- modulo_gt   := fun i j => let (_,r) := i/j in r;
- modulo      := fun i j => let (_,r) := i/j in r;
- gcd_gt      := gcd63;
- gcd         := gcd63;
- add_mul_div := addmuldiv63;
- pos_mod     := (* modulo 2^p *)
-  fun p i =>
-  match p ?= 63 with
-    | Lt => addmuldiv63 p 0 (addmuldiv63 (63-p) i 0)
-    | _ => i
-  end;
- is_even      :=
-  fun i => let (_,r) := i/2 in
-  match r ?= 0 with Eq => true | _ => false end;
- sqrt2       := sqrt632;
- sqrt        := sqrt63;
- lor         := lor63;
- land        := land63;
- lxor        := lxor63
-}.
-
-Section Int63_Specs.
-
- Local Open Scope Z_scope.
-
- Notation "[| x |]" := (phi x)  (at level 0, x at level 99).
-
- Local Notation wB := (2 ^ (Z.of_nat size)).
-
- Lemma wB_pos : wB > 0.
- Proof.
-  auto with zarith.
- Qed.
-
- Notation "[+| c |]" :=
-   (interp_carry 1 wB phi c)  (at level 0, c at level 99).
-
- Notation "[-| c |]" :=
-   (interp_carry (-1) wB phi c)  (at level 0, c at level 99).
-
- Notation "[|| x ||]" :=
-   (zn2z_to_Z wB phi x)  (at level 0, x at level 99).
-
- Lemma spec_zdigits : [| 63 |] = 63.
- Proof.
-  reflexivity.
- Qed.
-
- Lemma spec_more_than_1_digit: 1 < 63.
- Proof.
-  auto with zarith.
- Qed.
-
- Lemma spec_0   : [| 0 |] = 0.
- Proof.
-  reflexivity.
- Qed.
-
- Lemma spec_1   : [| 1 |] = 1.
- Proof.
-  reflexivity.
- Qed.
-
- Lemma spec_m1 : [| Tn |] = wB - 1.
- Proof.
-  reflexivity.
- Qed.
-
- Lemma spec_compare : forall x y,
-   (x ?= y)%int = ([|x|] ?= [|y|]).
- Proof. reflexivity. Qed.
-
- (** Addition *)
-
- Lemma spec_add_c  : forall x y, [+|add63c x y|] = [|x|] + [|y|].
- Proof.
- intros; unfold add63c, add63, interp_carry; rewrite phi_phi_inv.
- generalize (phi_bounded x)(phi_bounded y); intros.
- set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
-
- assert ((X+Y) mod wB ?= X+Y <> Eq -> [+|C1 (phi_inv (X+Y))|] = X+Y).
-  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
-  destruct (Z_lt_le_dec (X+Y) wB).
-  contradict H1; auto using Zmod_small with zarith.
-  rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
-  rewrite Zmod_small; romega.
-
- generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
- destruct Z.compare; intros;
-  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
- Qed.
-
- Lemma spec_succ_c : forall x, [+|add63c x 1|] = [|x|] + 1.
- Proof.
- intros; apply spec_add_c.
- Qed.
-
- Lemma spec_add_carry_c : forall x y, [+|add63carryc x y|] = [|x|] + [|y|] + 1.
- Proof.
- intros.
- unfold add63carryc, interp_carry; rewrite phi_phi_inv.
- generalize (phi_bounded x)(phi_bounded y); intros.
- set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
-
- assert ((X+Y+1) mod wB ?= X+Y+1 <> Eq -> [+|C1 (phi_inv (X+Y+1))|] = X+Y+1).
-  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
-  destruct (Z_lt_le_dec (X+Y+1) wB).
-  contradict H1; auto using Zmod_small with zarith.
-  rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
-  rewrite Zmod_small; romega.
-
- generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
- destruct Z.compare; intros;
-  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
- Qed.
-
- Lemma spec_add : forall x y, [|x+y|] = ([|x|] + [|y|]) mod wB.
- Proof.
- intros; apply phi_phi_inv.
- Qed.
-
- Lemma spec_add_carry :
-	 forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB.
- Proof.
- unfold add63; intros.
- repeat rewrite phi_phi_inv.
- apply Zplus_mod_idemp_l.
- Qed.
-
- Lemma spec_succ : forall x, [|x+1|] = ([|x|] + 1) mod wB.
- Proof.
- intros; rewrite <- spec_1; apply spec_add.
- Qed.
-
- (** Substraction *)
-
- Lemma spec_sub_c : forall x y, [-|sub63c x y|] = [|x|] - [|y|].
- Proof.
- unfold sub63c, sub63, interp_carry; intros.
- rewrite phi_phi_inv.
- generalize (phi_bounded x)(phi_bounded y); intros.
- set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
-
- assert ((X-Y) mod wB ?= X-Y <> Eq -> [-|C1 (phi_inv (X-Y))|] = X-Y).
-  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
-  destruct (Z_lt_le_dec (X-Y) 0).
-  rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
-
- generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
- destruct Z.compare; intros;
-  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
- Qed.
-
- Lemma spec_sub_carry_c : forall x y, [-|sub63carryc x y|] = [|x|] - [|y|] - 1.
- Proof.
- unfold sub63carryc, sub63, interp_carry; intros.
- rewrite phi_phi_inv.
- generalize (phi_bounded x)(phi_bounded y); intros.
- set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
-
- assert ((X-Y-1) mod wB ?= X-Y-1 <> Eq -> [-|C1 (phi_inv (X-Y-1))|] = X-Y-1).
-  unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
-  destruct (Z_lt_le_dec (X-Y-1) 0).
-  rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
-
- generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
- destruct Z.compare; intros;
-  [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
- Qed.
-
- Lemma spec_sub : forall x y, [|x-y|] = ([|x|] - [|y|]) mod wB.
- Proof.
- intros; apply phi_phi_inv.
- Qed.
-
- Lemma spec_sub_carry :
-   forall x y, [|x-y-1|] = ([|x|] - [|y|] - 1) mod wB.
- Proof.
- unfold sub63; intros.
- repeat rewrite phi_phi_inv.
- apply Zminus_mod_idemp_l.
- Qed.
-
- Lemma spec_opp_c : forall x, [-|sub63c 0 x|] = -[|x|].
- Proof.
- intros; apply spec_sub_c.
- Qed.
-
- Lemma spec_opp : forall x, [|0 - x|] = (-[|x|]) mod wB.
- Proof.
- intros; apply phi_phi_inv.
- Qed.
-
- Lemma spec_opp_carry : forall x, [|0 - x - 1|] = wB - [|x|] - 1.
- Proof.
- unfold sub63; intros.
- repeat rewrite phi_phi_inv.
- change [|1|] with 1; change [|0|] with 0.
- rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
- rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (phi_bounded x); romega.
- Qed.
-
- Lemma spec_pred_c : forall x, [-|sub63c x 1|] = [|x|] - 1.
- Proof.
- intros; apply spec_sub_c.
- Qed.
-
- Lemma spec_pred : forall x, [|x-1|] = ([|x|] - 1) mod wB.
- Proof.
- intros; apply spec_sub.
- Qed.
-
- (** Multiplication *)
-
- Lemma phi2_phi_inv2 : forall x, [||phi_inv2 x||] = x mod (wB^2).
- Proof.
- assert (forall z, (z / wB) mod wB * wB + z mod wB = z mod wB ^ 2).
-  intros.
-  assert ((z/wB) mod wB = z/wB - (z/wB/wB)*wB).
-   rewrite (Z_div_mod_eq (z/wB) wB wB_pos) at 2; ring.
-  assert (z mod wB = z - (z/wB)*wB).
-   rewrite (Z_div_mod_eq z wB wB_pos) at 2; ring.
-  rewrite H.
-  rewrite H0 at 1.
-  ring_simplify.
-  rewrite Zdiv_Zdiv; auto with zarith.
-  rewrite (Z_div_mod_eq z (wB*wB)) at 2; auto with zarith.
-  change (wB*wB) with (wB^2); ring.
-
- unfold phi_inv2.
- destruct x; unfold zn2z_to_Z; rewrite ?phi_phi_inv;
-  change base with wB; auto.
- Qed.
-
- Lemma spec_mul_c : forall x y, [|| mul63c x y ||] = [|x|] * [|y|].
- Proof.
- unfold mul63c; intros.
- rewrite phi2_phi_inv2.
- apply Zmod_small.
- generalize (phi_bounded x)(phi_bounded y); intros.
- change (wB^2) with (wB * wB).
- auto using Z.mul_lt_mono_nonneg with zarith.
- Qed.
-
- Lemma spec_mul : forall x y, [|x*y|] = ([|x|] * [|y|]) mod wB.
- Proof.
- intros; apply phi_phi_inv.
- Qed.
-
- Lemma spec_square_c : forall x, [|| mul63c x x ||] = [|x|] * [|x|].
- Proof.
- intros; apply spec_mul_c.
- Qed.
-
- (** Division *)
-
- Lemma spec_div21 : forall a1 a2 b,
-      wB/2 <= [|b|] ->
-      [|a1|] < [|b|] ->
-      let (q,r) := div6321 a1 a2 b in
-      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
-      0 <= [|r|] < [|b|].
- Proof.
- unfold div6321; intros.
- generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros.
- assert ([|b|]>0) by (auto with zarith).
- generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4).
- unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]).
- rewrite ?phi_phi_inv.
- destruct 1; intros.
- unfold phi2 in *.
- change base with wB; change base with wB in H5.
- change (Z.pow_pos 2 63) with wB; change (Z.pow_pos 2 63) with wB in H.
- rewrite H5, Z.mul_comm.
- replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega).
- replace (z mod wB) with z; auto with zarith.
-  symmetry; apply Zmod_small.
-  split.
-  apply H7; change base with wB; auto with zarith.
-  apply Z.mul_lt_mono_pos_r with [|b|]; [omega| ].
-  rewrite Z.mul_comm.
-  apply Z.le_lt_trans with ([|b|]*z+z0); [omega| ].
-  rewrite <- H5.
-  apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [omega | ].
-  replace ([|a1|]*wB+(wB-1)) with (wB*([|a1|]+1)-1) by ring.
-  assert (wB*([|a1|]+1) <= wB*[|b|]); try omega.
-  apply Z.mul_le_mono_nonneg; omega.
- Qed.
-
- Lemma spec_div : forall a b, 0 < [|b|] ->
-      let (q,r) := div63 a b in
-      [|a|] = [|q|] * [|b|] + [|r|] /\
-      0 <= [|r|] < [|b|].
- Proof.
- unfold div63; intros.
- assert ([|b|]>0) by (auto with zarith).
- generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0).
- unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]).
- rewrite ?phi_phi_inv.
- destruct 1; intros.
- rewrite H1, Z.mul_comm.
- generalize (phi_bounded a)(phi_bounded b); intros.
- replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega).
- replace (z mod wB) with z; auto with zarith.
-  symmetry; apply Zmod_small.
-  split; auto with zarith.
-  apply Z.le_lt_trans with [|a|]; auto with zarith.
-  rewrite H1.
-  apply Z.le_trans with ([|b|]*z); try omega.
-  rewrite <- (Z.mul_1_l z) at 1.
-  apply Z.mul_le_mono_nonneg; auto with zarith.
- Qed.
-
- Lemma spec_mod :  forall a b, 0 < [|b|] ->
-      [|let (_,r) := (a/b)%int in r|] = [|a|] mod [|b|].
- Proof.
- unfold div63; intros.
- assert ([|b|]>0) by (auto with zarith).
- unfold Z.modulo.
- generalize (Z_div_mod [|a|] [|b|] H0).
- destruct (Z.div_eucl [|a|] [|b|]).
- rewrite ?phi_phi_inv.
- destruct 1; intros.
- generalize (phi_bounded b); intros.
- apply Zmod_small; omega.
- Qed.
-
- Lemma phi_gcd : forall i j,
-  [|gcd63 i j|] = Zgcdn (2*size) [|j|] [|i|].
- Proof.
-  unfold gcd63.
-  induction (2*size)%nat; intros.
-  reflexivity.
-  simpl euler.
-  unfold compare63.
-  change [|On|] with 0.
-  generalize (phi_bounded j)(phi_bounded i); intros.
-  case_eq [|j|]; intros.
-  simpl; intros.
-  generalize (Zabs_spec [|i|]); omega.
-  simpl. rewrite IHn, H1; f_equal.
-  rewrite spec_mod, H1; auto.
-  rewrite H1; compute; auto.
-  rewrite H1 in H; destruct H as [H _]; compute in H; elim H; auto.
- Qed.
-
- Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd63 a b|].
- Proof.
- intros.
- rewrite phi_gcd.
- apply Zis_gcd_sym.
- apply Zgcdn_is_gcd.
- unfold Zgcd_bound.
- generalize (phi_bounded b).
- destruct [|b|].
- unfold size; auto with zarith.
- intros (_,H).
- cut (Pos.size_nat p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto].
- intros (H,_); compute in H; elim H; auto.
- Qed.
-
- Lemma iter_int63_iter_nat : forall A f i a,
-  iter_int63 i A f a = iter_nat (Z.abs_nat [|i|]) A f a.
- Proof.
- intros.
- unfold iter_int63.
- rewrite <- recrbis_equiv; auto; unfold recrbis.
- rewrite <- phibis_aux_equiv.
-
- revert i a; induction size.
- simpl; auto.
- simpl; intros.
- case_eq (firstr i); intros H; rewrite 2 IHn;
-  unfold phibis_aux; simpl; rewrite ?H; fold (phibis_aux n (shiftr i));
-  generalize (phibis_aux_pos n (shiftr i)); intros;
-  set (z := phibis_aux n (shiftr i)) in *; clearbody z;
-  rewrite <- nat_rect_plus.
-
- f_equal.
- rewrite Z.double_spec, <- Z.add_diag.
- symmetry; apply Zabs2Nat.inj_add; auto with zarith.
-
- change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a =
-    iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
- rewrite Z.succ_double_spec, <- Z.add_diag.
- rewrite Zabs2Nat.inj_add; auto with zarith.
- rewrite Zabs2Nat.inj_add; auto with zarith.
- change (Z.abs_nat 1) with 1%nat; omega.
- Qed.
-
- Fixpoint addmuldiv63_alt n i j :=
-  match n with
-    | O => i
-    | S n => addmuldiv63_alt n (sneakl (firstl j) i) (shiftl j)
-  end.
-
- Lemma addmuldiv63_equiv : forall p x y,
-  addmuldiv63 p x y = addmuldiv63_alt (Z.abs_nat [|p|]) x y.
- Proof.
- intros.
- unfold addmuldiv63.
- rewrite iter_int63_iter_nat.
- set (n:=Z.abs_nat [|p|]); clearbody n; clear p.
- revert x y; induction n.
- simpl; auto.
- intros.
- simpl addmuldiv63_alt.
- replace (S n) with (n+1)%nat by (rewrite plus_comm; auto).
- rewrite nat_rect_plus; simpl; auto.
- Qed.
-
- Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 63 ->
-   [| addmuldiv63 p x y |] =
-   ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos 63) - [|p|]))) mod wB.
- Proof.
- intros.
- rewrite addmuldiv63_equiv.
- assert ([|p|] = Z.of_nat (Z.abs_nat [|p|])).
-  rewrite Zabs2Nat.id_abs; symmetry; apply Z.abs_eq.
-  destruct (phi_bounded p); auto.
- rewrite H0; rewrite H0 in H; clear H0; rewrite Zabs2Nat.id.
- set (n := Z.abs_nat [|p|]) in *; clearbody n.
- assert (n <= 63)%nat.
-  rewrite Nat2Z.inj_le; auto with zarith.
- clear p H; revert x y.
-
- induction n.
- simpl Z.of_nat; intros.
- rewrite Z.mul_1_r.
- replace ([|y|] / 2^(63-0)) with 0.
- rewrite Z.add_0_r.
- symmetry; apply Zmod_small; apply phi_bounded.
- symmetry; apply Zdiv_small; apply phi_bounded.
-
- simpl addmuldiv63_alt; intros.
- rewrite IHn; [ | omega ].
- case_eq (firstl y); intros.
-
- rewrite phi_twice, Z.double_spec.
- rewrite phi_twice_firstl; auto.
- change (Z.double [|y|]) with (2*[|y|]).
- rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
- rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
- f_equal.
- f_equal.
- ring.
- replace (63-Z.of_nat n) with (Z.succ(63-Z.succ(Z.of_nat n))) by ring.
- rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith.
- rewrite Z.mul_comm, Z_div_mult; auto with zarith.
-
- rewrite phi_twice_plus_one, Z.succ_double_spec.
- rewrite phi_twice; auto.
- change (Z.double [|y|]) with (2*[|y|]).
- rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
- rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
- rewrite Z.mul_add_distr_r, Z.mul_1_l, <- Z.add_assoc.
- f_equal.
- f_equal.
- ring.
- assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
-  clear - H. symmetry. apply Zmod_unique with 1; [ | ring ].
-  generalize (phi_lowerbound  _ H) (phi_bounded y).
-  set (wB' := 2^Z.of_nat (pred size)).
-  replace wB with (2*wB'); [ omega | ].
-  unfold wB'. rewrite <- Z.pow_succ_r, <- Nat2Z.inj_succ by (auto with zarith).
-  f_equal.
- rewrite H1.
- replace wB with (2^(Z.of_nat n)*2^(63-Z.of_nat n)) by
-  (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
- unfold Z.sub; rewrite <- Z.mul_opp_l.
- rewrite Z_div_plus; auto with zarith.
- ring_simplify.
- replace (63+-Z.of_nat n) with (Z.succ(63-Z.succ(Z.of_nat n))) by ring.
- rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith.
- rewrite Z.mul_comm, Z_div_mult; auto with zarith.
- Qed.
-
- Lemma spec_pos_mod : forall w p,
-       [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
- Proof.
- unfold int63_ops, ZnZ.pos_mod, compare63.
- change [|63|] with 63%Z.
- assert (forall w p, 63<=p -> [|w|] = [|w|] mod 2^p).
-  intros.
-  generalize (phi_bounded w).
-  symmetry; apply Zmod_small.
-  split; auto with zarith.
-  apply Z.lt_le_trans with wB; auto with zarith.
-  apply Zpower_le_monotone; auto with zarith.
- intros.
- case_eq ([|p|] ?= 63); intros;
-  [ apply H; rewrite (Z.compare_eq _ _ H0); auto with zarith | |
-    apply H; change ([|p|]>63)%Z in H0; auto with zarith ].
- change ([|p|]<63) in H0.
- rewrite spec_add_mul_div by auto with zarith.
- change [|0|] with 0%Z; rewrite Z.mul_0_l, Z.add_0_l.
- generalize (phi_bounded p)(phi_bounded w); intros.
- assert (63-[|p|]<wB).
-  apply Z.le_lt_trans with 63%Z; auto with zarith.
-  compute; auto.
- assert ([|63-p|]=63-[|p|]).
-  unfold sub63; rewrite phi_phi_inv.
-  change [|63|] with 63%Z.
-  apply Zmod_small; auto with zarith.
- rewrite spec_add_mul_div by (rewrite H4; auto with zarith).
- change [|0|] with 0%Z; rewrite Zdiv_0_l, Z.add_0_r.
- rewrite H4.
- apply shift_unshift_mod_2; auto with zarith.
- Qed.
-
-
- (** Shift operations *)
-
- Lemma spec_head00:  forall x, [|x|] = 0 -> [|head063 x|] = Zpos 63.
- Proof.
-  intros.
-  generalize (phi_inv_phi x).
-  rewrite H; simpl phi_inv.
-  intros H'; rewrite <- H'.
-  simpl; auto.
- Qed.
-
- Fixpoint head063_alt n x :=
-  match n with
-    | O => 0%nat
-    | S n => match firstl x with
-               | D0 => S (head063_alt n (shiftl x))
-               | D1 => 0%nat
-             end
-  end.
-
- Lemma head063_equiv :
-   forall x, [|head063 x|] = Z.of_nat (head063_alt size x).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H).
- simpl; auto.
-
- unfold head063, recl.
- change On with (phi_inv (Z.of_nat (63-size))).
- replace (head063_alt size x) with
-   (head063_alt size x + (63 - size))%nat by auto.
- assert (size <= 63)%nat by auto with arith.
-
- revert x H; induction size; intros.
- simpl; auto.
- unfold recl_aux; fold recl_aux.
- unfold head063_alt; fold head063_alt.
- rewrite H.
- assert ([|phi_inv (Z.of_nat (63-S n))|] = Z.of_nat (63 - S n)).
-  rewrite phi_phi_inv.
-  apply Zmod_small.
-  split.
-  change 0 with (Z.of_nat O); apply inj_le; omega.
-  apply Z.le_lt_trans with (Z.of_nat 63).
-  apply inj_le; omega.
-  compute; auto.
- case_eq (firstl x); intros; auto.
- rewrite plus_Sn_m, plus_n_Sm.
- replace (S (63 - S n)) with (63 - n)%nat by omega.
- rewrite <- IHn; [ | omega | ].
- f_equal; f_equal.
- unfold add63.
- rewrite H1.
- f_equal.
- change [|In|] with 1.
- replace (63-n)%nat with (S (63 - S n))%nat by omega.
- rewrite Nat2Z.inj_succ; ring.
-
- clear - H H2.
- rewrite (sneakr_shiftl x) in H.
- rewrite H2 in H.
- case_eq (iszero (shiftl x)); intros; auto.
- rewrite (iszero_eq0 _ H0) in H; discriminate.
- Qed.
-
- Lemma phi_nz : forall x, 0 < [|x|] <-> x <> 0%int.
- Proof.
- split; intros.
- red; intro; subst x; discriminate.
- assert ([|x|]<>0%Z).
- contradict H.
- rewrite <- (phi_inv_phi x); rewrite H; auto.
- generalize (phi_bounded x); auto with zarith.
- Qed.
-
- Lemma spec_head0  : forall x,  0 < [|x|] ->
-	 wB/ 2 <= 2 ^ ([|head063 x|]) * [|x|] < wB.
- Proof.
- intros.
- rewrite head063_equiv.
- assert (nshiftl x size = 0%int).
-  apply nshiftl_size.
- revert x H H0.
- unfold size at 2 5.
- induction size.
- simpl Z.of_nat.
- intros.
- compute in H0; rewrite H0 in H; discriminate.
-
- intros.
- simpl head063_alt.
- case_eq (firstl x); intros.
- rewrite (Nat2Z.inj_succ (head063_alt n (shiftl x))), Z.pow_succ_r; auto with zarith.
- rewrite <- Z.mul_assoc, Z.mul_comm, <- Z.mul_assoc, <-(Z.mul_comm 2).
- rewrite <- Z.double_spec, <- (phi_twice_firstl _ H1).
- apply IHn.
-
- rewrite phi_nz; rewrite phi_nz in H; contradict H.
- change twice with shiftl in H.
- rewrite (sneakr_shiftl x), H1, H; auto.
-
- rewrite <- nshiftl_S_tail; auto.
-
- change (2^(Z.of_nat 0)) with 1; rewrite Z.mul_1_l.
- generalize (phi_bounded x); unfold size; split; auto with zarith.
- change (2^(Z.of_nat 63)/2) with (2^(Z.of_nat (pred size))).
- apply phi_lowerbound; auto.
- Qed.
-
- Lemma spec_tail00:  forall x, [|x|] = 0 -> [|tail063 x|] = Zpos 63.
- Proof.
-  intros.
-  generalize (phi_inv_phi x).
-  rewrite H; simpl phi_inv.
-  intros H'; rewrite <- H'.
-  simpl; auto.
- Qed.
-
- Fixpoint tail063_alt n x :=
-  match n with
-    | O => 0%nat
-    | S n => match firstr x with
-               | D0 => S (tail063_alt n (shiftr x))
-               | D1 => 0%nat
-             end
-  end.
-
- Lemma tail063_equiv :
-   forall x, [|tail063 x|] = Z.of_nat (tail063_alt size x).
- Proof.
- intros.
- case_eq (iszero x); intros.
- rewrite (iszero_eq0 _ H).
- simpl; auto.
-
- unfold tail063, recr.
- change On with (phi_inv (Z.of_nat (63-size))).
- replace (tail063_alt size x) with
-   (tail063_alt size x + (63 - size))%nat by auto.
- assert (size <= 63)%nat by auto with arith.
-
- revert x H; induction size; intros.
- simpl; auto.
- unfold recr_aux; fold recr_aux.
- unfold tail063_alt; fold tail063_alt.
- rewrite H.
- assert ([|phi_inv (Z.of_nat (63-S n))|] = Z.of_nat (63 - S n)).
-  rewrite phi_phi_inv.
-  apply Zmod_small.
-  split.
-  change 0 with (Z.of_nat O); apply inj_le; omega.
-  apply Z.le_lt_trans with (Z.of_nat 63).
-  apply inj_le; omega.
-  compute; auto.
- case_eq (firstr x); intros; auto.
- rewrite plus_Sn_m, plus_n_Sm.
- replace (S (63 - S n)) with (63 - n)%nat by omega.
- rewrite <- IHn; [ | omega | ].
- f_equal; f_equal.
- unfold add63.
- rewrite H1.
- f_equal.
- change [|In|] with 1.
- replace (63-n)%nat with (S (63 - S n))%nat by omega.
- rewrite Nat2Z.inj_succ; ring.
-
- clear - H H2.
- rewrite (sneakl_shiftr x) in H.
- rewrite H2 in H.
- case_eq (iszero (shiftr x)); intros; auto.
- rewrite (iszero_eq0 _ H0) in H; discriminate.
- Qed.
-
- Lemma spec_tail0  : forall x, 0 < [|x|] ->
-         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail063 x|]).
- Proof.
- intros.
- rewrite tail063_equiv.
- assert (nshiftr x size = 0%int).
-  apply nshiftr_size.
- revert x H H0.
- induction size.
- simpl Z.of_nat.
- intros.
- compute in H0; rewrite H0 in H; discriminate.
-
- intros.
- simpl tail063_alt.
- case_eq (firstr x); intros.
- rewrite (Nat2Z.inj_succ (tail063_alt n (shiftr x))), Z.pow_succ_r; auto with zarith.
- destruct (IHn (shiftr x)) as (y & Hy1 & Hy2).
-
- rewrite phi_nz; rewrite phi_nz in H; contradict H.
- rewrite (sneakl_shiftr x), H1, H; auto.
-
- rewrite <- nshiftr_S_tail; auto.
-
- exists y; split; auto.
- rewrite phi_eqn1; auto.
- rewrite Z.double_spec, Hy2; ring.
-
- exists [|shiftr x|].
- split.
- generalize (phi_bounded (shiftr x)); auto with zarith.
- rewrite phi_eqn2; auto.
- rewrite Z.succ_double_spec; simpl; ring.
- Qed.
-
- (* Sqrt *)
-
- (* Direct transcription of an old proof
-     of a fortran program in boyer-moore *)
-
- Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2).
- Proof.
- case (Z_mod_lt a 2); auto with zarith.
- intros H1; rewrite Zmod_eq_full; auto with zarith.
- Qed.
-
- Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
-   (j * k) + j <= ((j + k)/2 + 1)  ^ 2.
- Proof.
- intros Hj; generalize Hj k; pattern j; apply natlike_ind;
-   auto; clear k j Hj.
- intros _ k Hk; repeat rewrite Z.add_0_l.
- apply  Z.mul_nonneg_nonneg; generalize (Z_div_pos k 2); auto with zarith.
- intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk.
- rewrite Z.mul_0_r, Z.add_0_r, Z.add_0_l.
- generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j));
-   unfold Z.succ.
- rewrite Z.pow_2_r, Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
- auto with zarith.
- intros k Hk _.
- replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1).
- generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)).
- unfold Z.succ; repeat rewrite Z.pow_2_r;
-   repeat rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
- repeat rewrite Z.mul_1_l; repeat rewrite Z.mul_1_r.
- auto with zarith.
- rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith.
- apply f_equal2 with (f := Z.div); auto with zarith.
- Qed.
-
- Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2.
- Proof.
- intros Hi Hj.
- assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith).
- apply Z.lt_le_trans with (2 := sqrt_main_trick _ _ (Z.lt_le_incl _ _ Hj) Hij).
- pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith.
- Qed.
-
- Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2.
- Proof.
- intros Hi.
- assert (H1: 0 <= i - 2) by auto with zarith.
- assert (H2: 1 <= (i / 2) ^ 2); auto with zarith.
-   replace i with (1* 2 + (i - 2)); auto with zarith.
-   rewrite Z.pow_2_r, Z_div_plus_full_l; auto with zarith.
-   generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2).
-   rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l.
-   auto with zarith.
- generalize (quotient_by_2 i).
- rewrite Z.pow_2_r in H2 |- *;
-   repeat (rewrite Z.mul_add_distr_r ||
-           rewrite Z.mul_add_distr_l ||
-           rewrite Z.mul_1_l || rewrite Z.mul_1_r).
-   auto with zarith.
- Qed.
-
- Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i.
- Proof.
- intros Hi Hj Hd; rewrite Z.pow_2_r.
- apply Z.le_trans with (j * (i/j)); auto with zarith.
- apply Z_mult_div_ge; auto with zarith.
- Qed.
-
- Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j ->  (j + (i/j))/2 < j.
- Proof.
- intros Hi Hj H; case (Z.le_gt_cases j ((j + (i/j))/2)); auto.
- intros H1; contradict H; apply Z.le_ngt.
- assert (2 * j <= j + (i/j)); auto with zarith.
- apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith.
- apply Z_mult_div_ge; auto with zarith.
- Qed.
-
- Lemma sqrt63_step_def rec i j:
-   sqrt63_step rec i j =
-   match (fst (i/j) ?= j)%int with
-     Lt => rec i (fst ((j + fst(i/j))/2))%int
-   | _ =>  j
-   end.
- Proof.
- unfold sqrt63_step; case div63; intros.
- simpl; case compare63; auto.
- Qed.
-
- Lemma div63_phi i j: 0 < [|j|] -> [|fst (i/j)%int|] = [|i|]/[|j|].
- intros Hj; generalize (spec_div i j Hj).
- case div63; intros q r; simpl @fst.
- intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
- rewrite H1; ring.
- Qed.
-
- Lemma sqrt63_step_correct rec i j:
-  0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 ->
-   2 * [|j|] < wB ->
-  (forall j1 : int63,
-    0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 ->
-    [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
-  [|sqrt63_step rec i j|] ^ 2 <= [|i|] < ([|sqrt63_step rec i j|] + 1) ^ 2.
- Proof.
- assert (Hp2: 0 < [|2|]) by exact (eq_refl Lt).
- intros Hi Hj Hij H63 Hrec; rewrite sqrt63_step_def.
- rewrite spec_compare, div63_phi; auto.
-   case Z.compare_spec; auto; intros Hc;
-   try (split; auto; apply sqrt_test_true; auto with zarith; fail).
- apply Hrec; repeat rewrite div63_phi; auto with zarith.
- replace [|(j + fst (i / j)%int)|] with ([|j|] + [|i|] / [|j|]).
- split.
- apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj.
- Z.le_elim Hj.
- replace ([|j|] + [|i|]/[|j|]) with
-        (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])); try ring.
- rewrite Z_div_plus_full_l; auto with zarith.
- assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith).
- assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]) ; auto with zarith.
- rewrite <- Hj, Zdiv_1_r.
- replace (1 + [|i|])%Z with (1 * 2 + ([|i|] - 1))%Z; try ring.
- rewrite Z_div_plus_full_l; auto with zarith.
- assert (0 <= ([|i|] - 1) /2)%Z by (apply Z_div_pos; auto with zarith).
- change ([|2|]) with 2%Z; auto with zarith.
- apply sqrt_test_false; auto with zarith.
- rewrite spec_add, div63_phi; auto.
- symmetry; apply Zmod_small.
- split; auto with zarith.
- replace [|j + fst (i / j)%int|] with ([|j|] + [|i|] / [|j|]).
- apply sqrt_main; auto with zarith.
- rewrite spec_add, div63_phi; auto.
- symmetry; apply Zmod_small.
- split; auto with zarith.
- Qed.
-
- Lemma iter63_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
-  [|i|] < ([|j|] + 1) ^ 2 -> 2 * [|j|] < 2 ^ (Z.of_nat size) ->
-  (forall j1, 0 < [|j1|] -> 2^(Z.of_nat n) + [|j1|] <= [|j|] ->
-      [|i|] < ([|j1|] + 1) ^ 2 -> 2 * [|j1|] < 2 ^ (Z.of_nat size) ->
-       [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
-  [|iter63_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter63_sqrt n rec i j|] + 1) ^ 2.
- Proof.
- revert rec i j; elim n; unfold iter63_sqrt; fold iter63_sqrt; clear n.
- intros rec i j Hi Hj Hij H63 Hrec; apply sqrt63_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Z.pow_0_r; auto with zarith.
- intros n Hrec rec i j Hi Hj Hij H63 HHrec.
- apply sqrt63_step_correct; auto.
- intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
- intros j2 Hj2 H2j2 Hjp2 Hj63; apply Hrec; auto with zarith.
- intros j3 Hj3 Hpj3.
- apply HHrec; auto.
- rewrite Nat2Z.inj_succ, Z.pow_succ_r.
- apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith.
- apply Nat2Z.is_nonneg.
- Qed.
-
- Lemma spec_sqrt : forall x,
-       [|sqrt63 x|] ^ 2 <= [|x|] < ([|sqrt63 x|] + 1) ^ 2.
- Proof.
- intros i; unfold sqrt63.
- fold On In Twon.
- rewrite spec_compare. case Z.compare_spec; change [|1|] with 1;
-   intros Hi; auto with zarith.
- repeat rewrite Z.pow_2_r; auto with zarith.
- apply iter63_sqrt_correct; auto with zarith.
-  rewrite div63_phi; change ([|2|]) with 2;  auto with zarith.
-  replace ([|i|]) with (1 * 2 + ([|i|] - 2))%Z; try ring.
-  assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith).
-  rewrite Z_div_plus_full_l; auto with zarith.
-  rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
-  apply sqrt_init; auto.
- rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
- apply Z.le_lt_trans with ([|i|]).
- apply Z_mult_div_ge; auto with zarith.
- case (phi_bounded i); auto.
- intros j2 H1 H2; contradict H2; apply Z.lt_nge.
- rewrite div63_phi; change ([|2|]) with 2; auto with zarith.
- apply Z.le_lt_trans with ([|i|]); auto with zarith.
- assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith).
- apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith.
- apply Z_mult_div_ge; auto with zarith.
- case (phi_bounded i); unfold size; auto with zarith.
- change [|0|] with 0; auto with zarith.
- case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith.
- Qed.
-
- Lemma sqrt632_step_def rec ih il j:
-   sqrt632_step rec ih il j =
-   match (ih ?= j)%int with
-      Eq => j
-    | Gt => j
-    | _ =>
-       match (fst (div6321 ih il j) ?= j)%int with
-         Lt => let m := match j +c fst (div6321 ih il j) with
-                       C0 m1 => fst (m1/2)%int
-                     | C1 m1 => (fst (m1/2) + v30)%int
-                     end in rec ih il m
-       | _ =>  j
-       end
-   end.
- Proof.
- unfold sqrt632_step; case div6321; intros.
- simpl; case compare63; auto.
- Qed.
-
- Lemma sqrt632_lower_bound ih il j:
-   phi2 ih  il  < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|].
- Proof.
- intros H1.
- case (phi_bounded j); intros Hbj _.
- case (phi_bounded il); intros Hbil _.
- case (phi_bounded ih); intros Hbih Hbih1.
- assert (([|ih|] < [|j|] + 1)%Z); auto with zarith.
- apply Z.square_lt_simpl_nonneg; auto with zarith.
- repeat rewrite <-Z.pow_2_r; apply Z.le_lt_trans with (2 := H1).
- apply Z.le_trans with ([|ih|] * base)%Z; unfold phi2, base;
-  try rewrite Z.pow_2_r; auto with zarith.
- Qed.
-
- Lemma div632_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] ->
-  [|fst (div6321 ih il j)|] = phi2 ih il/[|j|])%Z.
- Proof.
- intros Hj Hj1.
- generalize (spec_div21 ih il j Hj Hj1).
- case div6321; intros q r (Hq, Hr).
- apply Zdiv_unique with (phi r); auto with zarith.
- simpl @fst; apply eq_trans with (1 := Hq); ring.
- Qed.
-
- Lemma sqrt632_step_correct rec ih il j:
-  2 ^ 61 <= [|ih|] -> 0 < [|j|] -> phi2 ih il < ([|j|] + 1) ^ 2 ->
-  (forall j1, 0 < [|j1|] < [|j|] ->  phi2 ih il < ([|j1|] + 1) ^ 2 ->
-     [|rec ih il j1|] ^ 2 <= phi2 ih il < ([|rec ih il j1|] + 1) ^ 2) ->
-  [|sqrt632_step rec ih il  j|] ^ 2 <= phi2 ih il
-      < ([|sqrt632_step rec ih il j|] + 1) ^  2.
- Proof.
- assert (Hp2: (0 < [|2|])%Z) by exact (eq_refl Lt).
- intros Hih Hj Hij Hrec; rewrite sqrt632_step_def.
- assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt632_lower_bound with il; auto).
- case (phi_bounded ih); intros Hih1 _.
- case (phi_bounded il); intros Hil1 _.
- case (phi_bounded j); intros _ Hj1.
- assert (Hp3: (0 < phi2 ih il)).
- unfold phi2; apply Z.lt_le_trans with ([|ih|] * base)%Z; auto with zarith.
- apply Z.mul_pos_pos; auto with zarith.
- apply Z.lt_le_trans with (2:= Hih); auto with zarith.
- rewrite spec_compare. case Z.compare_spec; intros Hc1.
- split; auto.
- apply sqrt_test_true; auto.
- unfold phi2, base; auto with zarith.
- unfold phi2; rewrite Hc1.
- assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith).
- rewrite Z.mul_comm, Z_div_plus_full_l; unfold base; auto with zarith.
- simpl wB in Hj1. unfold Z.pow_pos in Hj1. simpl in Hj1. auto with zarith.
- case (Z.le_gt_cases (2 ^ 62) [|j|]); intros Hjj.
- rewrite spec_compare; case Z.compare_spec;
-  rewrite div632_phi; auto; intros Hc;
-  try (split; auto; apply sqrt_test_true; auto with zarith; fail).
- apply Hrec.
- assert (Hf1: 0 <= phi2 ih il/ [|j|]) by (apply Z_div_pos; auto with zarith).
- apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj.
- Z.le_elim Hj.
- 2: contradict Hc; apply Z.le_ngt; rewrite <- Hj, Zdiv_1_r; auto with zarith.
- assert (Hf3: 0 < ([|j|] + phi2 ih il / [|j|]) / 2).
- replace ([|j|] + phi2 ih il/ [|j|])%Z with
-        (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])); try ring.
- rewrite Z_div_plus_full_l; auto with zarith.
- assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2) ; auto with zarith.
- assert (Hf4: ([|j|] + phi2 ih il / [|j|]) / 2 < [|j|]).
- apply sqrt_test_false; auto with zarith.
- generalize (spec_add_c j (fst (div6321 ih il j))).
- unfold interp_carry;  case add63c; intros r;
-  rewrite div632_phi; auto with zarith.
- rewrite div63_phi; change [|2|] with 2%Z; auto with zarith.
- intros HH; rewrite HH; clear HH; auto with zarith.
- rewrite spec_add, div63_phi; change [|2|] with 2%Z; auto.
- rewrite Z.mul_1_l; intros HH.
- rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith.
- change (phi v30 * 2) with (2 ^ Z.of_nat size).
- rewrite HH, Zmod_small; auto with zarith.
- replace (phi
-    match j +c fst (div6321 ih il j) with
-    | C0 m1 => fst (m1 / 2)%int
-    | C1 m1 => fst (m1 / 2)%int + v30
-    end) with ((([|j|] + (phi2 ih il)/([|j|]))/2)).
- apply sqrt_main; auto with zarith.
- generalize (spec_add_c j (fst (div6321 ih il j))).
- unfold interp_carry;  case add63c; intros r;
-  rewrite div632_phi; auto with zarith.
- rewrite div63_phi; auto with zarith.
- intros HH; rewrite HH; auto with zarith.
- intros HH; rewrite <- HH.
- change (1 * 2 ^ Z.of_nat size) with (phi (v30) * 2).
- rewrite Z_div_plus_full_l; auto with zarith.
- rewrite Z.add_comm.
- rewrite spec_add, Zmod_small.
- rewrite div63_phi; auto.
- split; auto with zarith.
- case (phi_bounded (fst (r/2)%int));
-   case (phi_bounded v30); auto with zarith.
- rewrite div63_phi; change (phi 2) with 2%Z; auto.
- change (2 ^Z.of_nat size) with (base/2 + phi v30).
- assert (phi r / 2 < base/2); auto with zarith.
- apply Z.mul_lt_mono_pos_r with 2; auto with zarith.
- change (base/2 * 2) with base.
- apply Z.le_lt_trans with (phi r).
- rewrite Z.mul_comm; apply Z_mult_div_ge; auto with zarith.
- case (phi_bounded r); auto with zarith.
- contradict Hij; apply Z.le_ngt.
- assert ((1 + [|j|]) <= 2 ^ 62); auto with zarith.
- apply Z.le_trans with ((2 ^ 62) * (2 ^ 62)); auto with zarith.
- assert (0 <= 1 + [|j|]); auto with zarith.
- apply Z.mul_le_mono_nonneg; auto with zarith.
- change ((2 ^ 62) * (2 ^ 62)) with ((2 ^ 61) * base).
- apply Z.le_trans with ([|ih|] * base); auto with zarith.
- unfold phi2, base; auto with zarith.
- split; auto.
- apply sqrt_test_true; auto.
- unfold phi2, base; auto with zarith.
- apply Z.le_ge; apply Z.le_trans with (([|j|] * base)/[|j|]).
- rewrite Z.mul_comm, Z_div_mult; auto with zarith.
- apply Z.ge_le; apply Z_div_ge; auto with zarith.
- Qed.
-
- Lemma iter632_sqrt_correct n rec ih il j:
-  2^61 <= [|ih|] ->  0 < [|j|] -> phi2 ih il < ([|j|] + 1) ^ 2 ->
-  (forall j1, 0 < [|j1|] -> 2^(Z.of_nat n) + [|j1|] <= [|j|] ->
-      phi2 ih il < ([|j1|] + 1) ^ 2 ->
-       [|rec ih il j1|] ^ 2 <= phi2 ih il < ([|rec ih il j1|] + 1) ^ 2)  ->
-  [|iter632_sqrt n rec ih il j|] ^ 2 <= phi2 ih il
-      < ([|iter632_sqrt n rec ih il j|] + 1) ^ 2.
- Proof.
- revert rec ih il j; elim n; unfold iter632_sqrt; fold iter632_sqrt; clear n.
- intros rec ih il j Hi Hj Hij Hrec; apply sqrt632_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Z.pow_0_r; auto with zarith.
- intros n Hrec rec ih il j Hi Hj Hij HHrec.
- apply sqrt632_step_correct; auto.
- intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
- intros j2 Hj2 H2j2 Hjp2; apply Hrec; auto with zarith.
- intros j3 Hj3 Hpj3.
- apply HHrec; auto.
- rewrite Nat2Z.inj_succ, Z.pow_succ_r.
- apply Z.le_trans with (2 ^Z.of_nat n + [|j2|])%Z; auto with zarith.
- apply Nat2Z.is_nonneg.
- Qed.
-
- (* Avoid expanding [iter632_sqrt] before variables in the context. *)
- Strategy 1 [iter632_sqrt].
-
- Lemma spec_sqrt2 : forall x y,
-       wB/ 4 <= [|x|] ->
-       let (s,r) := sqrt632 x y in
-          [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
-          [+|r|] <= 2 * [|s|].
- Proof.
- intros ih il Hih; unfold sqrt632.
- fold On In.
- change [||WW ih il||] with (phi2 ih il).
- assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by
-  (intros s; ring).
- assert (Hb: 0 <= base) by (red; intros HH; discriminate).
- assert (Hi2: phi2 ih il < (phi Tn + 1) ^ 2).
- { change ((phi Tn + 1) ^ 2) with (2^126).
-   apply Z.le_lt_trans with ((2^63 -1) * base + (2^63 - 1)); auto with zarith.
-   2: simpl; unfold Z.pow_pos; simpl; auto with zarith.
-   case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4.
-   unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4.
-   unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. }
- case (iter632_sqrt_correct 63 (fun _ _ j => j) ih il Tn); auto with zarith.
- change [|Tn|] with 9223372036854775807; auto with zarith.
- intros j1 _ HH; contradict HH.
- apply Z.lt_nge.
- change [|Tn|] with 9223372036854775807; auto with zarith.
- change (2 ^ Z.of_nat 63) with 9223372036854775808; auto with zarith.
- case (phi_bounded j1); auto with zarith.
- set (s := iter632_sqrt 63 (fun _ _ j : int63 => j) ih il Tn).
- intros Hs1 Hs2.
- generalize (spec_mul_c s s); case mul63c.
- simpl zn2z_to_Z; intros HH.
- assert ([|s|] = 0).
- { symmetry in HH. rewrite Z.mul_eq_0 in HH. destruct HH; auto. }
- contradict Hs2; apply Z.le_ngt; rewrite H.
- change ((0 + 1) ^ 2) with 1.
- apply Z.le_trans with (2 ^ Z.of_nat size / 4 * base).
- simpl; auto with zarith.
- apply Z.le_trans with ([|ih|] * base); auto with zarith.
- unfold phi2; case (phi_bounded il); auto with zarith.
- intros ih1 il1.
- change [||WW ih1 il1||] with (phi2 ih1 il1).
- intros Hihl1.
- generalize (spec_sub_c il il1).
- case sub63c; intros il2 Hil2.
- rewrite spec_compare; case Z.compare_spec.
- unfold interp_carry in *.
- intros H1; split.
- rewrite Z.pow_2_r, <- Hihl1.
- unfold phi2; ring[Hil2 H1].
- replace [|il2|] with (phi2 ih il - phi2 ih1 il1).
- rewrite Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
- unfold phi2; rewrite H1, Hil2; ring.
- unfold interp_carry.
- intros H1; contradict Hs1.
- apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
- unfold phi2.
- case (phi_bounded il); intros _ H2.
- apply Z.lt_le_trans with (([|ih|] + 1) * base + 0).
- rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith.
- case (phi_bounded il1); intros H3 _.
- apply Z.add_le_mono; auto with zarith.
- unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base.
- rewrite Z.pow_2_r, <- Hihl1, Hil2.
- intros H1.
- rewrite <- Z.le_succ_l, <- Z.add_1_r in H1.
- Z.le_elim H1.
- contradict Hs2; apply Z.le_ngt.
- replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1).
- unfold phi2.
- case (phi_bounded il); intros Hpil _.
- assert (Hl1l: [|il1|] <= [|il|]).
- { case (phi_bounded il2); rewrite Hil2; auto with zarith. }
- assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base); auto with zarith.
- case (phi_bounded s);  change (2 ^ Z.of_nat size) with base; intros _ Hps.
- case (phi_bounded ih1); intros Hpih1 _; auto with zarith.
- apply Z.le_trans with (([|ih1|] + 2) * base); auto with zarith.
- rewrite Z.mul_add_distr_r.
- assert (2 * [|s|] + 1 <= 2 * base); auto with zarith.
- rewrite Hihl1, Hbin; auto.
- split.
- unfold phi2; rewrite <- H1; ring.
- replace (base + ([|il|] - [|il1|])) with (phi2 ih il - ([|s|] * [|s|])).
- rewrite <-Hbin in Hs2; auto with zarith.
- rewrite <- Hihl1; unfold phi2; rewrite <- H1; ring.
- unfold interp_carry in Hil2 |- *.
- unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base.
- assert (Hsih: [|ih - 1|] = [|ih|] - 1).
- { rewrite spec_sub, Zmod_small; auto; change [|1|] with 1.
-   case (phi_bounded ih); intros H1 H2.
-   generalize Hih; change (2 ^ Z.of_nat size / 4) with 2305843009213693952.
-   split; auto with zarith. }
- rewrite spec_compare; case Z.compare_spec.
- rewrite Hsih.
- intros H1; split.
- rewrite Z.pow_2_r, <- Hihl1.
- unfold phi2; rewrite <-H1.
- transitivity ([|ih|] * base + [|il1|] + ([|il|] - [|il1|])).
- ring.
- rewrite <-Hil2.
- change (2 ^ Z.of_nat size) with base; ring.
- replace [|il2|] with (phi2 ih il - phi2 ih1 il1).
- rewrite Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
- unfold phi2.
- rewrite <-H1.
- ring_simplify.
- transitivity (base + ([|il|] - [|il1|])).
- ring.
- rewrite <-Hil2.
- change (2 ^ Z.of_nat size) with base; ring.
- rewrite Hsih; intros H1.
- assert (He: [|ih|] = [|ih1|]).
- { apply Z.le_antisymm; auto with zarith.
-   case (Z.le_gt_cases [|ih1|] [|ih|]); auto; intros H2.
-   contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
-   unfold phi2.
-   case (phi_bounded il); change (2 ^ Z.of_nat size) with base;
-    intros _ Hpil1.
-   apply Z.lt_le_trans with (([|ih|] + 1) * base).
-   rewrite Z.mul_add_distr_r, Z.mul_1_l; auto with zarith.
-   case (phi_bounded il1); intros Hpil2 _.
-   apply Z.le_trans with (([|ih1|]) * base); auto with zarith. }
- rewrite Z.pow_2_r, <-Hihl1; unfold phi2; rewrite <-He.
- contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1.
- unfold phi2; rewrite He.
- assert (phi il - phi il1 < 0); auto with zarith.
- rewrite <-Hil2.
- case (phi_bounded il2); auto with zarith.
- intros H1.
- rewrite Z.pow_2_r, <-Hihl1.
- assert (H2 : [|ih1|]+2 <= [|ih|]); auto with zarith.
- Z.le_elim H2.
- contradict Hs2; apply Z.le_ngt.
- replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1).
- unfold phi2.
- assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|]));
-  auto with zarith.
- rewrite <-Hil2.
- change (-1 * 2 ^ Z.of_nat size) with (-base).
- case (phi_bounded il2); intros Hpil2 _.
- apply Z.le_trans with ([|ih|] * base + - base); auto with zarith.
- case (phi_bounded s);  change (2 ^ Z.of_nat size) with base; intros _ Hps.
- assert (2 * [|s|] + 1 <= 2 * base); auto with zarith.
- apply Z.le_trans with ([|ih1|] * base + 2 * base); auto with zarith.
- assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base); auto with zarith.
- rewrite Z.mul_add_distr_r in Hi; auto with zarith.
- rewrite Hihl1, Hbin; auto.
- unfold phi2; rewrite <-H2.
- split.
- replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
- rewrite <-Hil2.
- change (-1 * 2 ^ Z.of_nat size) with (-base); ring.
- replace (base + [|il2|]) with (phi2 ih il - phi2 ih1 il1).
- rewrite Hihl1.
- rewrite <-Hbin in Hs2; auto with zarith.
- unfold phi2; rewrite <-H2.
- replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
- rewrite <-Hil2.
- change (-1 * 2 ^ Z.of_nat size) with (-base); ring.
-Qed.
-
- (** [iszero] *)
-
- Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0.
- Proof.
- clear; unfold ZnZ.eq0, int63_ops.
- unfold compare63; intros.
- change [|0|] with 0 in H.
- apply Z.compare_eq.
- now destruct ([|x|] ?= 0).
- Qed.
-
- (* Even *)
-
- Lemma spec_is_even : forall x,
-      if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
- Proof.
- unfold ZnZ.is_even, int63_ops; intros.
- generalize (spec_div x 2).
- destruct (x/2)%int as (q,r); intros.
- unfold compare63.
- change [|2|] with 2 in H.
- change [|0|] with 0.
- destruct H; auto with zarith.
- replace ([|x|] mod 2) with [|r|].
- destruct H; auto with zarith.
- case Z.compare_spec; auto with zarith.
- apply Zmod_unique with [|q|]; auto with zarith.
- Qed.
-
- (* Bitwise *)
-
- Lemma log2_phi_bounded x : Z.log2 [|x|] < Z.of_nat size.
- Proof.
-  destruct (phi_bounded x) as (H,H').
-  Z.le_elim H.
-  - now apply Z.log2_lt_pow2.
-  - now rewrite <- H.
- Qed.
-
- Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].
- Proof.
- unfold ZnZ.lor,int63_ops. unfold lor63.
- rewrite phi_phi_inv.
- apply Z.mod_small; split; trivial.
- - apply Z.lor_nonneg; split; apply phi_bounded.
- - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
-   rewrite Z.log2_lor; try apply phi_bounded.
-   apply Z.max_lub_lt; apply log2_phi_bounded.
- Qed.
-
- Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].
- Proof.
- unfold ZnZ.land, int63_ops. unfold land63.
- rewrite phi_phi_inv.
- apply Z.mod_small; split; trivial.
- - apply Z.land_nonneg; left; apply phi_bounded.
- - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
-   eapply Z.le_lt_trans.
-   apply Z.log2_land; try apply phi_bounded.
-   apply Z.min_lt_iff; left; apply log2_phi_bounded.
- Qed.
-
- Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].
- Proof.
- unfold ZnZ.lxor, int63_ops. unfold lxor63.
- rewrite phi_phi_inv.
- apply Z.mod_small; split; trivial.
- - apply Z.lxor_nonneg; split; intros; apply phi_bounded.
- - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
-   eapply Z.le_lt_trans.
-   apply Z.log2_lxor; try apply phi_bounded.
-   apply Z.max_lub_lt; apply log2_phi_bounded.
- Qed.
-
- Global Instance int63_specs : ZnZ.Specs int63_ops := {
-    spec_to_Z   := phi_bounded;
-    spec_of_pos := positive_to_int63_spec;
-    spec_zdigits := spec_zdigits;
-    spec_more_than_1_digit := spec_more_than_1_digit;
-    spec_0   := spec_0;
-    spec_1   := spec_1;
-    spec_m1  := spec_m1;
-    spec_compare := spec_compare;
-    spec_eq0 := spec_eq0;
-    spec_opp_c := spec_opp_c;
-    spec_opp := spec_opp;
-    spec_opp_carry := spec_opp_carry;
-    spec_succ_c := spec_succ_c;
-    spec_add_c := spec_add_c;
-    spec_add_carry_c := spec_add_carry_c;
-    spec_succ := spec_succ;
-    spec_add := spec_add;
-    spec_add_carry := spec_add_carry;
-    spec_pred_c := spec_pred_c;
-    spec_sub_c := spec_sub_c;
-    spec_sub_carry_c := spec_sub_carry_c;
-    spec_pred := spec_pred;
-    spec_sub := spec_sub;
-    spec_sub_carry := spec_sub_carry;
-    spec_mul_c := spec_mul_c;
-    spec_mul := spec_mul;
-    spec_square_c := spec_square_c;
-    spec_div21 := spec_div21;
-    spec_div_gt := fun a b _ => spec_div a b;
-    spec_div := spec_div;
-    spec_modulo_gt := fun a b _ => spec_mod a b;
-    spec_modulo := spec_mod;
-    spec_gcd_gt := fun a b _ => spec_gcd a b;
-    spec_gcd := spec_gcd;
-    spec_head00 := spec_head00;
-    spec_head0 := spec_head0;
-    spec_tail00 := spec_tail00;
-    spec_tail0 := spec_tail0;
-    spec_add_mul_div := spec_add_mul_div;
-    spec_pos_mod := spec_pos_mod;
-    spec_is_even := spec_is_even;
-    spec_sqrt2 := spec_sqrt2;
-    spec_sqrt := spec_sqrt;
-    spec_lor := spec_lor;
-    spec_land := spec_land;
-    spec_lxor := spec_lxor }.
-
-End Int63_Specs.
-
-
-Module Int63Cyclic <: CyclicType.
-  Definition t := int63.
-  Definition ops := int63_ops.
-  Definition specs := int63_specs.
-End Int63Cyclic.
diff --git a/src/versions/standard/Int63/Int63Lib_standard.v b/src/versions/standard/Int63/Int63Lib_standard.v
deleted file mode 100644
index 4d21346..0000000
--- a/src/versions/standard/Int63/Int63Lib_standard.v
+++ /dev/null
@@ -1,487 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2016                                          *)
-(*                                                                        *)
-(*     Chantal Keller                                                     *)
-(*                                                                        *)
-(*       from the Int31 library                                           *)
-(*         by Arnaud Spiwack and Pierre Letouzey                          *)
-(*       and the Int63 library of native-coq                              *)
-(*         by Benjamin Gregoire and Laurent Thery                         *)
-(*                                                                        *)
-(*     Inria - École Polytechnique - Université Paris-Sud                 *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-Require Import NaryFunctions.
-Require Import Wf_nat.
-Require Export ZArith.
-Require Export DoubleType.
-
-(** * 63-bit integers *)
-
-(** This file contains basic definitions of a 63-bit integer arithmetic.
-  It is based on the Int31 library, using its genericity. *)
-
-Definition size := 63%nat.
-
-(** Digits *)
-
-Inductive digits : Type := D0 | D1.
-
-(** The type of 63-bit integers *)
-
-(** The type [int63] has a unique constructor [I63] that expects
-   63 arguments of type [digits]. *)
-
-Definition digits63 t := Eval compute in nfun digits size t.
-
-Inductive int63 : Type := I63 : digits63 int63.
-
-Notation int := int63.
-
-(* spiwack: Registration of the type of integers, so that the matchs in
-   the functions below perform dynamic decompilation (otherwise some segfault
-   occur when they are applied to one non-closed term and one closed term). *)
-
-Delimit Scope int63_scope with int.
-Bind Scope int63_scope with int.
-Local Open Scope int63_scope.
-
-(** * Constants *)
-
-(** Zero is [I63 D0 ... D0] *)
-Definition On : int63 := Eval compute in napply_cst _ _ D0 size I63.
-Notation "0" := On : int63_scope.
-
-(** One is [I63 D0 ... D0 D1] *)
-Definition In : int63 := Eval compute in (napply_cst _ _ D0 (size-1) I63) D1.
-Notation "1" := In : int63_scope.
-
-(** The biggest integer is [I63 D1 ... D1], corresponding to [(2^size)-1] *)
-Definition Tn : int63 := Eval compute in napply_cst _ _ D1 size I63.
-
-(** Two is [I63 D0 ... D0 D1 D0] *)
-Definition Twon : int63 := Eval compute in (napply_cst _ _ D0 (size-2) I63) D1 D0.
-Notation "2" := Twon : int63_scope.
-
-(** * Bits manipulation *)
-
-
-(** [sneakr b x] shifts [x] to the right by one bit.
-   Rightmost digit is lost while leftmost digit becomes [b].
-   Pseudo-code is
-    [ match x with (I63 d0 ... dN) => I63 b d0 ... d(N-1) end ]
-*)
-
-Definition sneakr : digits -> int63 -> int63 := Eval compute in
- fun b => int63_rect _ (napply_except_last _ _ (size-1) (I63 b)).
-
-(** [sneakl b x] shifts [x] to the left by one bit.
-   Leftmost digit is lost while rightmost digit becomes [b].
-   Pseudo-code is
-    [ match x with (I63 d0 ... dN) => I63 d1 ... dN b end ]
-*)
-
-Definition sneakl : digits -> int63 -> int63 := Eval compute in
- fun b => int63_rect _ (fun _ => napply_then_last _ _ b (size-1) I63).
-
-
-(** [shiftl], [shiftr], [twice] and [twice_plus_one] are direct
-    consequences of [sneakl] and [sneakr]. *)
-
-Definition shiftl := sneakl D0.
-Definition shiftr := sneakr D0.
-Definition twice := sneakl D0.
-Definition twice_plus_one := sneakl D1.
-
-(** [firstl x] returns the leftmost digit of number [x].
-    Pseudo-code is [ match x with (I63 d0 ... dN) => d0 end ] *)
-
-Definition firstl : int63 -> digits := Eval compute in
- int63_rect _ (fun d => napply_discard _ _ d (size-1)).
-
-(** [firstr x] returns the rightmost digit of number [x].
-    Pseudo-code is [ match x with (I63 d0 ... dN) => dN end ] *)
-
-Definition firstr : int63 -> digits := Eval compute in
- int63_rect _ (napply_discard _ _ (fun d=>d) (size-1)).
-
-(** [iszero x] is true iff [x = I63 D0 ... D0]. Pseudo-code is
-    [ match x with (I63 D0 ... D0) => true | _ => false end ] *)
-
-Definition iszero : int63 -> bool := Eval compute in
- let f d b := match d with D0 => b | D1 => false end
- in int63_rect _ (nfold_bis _ _ f true size).
-
-(* NB: DO NOT transform the above match in a nicer (if then else).
-   It seems to work, but later "unfold iszero" takes forever. *)
-
-
-(** [base] is [2^63], obtained via iterations of [Z.double].
-   It can also be seen as the smallest b > 0 s.t. phi_inv b = 0
-   (see below) *)
-
-Definition base := Eval compute in
- iter_nat size Z Z.double 1%Z.
-
-(** * Recursors *)
-
-Fixpoint recl_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
- (i:int63) : A :=
-  match n with
-  | O => case0
-  | S next =>
-          if iszero i then
-             case0
-          else
-             let si := shiftl i in
-             caserec (firstl i) si (recl_aux next A case0 caserec si)
-  end.
-
-Fixpoint recr_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int63->A->A)
- (i:int63) : A :=
-  match n with
-  | O => case0
-  | S next =>
-          if iszero i then
-             case0
-          else
-             let si := shiftr i in
-             caserec (firstr i) si (recr_aux next A case0 caserec si)
-  end.
-
-Definition recl := recl_aux size.
-Definition recr := recr_aux size.
-
-(** * Conversions *)
-
-(** From int63 to Z, we simply iterates [Z.double] or [Z.succ_double]. *)
-
-Definition phi : int63 -> Z :=
- recr Z (0%Z)
-  (fun b _ => match b with D0 => Z.double | D1 => Z.succ_double end).
-
-(** From positive to int63. An abstract definition could be :
-      [ phi_inv (2n) = 2*(phi_inv n) /\
-        phi_inv 2n+1 = 2*(phi_inv n) + 1 ] *)
-
-Fixpoint phi_inv_positive p :=
-  match p with
-    | xI q => twice_plus_one (phi_inv_positive q)
-    | xO q => twice (phi_inv_positive q)
-    | xH => In
-  end.
-
-(** The negative part : 2-complement  *)
-
-Fixpoint complement_negative p :=
-  match p with
-    | xI q => twice (complement_negative q)
-    | xO q => twice_plus_one (complement_negative q)
-    | xH => twice Tn
-  end.
-
-(** A simple incrementation function *)
-
-Definition incr : int63 -> int63 :=
- recr int63 In
-   (fun b si rec => match b with
-     | D0 => sneakl D1 si
-     | D1 => sneakl D0 rec end).
-
-(** We can now define the conversion from Z to int63. *)
-
-Definition phi_inv : Z -> int63 := fun n =>
- match n with
- | Z0 => On
- | Zpos p => phi_inv_positive p
- | Zneg p => incr (complement_negative p)
- end.
-
-(** [phi_inv2] is similar to [phi_inv] but returns a double word
-    [zn2z int63] *)
-
-Definition phi_inv2 n :=
-  match n with
-  | Z0 => W0
-  | _ => WW (phi_inv (n/base)%Z) (phi_inv n)
-  end.
-
-(** [phi2] is similar to [phi] but takes a double word (two args) *)
-
-Definition phi2 nh nl :=
-  ((phi nh)*base+(phi nl))%Z.
-
-(** * Addition *)
-
-(** Addition modulo [2^63] *)
-
-Definition add63 (n m : int63) := phi_inv ((phi n)+(phi m)).
-Notation "n + m" := (add63 n m) : int63_scope.
-
-(** Addition with carry (the result is thus exact) *)
-
-(* spiwack : when executed in non-compiled*)
-(* mode, (phi n)+(phi m) is computed twice*)
-(* it may be considered to optimize it *)
-
-Definition add63c (n m : int63) :=
-  let npm := n+m in
-  match (phi npm ?= (phi n)+(phi m))%Z with
-  | Eq => C0 npm
-  | _ => C1 npm
-  end.
-Notation "n '+c' m" := (add63c n m) (at level 50, no associativity) : int63_scope.
-
-(**  Addition plus one with carry (the result is thus exact) *)
-
-Definition add63carryc (n m : int63) :=
-  let npmpone_exact := ((phi n)+(phi m)+1)%Z in
-  let npmpone := phi_inv npmpone_exact in
-  match (phi npmpone ?= npmpone_exact)%Z with
-  | Eq => C0 npmpone
-  | _ => C1 npmpone
-  end.
-
-(** * Substraction *)
-
-(** Subtraction modulo [2^63] *)
-
-Definition sub63 (n m : int63) := phi_inv ((phi n)-(phi m)).
-Notation "n - m" := (sub63 n m) : int63_scope.
-
-(** Subtraction with carry (thus exact) *)
-
-Definition sub63c (n m : int63) :=
-  let nmm := n-m in
-  match (phi nmm ?= (phi n)-(phi m))%Z with
-  | Eq => C0 nmm
-  | _ => C1 nmm
-  end.
-Notation "n '-c' m" := (sub63c n m) (at level 50, no associativity) : int63_scope.
-
-(** subtraction minus one with carry (thus exact) *)
-
-Definition sub63carryc (n m : int63) :=
-  let nmmmone_exact := ((phi n)-(phi m)-1)%Z in
-  let nmmmone := phi_inv nmmmone_exact in
-  match (phi nmmmone ?= nmmmone_exact)%Z with
-  | Eq => C0 nmmmone
-  | _ => C1 nmmmone
-  end.
-
-(** Opposite *)
-
-Definition opp63 x := On - x.
-Notation "- x" := (opp63 x) : int63_scope.
-
-(** Multiplication *)
-
-(** multiplication modulo [2^63] *)
-
-Definition mul63 (n m : int63) := phi_inv ((phi n)*(phi m)).
-Notation "n * m" := (mul63 n m) : int63_scope.
-
-(** multiplication with double word result (thus exact) *)
-
-Definition mul63c (n m : int63) := phi_inv2 ((phi n)*(phi m)).
-Notation "n '*c' m" := (mul63c n m) (at level 40, no associativity) : int63_scope.
-
-
-(** * Division *)
-
-(** Division of a double size word modulo [2^63] *)
-
-Definition div6321 (nh nl m : int63) :=
-  let (q,r) := Z.div_eucl (phi2 nh nl) (phi m) in
-  (phi_inv q, phi_inv r).
-
-(** Division modulo [2^63] *)
-
-Definition div63 (n m : int63) :=
-  let (q,r) := Z.div_eucl (phi n) (phi m) in
-  (phi_inv q, phi_inv r).
-Notation "n / m" := (div63 n m) : int63_scope.
-
-
-(** * Unsigned comparison *)
-
-Definition compare63 (n m : int63) := ((phi n)?=(phi m))%Z.
-Notation "n ?= m" := (compare63 n m) (at level 70, no associativity) : int63_scope.
-
-Definition eqb63 (n m : int63) :=
- match n ?= m with Eq => true | _ => false end.
-
-
-(** Computing the [i]-th iterate of a function:
-    [iter_int63 i A f = f^i] *)
-
-Definition iter_int63 i A f :=
-  recr (A->A) (fun x => x)
-   (fun b si rec => match b with
-      | D0 => fun x => rec (rec x)
-      | D1 => fun x => f (rec (rec x))
-    end)
-    i.
-
-(** Combining the [(63-p)] low bits of [i] above the [p] high bits of [j]:
-    [addmuldiv63 p i j = i*2^p+j/2^(63-p)]  (modulo [2^63]) *)
-
-Definition addmuldiv63 p i j :=
- let (res, _ ) :=
- iter_int63 p (int63*int63)
-  (fun ij => let (i,j) := ij in (sneakl (firstl j) i, shiftl j))
-  (i,j)
- in
- res.
-
-(** Bitwise operations *)
-
-Definition lor63 n m := phi_inv (Z.lor (phi n) (phi m)).
-Definition land63 n m := phi_inv (Z.land (phi n) (phi m)).
-Definition lxor63 n m := phi_inv (Z.lxor (phi n) (phi m)).
-
-(* Register add63 as int63 plus in "coq_int63" by True. *)
-(* Register add63c as int63 plusc in "coq_int63" by True. *)
-(* Register add63carryc as int63 pluscarryc in "coq_int63" by True. *)
-(* Register sub63 as int63 minus in "coq_int63" by True. *)
-(* Register sub63c as int63 minusc in "coq_int63" by True. *)
-(* Register sub63carryc as int63 minuscarryc in "coq_int63" by True. *)
-(* Register mul63 as int63 times in "coq_int63" by True. *)
-(* Register mul63c as int63 timesc in "coq_int63" by True. *)
-(* Register div6321 as int63 div21 in "coq_int63" by True. *)
-(* Register div63 as int63 diveucl in "coq_int63" by True. *)
-(* Register compare63 as int63 compare in "coq_int63" by True. *)
-(* Register addmuldiv63 as int63 addmuldiv in "coq_int63" by True. *)
-(* Register lor63 as int63 lor in "coq_int63" by True. *)
-(* Register land63 as int63 land in "coq_int63" by True. *)
-(* Register lxor63 as int63 lxor in "coq_int63" by True. *)
-
-Definition lnot63 n := lxor63 Tn n.
-Definition ldiff63 n m := land63 n (lnot63 m).
-
-Fixpoint euler (guard:nat) (i j:int63) {struct guard} :=
-  match guard with
-    | O => In
-    | S p => match j ?= On with
-               | Eq => i
-               | _ => euler p j (let (_, r ) := i/j in r)
-             end
-  end.
-
-Definition gcd63 (i j:int63) := euler (2*size)%nat i j.
-
-(** Square root functions using newton iteration
-    we use a very naive upper-bound on the iteration
-    2^63 instead of the usual 63.
-**)
-
-
-
-Definition sqrt63_step (rec: int63 -> int63 -> int63) (i j: int63)  :=
-Eval lazy delta [Twon] in
-  let (quo,_) := i/j in
-  match quo ?= j with
-    Lt => rec i (fst ((j + quo)/Twon))
-  | _ =>  j
-  end.
-
-Fixpoint iter63_sqrt (n: nat) (rec: int63 -> int63 -> int63)
-          (i j: int63) {struct n} : int63 :=
-  sqrt63_step
-   (match n with
-      O =>  rec
-   | S n => (iter63_sqrt n (iter63_sqrt n rec))
-   end) i j.
-
-Definition sqrt63 i :=
-Eval lazy delta [On In Twon] in
-  match compare63 In i with
-    Gt => On
-  | Eq => In
-  | Lt => iter63_sqrt 63 (fun i j => j) i (fst (i/Twon))
-  end.
-
-Definition v30 := Eval compute in (addmuldiv63 (phi_inv (Z.of_nat size - 1)) In On).
-
-Definition sqrt632_step (rec: int63 -> int63 -> int63 -> int63)
-   (ih il j: int63)  :=
-Eval lazy delta [Twon v30] in
-  match ih ?= j with Eq => j | Gt => j | _ =>
-  let (quo,_) := div6321 ih il j in
-  match quo ?= j with
-    Lt => let m := match j +c quo with
-                    C0 m1 => fst (m1/Twon)
-                  | C1 m1 => fst (m1/Twon) + v30
-                  end in rec ih il m
-  | _ =>  j
-  end end.
-
-Fixpoint iter632_sqrt (n: nat)
-          (rec: int63  -> int63 -> int63 -> int63)
-          (ih il j: int63) {struct n} : int63 :=
-  sqrt632_step
-   (match n with
-      O =>  rec
-   | S n => (iter632_sqrt n (iter632_sqrt n rec))
-   end) ih il j.
-
-Definition sqrt632 ih il :=
-Eval lazy delta [On In] in
-  let s := iter632_sqrt 63 (fun ih il j => j) ih il Tn in
-           match s *c s with
-            W0 => (On, C0 On) (* impossible *)
-          | WW ih1 il1 =>
-             match il -c il1 with
-                C0 il2 =>
-                  match ih ?= ih1 with
-                    Gt => (s, C1 il2)
-                  | _  => (s, C0 il2)
-                  end
-              | C1 il2 =>
-                  match (ih - In) ?= ih1 with (* we could parametrize ih - 1 *)
-                    Gt => (s, C1 il2)
-                  | _  => (s, C0 il2)
-                  end
-              end
-          end.
-
-
-Fixpoint p2i n p : (N*int63)%type :=
-  match n with
-    | O => (Npos p, On)
-    | S n => match p with
-               | xO p => let (r,i) := p2i n p in (r, Twon*i)
-               | xI p => let (r,i) := p2i n p in (r, Twon*i+In)
-               | xH => (N0, In)
-             end
-  end.
-
-Definition positive_to_int63 (p:positive) := p2i size p.
-
-(** Constant 63 converted into type int63.
-    It is used as default answer for numbers of zeros
-    in [head0] and [tail0] *)
-
-Definition T63 : int63 := Eval compute in phi_inv (Z.of_nat size).
-
-Definition head063 (i:int63) :=
-  recl _ (fun _ => T63)
-   (fun b si rec n => match b with
-     | D0 => rec (add63 n In)
-     | D1 => n
-    end)
-   i On.
-
-Definition tail063 (i:int63) :=
-  recr _ (fun _ => T63)
-   (fun b si rec n => match b with
-     | D0 => rec (add63 n In)
-     | D1 => n
-    end)
-   i On.
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
index 6b480b0..865c238 100644
--- a/src/versions/standard/Int63/Int63_standard.v
+++ b/src/versions/standard/Int63/Int63_standard.v
@@ -20,7 +20,6 @@
 (** Naive software representation of Int63. To improve. Anyway, if you
     want efficiency, rather use native-coq. **)
 
-(* Require Export Cyclic31. *)
 Require Export Ring31.
 Require Export Int63Native.
 Require Export Int63Op.
diff --git a/src/versions/standard/Int63/Ring63_standard.v b/src/versions/standard/Int63/Ring63_standard.v
deleted file mode 100644
index 7041c79..0000000
--- a/src/versions/standard/Int63/Ring63_standard.v
+++ /dev/null
@@ -1,125 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2016                                          *)
-(*                                                                        *)
-(*     Chantal Keller                                                     *)
-(*                                                                        *)
-(*       from the Int31 library                                           *)
-(*         by Arnaud Spiwack and Pierre Letouzey                          *)
-(*       and the Int63 library of native-coq                              *)
-(*         by Benjamin Gregoire and Laurent Thery                         *)
-(*                                                                        *)
-(*     Inria - École Polytechnique - Université Paris-Sud                 *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-(** * Int63 numbers defines Z/(2^63)Z, and can hence be equipped
-      with a ring structure and a ring tactic *)
-
-Require Import Int63Lib Cyclic63 CyclicAxioms.
-
-Local Open Scope int63_scope.
-
-(** Detection of constants *)
-
-Local Open Scope list_scope.
-
-Ltac isInt63cst_lst l :=
- match l with
- | nil => constr:true
- | ?t::?l => match t with
-               | D1 => isInt63cst_lst l
-               | D0 => isInt63cst_lst l
-               | _ => constr:false
-             end
- | _ => constr:false
- end.
-
-Ltac isInt63cst t :=
- match t with
- | I63 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
-       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
-       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30
-       ?i31 ?i32 ?i33 ?i34 ?i35 ?i36 ?i37 ?i38 ?i39 ?i40
-       ?i41 ?i42 ?i43 ?i44 ?i45 ?i46 ?i47 ?i48 ?i49 ?i50
-       ?i51 ?i52 ?i53 ?i54 ?i55 ?i56 ?i57 ?i58 ?i59 ?i60
-       ?i61 ?i62 =>
-    let l :=
-      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
-      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
-      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30
-      ::i31::i32::i33::i34::i35::i36::i37::i38::i39::i40
-      ::i41::i42::i43::i44::i45::i46::i47::i48::i49::i50
-      ::i51::i52::i53::i54::i55::i56::i57::i58::i59::i60
-      ::i61::i62::nil)
-    in isInt63cst_lst l
- | Int63Lib.On => constr:true
- | Int63Lib.In => constr:true
- | Int63Lib.Tn => constr:true
- | Int63Lib.Twon => constr:true
- | _ => constr:false
- end.
-
-Ltac Int63cst t :=
- match isInt63cst t with
- | true => constr:t
- | false => constr:NotConstant
- end.
-
-(** The generic ring structure inferred from the Cyclic structure *)
-
-Module Int63ring := CyclicRing Int63Cyclic.
-
-(** Unlike in the generic [CyclicRing], we can use Leibniz here. *)
-
-Lemma Int63_canonic : forall x y, phi x = phi y -> x = y.
-Proof.
- intros x y EQ.
- now rewrite <- (phi_inv_phi x), <- (phi_inv_phi y), EQ.
-Qed.
-
-Lemma ring_theory_switch_eq :
- forall A (R R':A->A->Prop) zero one add mul sub opp,
-  (forall x y : A, R x y -> R' x y) ->
-  ring_theory zero one add mul sub opp R ->
-  ring_theory zero one add mul sub opp R'.
-Proof.
-intros A R R' zero one add mul sub opp Impl Ring.
-constructor; intros; apply Impl; apply Ring.
-Qed.
-
-Lemma Int63Ring : ring_theory 0 1 add63 mul63 sub63 opp63 Logic.eq.
-Proof.
-exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int63_canonic Int63ring.CyclicRing).
-Qed.
-
-Lemma eqb63_eq : forall x y, eqb63 x y = true <-> x=y.
-Proof.
-unfold eqb63. intros x y.
-rewrite Cyclic63.spec_compare. case Z.compare_spec.
-intuition. apply Int63_canonic; auto.
-intuition; subst; auto with zarith; try discriminate.
-intuition; subst; auto with zarith; try discriminate.
-Qed.
-
-Lemma eqb63_correct : forall x y, eqb63 x y = true -> x=y.
-Proof. now apply eqb63_eq. Qed.
-
-Add Ring Int63Ring : Int63Ring
- (decidable eqb63_correct,
-  constants [Int63cst]).
-
-Section TestRing.
-Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x.
-intros. ring.
-Qed.
-
-Let test2 : forall x, (x - 1) + 1 = x.
-intros. ring.
-Qed.
-End TestRing.
-
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 46faa49..3834ee0 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -49,9 +49,6 @@ CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
 versions/standard/Int63/Int63.v
-versions/standard/Int63/Int63Lib.v
-versions/standard/Int63/Cyclic63.v
-versions/standard/Int63/Ring63.v
 versions/standard/Int63/Int63Native.v
 versions/standard/Int63/Int63Op.v
 versions/standard/Int63/Int63Axioms.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 21c0d54..43946bf 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -169,9 +169,6 @@ endif
 ######################
 
 VFILES:=versions/standard/Int63/Int63.v\
-  versions/standard/Int63/Int63Lib.v\
-  versions/standard/Int63/Cyclic63.v\
-  versions/standard/Int63/Ring63.v\
   versions/standard/Int63/Int63Native.v\
   versions/standard/Int63/Int63Op.v\
   versions/standard/Int63/Int63Axioms.v\