From 7f028d564bc00b46e0d836b81246ad8b64d5ead1 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 28 Sep 2016 11:17:44 +0200 Subject: Use the Int31 library with coq-8.5 --- src/versions/standard/Int63/Cyclic63_standard.v | 2522 ----------------------- src/versions/standard/Int63/Int63Lib_standard.v | 487 ----- src/versions/standard/Int63/Int63_standard.v | 1 - src/versions/standard/Int63/Ring63_standard.v | 125 -- src/versions/standard/Make | 3 - src/versions/standard/Makefile | 3 - 6 files changed, 3141 deletions(-) delete mode 100644 src/versions/standard/Int63/Cyclic63_standard.v delete mode 100644 src/versions/standard/Int63/Int63Lib_standard.v delete mode 100644 src/versions/standard/Int63/Ring63_standard.v (limited to 'src/versions') 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|] [|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\ -- cgit