diff options
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 432 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 73 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 221 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2541 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 495 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 104 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 967 |
7 files changed, 4833 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v new file mode 100644 index 0000000000..9f718cba65 --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -0,0 +1,432 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(** * Signature and specification of a bounded integer structure *) + +(** This file specifies how to represent [Z/nZ] when [n=2^d], + [d] being the number of digits of these bounded integers. *) + +Set Implicit Arguments. + +Require Import ZArith. +Require Import Znumtheory. +Require Import Zpow_facts. +Require Import DoubleType. + +Local Open Scope Z_scope. + +(** First, a description via an operator record and a spec record. *) + +Module ZnZ. + + #[universes(template)] + Class Ops (t:Type) := MkOps { + + (* Conversion functions with Z *) + digits : positive; + zdigits: t; + to_Z : t -> Z; + of_pos : positive -> N * t; (* Euclidean division by [2^digits] *) + head0 : t -> t; (* number of digits 0 in front of the number *) + tail0 : t -> t; (* number of digits 0 at the bottom of the number *) + + (* Basic numbers *) + zero : t; + one : t; + minus_one : t; (* [2^digits-1], which is equivalent to [-1] *) + + (* Comparison *) + compare : t -> t -> comparison; + eq0 : t -> bool; + + (* Basic arithmetic operations *) + opp_c : t -> carry t; + opp : t -> t; + opp_carry : t -> t; (* the carry is known to be -1 *) + + succ_c : t -> carry t; + add_c : t -> t -> carry t; + add_carry_c : t -> t -> carry t; + succ : t -> t; + add : t -> t -> t; + add_carry : t -> t -> t; + + pred_c : t -> carry t; + sub_c : t -> t -> carry t; + sub_carry_c : t -> t -> carry t; + pred : t -> t; + sub : t -> t -> t; + sub_carry : t -> t -> t; + + mul_c : t -> t -> zn2z t; + mul : t -> t -> t; + square_c : t -> zn2z t; + + (* Special divisions operations *) + div21 : t -> t -> t -> t*t; + div_gt : t -> t -> t * t; (* specialized version of [div] *) + div : t -> t -> t * t; + + modulo_gt : t -> t -> t; (* specialized version of [mod] *) + modulo : t -> t -> t; + + gcd_gt : t -> t -> t; (* specialized version of [gcd] *) + gcd : t -> t -> t; + (* [add_mul_div p i j] is a combination of the [(digits-p)] + low bits of [i] above the [p] high bits of [j]: + [add_mul_div p i j = i*2^p+j/2^(digits-p)] *) + add_mul_div : t -> t -> t -> t; + (* [pos_mod p i] is [i mod 2^p] *) + pos_mod : t -> t -> t; + + is_even : t -> bool; + (* square root *) + sqrt2 : t -> t -> t * carry t; + sqrt : t -> t; + (* bitwise operations *) + lor : t -> t -> t; + land : t -> t -> t; + lxor : t -> t -> t }. + + Section Specs. + Context {t : Type}{ops : Ops t}. + + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). + + Let wB := base digits. + + Notation "[+| c |]" := + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). + + Notation "[-| c |]" := + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). + + Notation "[|| x ||]" := + (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). + + Class Specs := MkSpecs { + + (* Conversion functions with Z *) + spec_to_Z : forall x, 0 <= [| x |] < wB; + spec_of_pos : forall p, + Zpos p = (Z.of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]; + spec_zdigits : [| zdigits |] = Zpos digits; + spec_more_than_1_digit: 1 < Zpos digits; + + (* Basic numbers *) + spec_0 : [|zero|] = 0; + spec_1 : [|one|] = 1; + spec_m1 : [|minus_one|] = wB - 1; + + (* Comparison *) + spec_compare : forall x y, compare x y = ([|x|] ?= [|y|]); + (* NB: the spec of [eq0] is deliberately partial, + see DoubleCyclic where [eq0 x = true <-> x = W0] *) + spec_eq0 : forall x, eq0 x = true -> [|x|] = 0; + (* Basic arithmetic operations *) + spec_opp_c : forall x, [-|opp_c x|] = -[|x|]; + spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB; + spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1; + + spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1; + spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]; + spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1; + spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB; + spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB; + spec_add_carry : + forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB; + + spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1; + spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]; + spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1; + spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB; + spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB; + spec_sub_carry : + forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB; + + spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|]; + spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB; + spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|]; + + (* Special divisions operations *) + spec_div21 : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := div21 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + let (q,r) := div_gt a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + spec_div : forall a b, 0 < [|b|] -> + let (q,r) := div a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + + spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + [|modulo_gt a b|] = [|a|] mod [|b|]; + spec_modulo : forall a b, 0 < [|b|] -> + [|modulo a b|] = [|a|] mod [|b|]; + + spec_gcd_gt : forall a b, [|a|] > [|b|] -> + Zis_gcd [|a|] [|b|] [|gcd_gt a b|]; + spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]; + + + (* shift operations *) + spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits; + spec_head0 : forall x, 0 < [|x|] -> + wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB; + spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits; + spec_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]) ; + spec_add_mul_div : forall x y p, + [|p|] <= Zpos digits -> + [| add_mul_div p x y |] = + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB; + spec_pos_mod : forall w p, + [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]); + (* sqrt *) + spec_is_even : forall x, + if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1; + spec_sqrt2 : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := sqrt2 x y in + [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]; + spec_sqrt : forall x, + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2; + spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|]; + spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|]; + spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|] + }. + + End Specs. + + Arguments Specs {t} ops. + + (** Generic construction of double words *) + + Section WW. + + Context {t : Type}{ops : Ops t}{specs : Specs ops}. + + Let wB := base digits. + + Definition WO' (eq0:t->bool) zero h := + if eq0 h then W0 else WW h zero. + + Definition WO := Eval lazy beta delta [WO'] in + let eq0 := ZnZ.eq0 in + let zero := ZnZ.zero in + WO' eq0 zero. + + Definition OW' (eq0:t->bool) zero l := + if eq0 l then W0 else WW zero l. + + Definition OW := Eval lazy beta delta [OW'] in + let eq0 := ZnZ.eq0 in + let zero := ZnZ.zero in + OW' eq0 zero. + + Definition WW' (eq0:t->bool) zero h l := + if eq0 h then OW' eq0 zero l else WW h l. + + Definition WW := Eval lazy beta delta [WW' OW'] in + let eq0 := ZnZ.eq0 in + let zero := ZnZ.zero in + WW' eq0 zero. + + Lemma spec_WO : forall h, + zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB. + Proof. + unfold zn2z_to_Z, WO; simpl; intros. + case_eq (eq0 h); intros. + rewrite (spec_eq0 _ H); auto. + rewrite spec_0; auto with zarith. + Qed. + + Lemma spec_OW : forall l, + zn2z_to_Z wB to_Z (OW l) = to_Z l. + Proof. + unfold zn2z_to_Z, OW; simpl; intros. + case_eq (eq0 l); intros. + rewrite (spec_eq0 _ H); auto. + rewrite spec_0; auto with zarith. + Qed. + + Lemma spec_WW : forall h l, + zn2z_to_Z wB to_Z (WW h l) = (to_Z h)*wB + to_Z l. + Proof. + unfold WW; simpl; intros. + case_eq (eq0 h); intros. + rewrite (spec_eq0 _ H); auto. + fold (OW l). + rewrite spec_OW; auto. + simpl; auto. + Qed. + + End WW. + + (** Injecting [Z] numbers into a cyclic structure *) + + Section Of_Z. + + Context {t : Type}{ops : Ops t}{specs : Specs ops}. + + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). + + Theorem of_pos_correct: + forall p, Zpos p < base digits -> [|(snd (of_pos p))|] = Zpos p. + Proof. + intros p Hp. + generalize (spec_of_pos p). + case (of_pos p); intros n w1; simpl. + case n; auto with zarith. + intros p1 Hp1; contradict Hp; apply Z.le_ngt. + replace (base digits) with (1 * base digits + 0) by ring. + rewrite Hp1. + apply Z.add_le_mono. + apply Z.mul_le_mono_nonneg; auto with zarith. + case p1; simpl; intros; red; simpl; intros; discriminate. + unfold base; auto with zarith. + case (spec_to_Z w1); auto with zarith. + Qed. + + Definition of_Z z := + match z with + | Zpos p => snd (of_pos p) + | _ => zero + end. + + Theorem of_Z_correct: + forall p, 0 <= p < base digits -> [|of_Z p|] = p. + Proof. + intros p; case p; simpl; try rewrite spec_0; auto. + intros; rewrite of_pos_correct; auto with zarith. + intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto. + Qed. + + End Of_Z. + +End ZnZ. + +(** A modular specification grouping the earlier records. *) + +Module Type CyclicType. + Parameter t : Type. + Declare Instance ops : ZnZ.Ops t. + Declare Instance specs : ZnZ.Specs ops. +End CyclicType. + + +(** A Cyclic structure can be seen as a ring *) + +Module CyclicRing (Import Cyclic : CyclicType). + +Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). + +Definition eq (n m : t) := [| n |] = [| m |]. + +Local Infix "==" := eq (at level 70). +Local Notation "0" := ZnZ.zero. +Local Notation "1" := ZnZ.one. +Local Infix "+" := ZnZ.add. +Local Infix "-" := ZnZ.sub. +Local Notation "- x" := (ZnZ.opp x). +Local Infix "*" := ZnZ.mul. +Local Notation wB := (base ZnZ.digits). + +Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul + ZnZ.spec_opp ZnZ.spec_sub + : cyclic. + +Ltac zify := unfold eq in *; autorewrite with cyclic. + +Lemma add_0_l : forall x, 0 + x == x. +Proof. +intros. zify. rewrite Z.add_0_l. +apply Zmod_small. apply ZnZ.spec_to_Z. +Qed. + +Lemma add_comm : forall x y, x + y == y + x. +Proof. +intros. zify. now rewrite Z.add_comm. +Qed. + +Lemma add_assoc : forall x y z, x + (y + z) == x + y + z. +Proof. +intros. zify. now rewrite Zplus_mod_idemp_r, Zplus_mod_idemp_l, Z.add_assoc. +Qed. + +Lemma mul_1_l : forall x, 1 * x == x. +Proof. +intros. zify. rewrite Z.mul_1_l. +apply Zmod_small. apply ZnZ.spec_to_Z. +Qed. + +Lemma mul_comm : forall x y, x * y == y * x. +Proof. +intros. zify. now rewrite Z.mul_comm. +Qed. + +Lemma mul_assoc : forall x y z, x * (y * z) == x * y * z. +Proof. +intros. zify. now rewrite Zmult_mod_idemp_r, Zmult_mod_idemp_l, Z.mul_assoc. +Qed. + +Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z. +Proof. +intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Z.mul_add_distr_r. +Qed. + +Lemma add_opp_r : forall x y, x + - y == x-y. +Proof. +intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Z.sub. +destruct (Z.eq_dec ([|y|] mod wB) 0) as [EQ|NEQ]. +rewrite Z_mod_zero_opp_full, EQ, 2 Z.add_0_r; auto. +rewrite Z_mod_nz_opp_full by auto. +rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l. +rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r. +Qed. + +Lemma add_opp_diag_r : forall x, x + - x == 0. +Proof. +intros. red. rewrite add_opp_r. zify. now rewrite Z.sub_diag, Zmod_0_l. +Qed. + +Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq. +Proof. +constructor. +exact add_0_l. exact add_comm. exact add_assoc. +exact mul_1_l. exact mul_comm. exact mul_assoc. +exact mul_add_distr_r. +symmetry. apply add_opp_r. +exact add_opp_diag_r. +Qed. + +Definition eqb x y := + match ZnZ.compare x y with Eq => true | _ => false end. + +Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. +Proof. + intros. unfold eqb, eq. + rewrite ZnZ.spec_compare. + case Z.compare_spec; intuition; try discriminate. +Qed. + +Lemma eqb_correct : forall x y, eqb x y = true -> x==y. +Proof. now apply eqb_eq. Qed. + +End CyclicRing. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v new file mode 100644 index 0000000000..b6441bb76a --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +Set Implicit Arguments. + +Require Import ZArith. +Local Open Scope Z_scope. + +Definition base digits := Z.pow 2 (Zpos digits). +Arguments base digits: simpl never. + +Section Carry. + + Variable A : Type. + + #[universes(template)] + Inductive carry := + | C0 : A -> carry + | C1 : A -> carry. + + Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c := + match c with + | C0 x => interp x + | C1 x => sign*B + interp x + end. + +End Carry. + +Section Zn2Z. + + Variable znz : Type. + + (** From a type [znz] representing a cyclic structure Z/nZ, + we produce a representation of Z/2nZ by pairs of elements of [znz] + (plus a special case for zero). High half of the new number comes + first. + *) + + #[universes(template)] + Inductive zn2z := + | W0 : zn2z + | WW : znz -> znz -> zn2z. + + Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) := + match x with + | W0 => 0 + | WW xh xl => w_to_Z xh * wB + w_to_Z xl + end. + +End Zn2Z. + +Arguments W0 {znz}. + +(** From a cyclic representation [w], we iterate the [zn2z] construct + [n] times, gaining the type of binary trees of depth at most [n], + whose leafs are either W0 (if depth < n) or elements of w + (if depth = n). +*) + +Fixpoint word (w:Type) (n:nat) : Type := + match n with + | O => w + | S n => zn2z (word w n) + end. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v new file mode 100644 index 0000000000..64935ffe1a --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -0,0 +1,221 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +Require Export NZAxioms. +Require Import ZArith. +Require Import Zpow_facts. +Require Import DoubleType. +Require Import CyclicAxioms. + +(** * From [CyclicType] to [NZAxiomsSig] *) + +(** A [Z/nZ] representation given by a module type [CyclicType] + implements [NZAxiomsSig], e.g. the common properties between + N and Z with no ordering. Notice that the [n] in [Z/nZ] is + a power of 2. +*) + +Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig. + +Local Open Scope Z_scope. + +Local Notation wB := (base ZnZ.digits). + +Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). + +Definition eq (n m : t) := [| n |] = [| m |]. +Definition zero := ZnZ.zero. +Definition one := ZnZ.one. +Definition two := ZnZ.succ ZnZ.one. +Definition succ := ZnZ.succ. +Definition pred := ZnZ.pred. +Definition add := ZnZ.add. +Definition sub := ZnZ.sub. +Definition mul := ZnZ.mul. + +Local Infix "==" := eq (at level 70). +Local Notation "0" := zero. +Local Notation S := succ. +Local Notation P := pred. +Local Infix "+" := add. +Local Infix "-" := sub. +Local Infix "*" := mul. + +Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred + ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. +Ltac zify := + unfold eq, zero, one, two, succ, pred, add, sub, mul in *; + autorewrite with cyclic. +Ltac zcongruence := repeat red; intros; zify; congruence. + +Instance eq_equiv : Equivalence eq. +Proof. +unfold eq. firstorder. +Qed. + +Local Obligation Tactic := zcongruence. + +Program Instance succ_wd : Proper (eq ==> eq) succ. +Program Instance pred_wd : Proper (eq ==> eq) pred. +Program Instance add_wd : Proper (eq ==> eq ==> eq) add. +Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. + +Theorem gt_wB_1 : 1 < wB. +Proof. +unfold base. apply Zpower_gt_1; unfold Z.lt; auto with zarith. +Qed. + +Theorem gt_wB_0 : 0 < wB. +Proof. +pose proof gt_wB_1; auto with zarith. +Qed. + +Lemma one_mod_wB : 1 mod wB = 1. +Proof. +rewrite Zmod_small. reflexivity. split. auto with zarith. apply gt_wB_1. +Qed. + +Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB. +Proof. +intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod. +Qed. + +Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB. +Proof. +intro n. rewrite <- one_mod_wB at 2. now rewrite Zminus_mod. +Qed. + +Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |]. +Proof. +intro n; rewrite Zmod_small. reflexivity. apply ZnZ.spec_to_Z. +Qed. + +Theorem pred_succ : forall n, P (S n) == n. +Proof. +intro n. zify. +rewrite <- pred_mod_wB. +replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod. +Qed. + +Theorem one_succ : one == succ zero. +Proof. +zify; simpl Z.add. now rewrite one_mod_wB. +Qed. + +Theorem two_succ : two == succ one. +Proof. +reflexivity. +Qed. + +Section Induction. + +Variable A : t -> Prop. +Hypothesis A_wd : Proper (eq ==> iff) A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n, A n <-> A (S n). + (* Below, we use only -> direction *) + +Let B (n : Z) := A (ZnZ.of_Z n). + +Lemma B0 : B 0. +Proof. +unfold B. apply A0. +Qed. + +Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). +Proof. +intros n H1 H2 H3. +unfold B in *. apply AS in H3. +setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption. +zify. +rewrite 2 ZnZ.of_Z_correct; auto with zarith. +symmetry; apply Zmod_small; auto with zarith. +Qed. + +Theorem Zbounded_induction : + (forall Q : Z -> Prop, forall b : Z, + Q 0 -> + (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) -> + forall n, 0 <= n -> n < b -> Q n)%Z. +Proof. +intros Q b Q0 QS. +set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)). +assert (H : forall n, 0 <= n -> Q' n). +apply natlike_rec2; unfold Q'. +destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split. +intros n H IH. destruct IH as [[IH1 IH2] | IH]. +destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1]. +right; auto with zarith. +left. split; [auto with zarith | now apply (QS n)]. +right; auto with zarith. +unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. +assumption. now apply Z.le_ngt in H3. +Qed. + +Lemma B_holds : forall n : Z, 0 <= n < wB -> B n. +Proof. +intros n [H1 H2]. +apply Zbounded_induction with wB. +apply B0. apply BS. assumption. assumption. +Qed. + +Theorem bi_induction : forall n, A n. +Proof. +intro n. setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)). +apply B_holds. apply ZnZ.spec_to_Z. +red. symmetry. apply ZnZ.of_Z_correct. +apply ZnZ.spec_to_Z. +Qed. + +End Induction. + +Theorem add_0_l : forall n, 0 + n == n. +Proof. +intro n. zify. +rewrite Z.add_0_l. apply Zmod_small. apply ZnZ.spec_to_Z. +Qed. + +Theorem add_succ_l : forall n m, (S n) + m == S (n + m). +Proof. +intros n m. zify. +rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. +rewrite <- (Z.add_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. +rewrite (Z.add_comm 1 [| m |]); now rewrite Z.add_assoc. +Qed. + +Theorem sub_0_r : forall n, n - 0 == n. +Proof. +intro n. zify. rewrite Z.sub_0_r. apply NZ_to_Z_mod. +Qed. + +Theorem sub_succ_r : forall n m, n - (S m) == P (n - m). +Proof. +intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. +now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z + by ring. +Qed. + +Theorem mul_0_l : forall n, 0 * n == 0. +Proof. +intro n. now zify. +Qed. + +Theorem mul_succ_l : forall n m, (S n) * m == n * m + m. +Proof. +intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. +now rewrite Z.mul_add_distr_r, Z.mul_1_l. +Qed. + +Definition t := t. + +End NZCyclicAxiomsMod. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v new file mode 100644 index 0000000000..4a1f24b95e --- /dev/null +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -0,0 +1,2541 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *) + +(** +Author: Arnaud Spiwack (+ Pierre Letouzey) +*) + +Require Import List. +Require Import Min. +Require Export Int31. +Require Import Znumtheory. +Require Import Zgcd_alt. +Require Import Zpow_facts. +Require Import CyclicAxioms. +Require Import Lia. + +Local Open Scope nat_scope. +Local Open Scope int31_scope. + +Local Hint Resolve Z.lt_gt Z.div_pos : zarith. + +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 [int31] *) + + (** Not used for the moment. Are they really useful ? *) + + Lemma int31_ind_sneakl : forall P : int31->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 int31_ind_twice : forall P : int31->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 int31_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->int31->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->int31->A->A) + (i:int31) : 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; auto. + replace (recrbis_aux n A case0 caserec 0) with case0; auto. + clear H IHn; induction n; simpl; 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 : int31) := + 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 (_:int31) => + 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^31] *) + + 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_nonneg : forall x, (0 <= phi x)%Z. + Proof. + intros. + rewrite <- phibis_aux_equiv. + apply phibis_aux_pos. + Qed. + + Hint Resolve phi_nonneg : zarith. + + Lemma phi_bounded : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z. + Proof. + intros. split; [auto with zarith|]. + rewrite <- phibis_aux_equiv. + 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 int31 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 int31 to Z and then back to int31. *) + + 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_in31]. *) + + (** * [positive_to_int31] *) + + (** A variant of [p2i] with [twice] and [twice_plus_one] instead of + [2*i] and [2*i+1] *) + + Fixpoint p2ibis n p : (N*int31)%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_int31]. *) + + Lemma double_twice_firstl : forall x, firstl x = D0 -> + (Twon*x = twice x)%int31. + Proof. + intros. + unfold mul31. + 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)%int31. + Proof. + intros. + rewrite double_twice_firstl; auto. + unfold add31. + 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_int31_phi_inv_positive : forall p, + snd (positive_to_int31 p) = phi_inv_positive p. + Proof. + intros; unfold positive_to_int31. + rewrite p2i_p2ibis; auto. + symmetry. + rewrite <- EqShiftL_zero. + apply (phi_inv_positive_p2ibis size); auto. + Qed. + + Lemma positive_to_int31_spec : forall p, + Zpos p = (Z.of_N (fst (positive_to_int31 p)))*2^(Z.of_nat size) + + phi (snd (positive_to_int31 p)). + Proof. + unfold positive_to_int31. + 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. + +Instance int31_ops : ZnZ.Ops int31 := +{ + digits := 31%positive; (* number of digits *) + zdigits := 31; (* number of digits *) + to_Z := phi; (* conversion to Z *) + of_pos := positive_to_int31; (* positive -> N*int31 : p => N,i + where p = N*2^31+phi i *) + head0 := head031; (* number of head 0 *) + tail0 := tail031; (* number of tail 0 *) + zero := 0; + one := 1; + minus_one := Tn; (* 2^31 - 1 *) + compare := compare31; + eq0 := fun i => match i ?= 0 with Eq => true | _ => false end; + opp_c := fun i => 0 -c i; + opp := opp31; + opp_carry := fun i => 0-i-1; + succ_c := fun i => i +c 1; + add_c := add31c; + add_carry_c := add31carryc; + succ := fun i => i + 1; + add := add31; + add_carry := fun i j => i + j + 1; + pred_c := fun i => i -c 1; + sub_c := sub31c; + sub_carry_c := sub31carryc; + pred := fun i => i - 1; + sub := sub31; + sub_carry := fun i j => i - j - 1; + mul_c := mul31c; + mul := mul31; + square_c := fun x => x *c x; + div21 := div3121; + div_gt := div31; (* this is supposed to be the special case of + division a/b where a > b *) + div := div31; + modulo_gt := fun i j => let (_,r) := i/j in r; + modulo := fun i j => let (_,r) := i/j in r; + gcd_gt := gcd31; + gcd := gcd31; + add_mul_div := addmuldiv31; + pos_mod := (* modulo 2^p *) + fun p i => + match p ?= 31 with + | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) + | _ => i + end; + is_even := + fun i => let (_,r) := i/2 in + match r ?= 0 with Eq => true | _ => false end; + sqrt2 := sqrt312; + sqrt := sqrt31; + lor := lor31; + land := land31; + lxor := lxor31 +}. + +Section Int31_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 : [| 31 |] = 31. + Proof. + reflexivity. + Qed. + + Lemma spec_more_than_1_digit: 1 < 31. + 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)%int31 = ([|x|] ?= [|y|]). + Proof. reflexivity. Qed. + + (** Addition *) + + Lemma spec_add_c : forall x y, [+|add31c x y|] = [|x|] + [|y|]. + Proof. + intros; unfold add31c, add31, 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; lia. + + 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, [+|add31c x 1|] = [|x|] + 1. + Proof. + intros; apply spec_add_c. + Qed. + + Lemma spec_add_carry_c : forall x y, [+|add31carryc x y|] = [|x|] + [|y|] + 1. + Proof. + intros. + unfold add31carryc, 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; lia. + + 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 add31; 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, [-|sub31c x y|] = [|x|] - [|y|]. + Proof. + unfold sub31c, sub31, 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; lia. + contradict H1; apply Zmod_small; lia. + + 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, [-|sub31carryc x y|] = [|x|] - [|y|] - 1. + Proof. + unfold sub31carryc, sub31, 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; lia. + contradict H1; apply Zmod_small; lia. + + 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 sub31; intros. + repeat rewrite phi_phi_inv. + apply Zminus_mod_idemp_l. + Qed. + + Lemma spec_opp_c : forall x, [-|sub31c 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 sub31; 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); lia. + Qed. + + Lemma spec_pred_c : forall x, [-|sub31c 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, [|| mul31c x y ||] = [|x|] * [|y|]. + Proof. + unfold mul31c; 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, [|| mul31c 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) := div3121 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + unfold div3121; 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 31) with wB; change (Z.pow_pos 2 31) 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) := div31 a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + unfold div31; 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)%int31 in r|] = [|a|] mod [|b|]. + Proof. + unfold div31; 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, + [|gcd31 i j|] = Zgcdn (2*size) [|j|] [|i|]. + Proof. + unfold gcd31. + induction (2*size)%nat; intros. + reflexivity. + simpl euler. + unfold compare31. + 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|] [|gcd31 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_int31_iter_nat : forall A f i a, + iter_int31 i A f a = iter_nat (Z.abs_nat [|i|]) A f a. + Proof. + intros. + unfold iter_int31. + 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 addmuldiv31_alt n i j := + match n with + | O => i + | S n => addmuldiv31_alt n (sneakl (firstl j) i) (shiftl j) + end. + + Lemma addmuldiv31_equiv : forall p x y, + addmuldiv31 p x y = addmuldiv31_alt (Z.abs_nat [|p|]) x y. + Proof. + intros. + unfold addmuldiv31. + rewrite iter_int31_iter_nat. + set (n:=Z.abs_nat [|p|]); clearbody n; clear p. + revert x y; induction n. + simpl; auto. + intros. + simpl addmuldiv31_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 31 -> + [| addmuldiv31 p x y |] = + ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB. + Proof. + intros. + rewrite addmuldiv31_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 <= 31)%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^(31-0)) with 0. + rewrite Z.add_0_r. + symmetry; apply Zmod_small; apply phi_bounded. + symmetry; apply Zdiv_small; apply phi_bounded. + + simpl addmuldiv31_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 (31-Z.of_nat n) with (Z.succ(31-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^(31-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 (31+-Z.of_nat n) with (Z.succ(31-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 shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> + ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = + a mod 2 ^ p. + Proof. + intros. + rewrite Zmod_small. + rewrite Zmod_eq by (auto with zarith). + unfold Z.sub at 1. + rewrite Z_div_plus_full_l + by (cut (0 < 2^(n-p)); auto with zarith). + assert (2^n = 2^(n-p)*2^p). + rewrite <- Zpower_exp by (auto with zarith). + replace (n-p+p) with n; auto with zarith. + rewrite H0. + rewrite <- Zdiv_Zdiv, Z_div_mult by (auto with zarith). + rewrite (Z.mul_comm (2^(n-p))), Z.mul_assoc. + rewrite <- Z.mul_opp_l. + rewrite Z_div_mult by (auto with zarith). + symmetry; apply Zmod_eq; auto with zarith. + + remember (a * 2 ^ (n - p)) as b. + destruct (Z_mod_lt b (2^n)); auto with zarith. + split. + apply Z_div_pos; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + apply Z.lt_le_trans with (2^n); auto with zarith. + rewrite <- (Z.mul_1_r (2^n)) at 1. + apply Z.mul_le_mono_nonneg; auto with zarith. + cut (0 < 2 ^ (n-p)); auto with zarith. + Qed. + + Lemma spec_pos_mod : forall w p, + [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]). + Proof. + unfold int31_ops, ZnZ.pos_mod, compare31. + change [|31|] with 31%Z. + assert (forall w p, 31<=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|] ?= 31); intros; + [ apply H; rewrite (Z.compare_eq _ _ H0); auto with zarith | | + apply H; change ([|p|]>31)%Z in H0; auto with zarith ]. + change ([|p|]<31) 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 (31-[|p|]<wB). + apply Z.le_lt_trans with 31%Z; auto with zarith. + compute; auto. + assert ([|31-p|]=31-[|p|]). + unfold sub31; rewrite phi_phi_inv. + change [|31|] with 31%Z. + apply Zmod_small; auto with zarith. + rewrite spec_add_mul_div by (rewrite H4; auto with zarith). + change [|0|] with 0%Z; rewrite Zdiv_0_l, Z.add_0_r. + rewrite H4. + apply shift_unshift_mod_2; simpl; auto with zarith. + Qed. + + + (** Shift operations *) + + Lemma spec_head00: forall x, [|x|] = 0 -> [|head031 x|] = Zpos 31. + Proof. + intros. + generalize (phi_inv_phi x). + rewrite H; simpl phi_inv. + intros H'; rewrite <- H'. + simpl; auto. + Qed. + + Fixpoint head031_alt n x := + match n with + | O => 0%nat + | S n => match firstl x with + | D0 => S (head031_alt n (shiftl x)) + | D1 => 0%nat + end + end. + + Lemma head031_equiv : + forall x, [|head031 x|] = Z.of_nat (head031_alt size x). + Proof. + intros. + case_eq (iszero x); intros. + rewrite (iszero_eq0 _ H). + simpl; auto. + + unfold head031, recl. + change On with (phi_inv (Z.of_nat (31-size))). + replace (head031_alt size x) with + (head031_alt size x + (31 - size))%nat by auto. + assert (size <= 31)%nat by auto with arith. + + revert x H; induction size; intros. + simpl; auto. + unfold recl_aux; fold recl_aux. + unfold head031_alt; fold head031_alt. + rewrite H. + assert ([|phi_inv (Z.of_nat (31-S n))|] = Z.of_nat (31 - 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 31). + apply inj_le; omega. + compute; auto. + case_eq (firstl x); intros; auto. + rewrite plus_Sn_m, plus_n_Sm. + replace (S (31 - S n)) with (31 - n)%nat by omega. + rewrite <- IHn; [ | omega | ]. + f_equal; f_equal. + unfold add31. + rewrite H1. + f_equal. + change [|In|] with 1. + replace (31-n)%nat with (S (31 - 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%int31. + 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 ^ ([|head031 x|]) * [|x|] < wB. + Proof. + intros. + rewrite head031_equiv. + assert (nshiftl x size = 0%int31). + 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 head031_alt. + case_eq (firstl x); intros. + rewrite (Nat2Z.inj_succ (head031_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 31)/2) with (2^(Z.of_nat (pred size))). + apply phi_lowerbound; auto. + Qed. + + Lemma spec_tail00: forall x, [|x|] = 0 -> [|tail031 x|] = Zpos 31. + Proof. + intros. + generalize (phi_inv_phi x). + rewrite H; simpl phi_inv. + intros H'; rewrite <- H'. + simpl; auto. + Qed. + + Fixpoint tail031_alt n x := + match n with + | O => 0%nat + | S n => match firstr x with + | D0 => S (tail031_alt n (shiftr x)) + | D1 => 0%nat + end + end. + + Lemma tail031_equiv : + forall x, [|tail031 x|] = Z.of_nat (tail031_alt size x). + Proof. + intros. + case_eq (iszero x); intros. + rewrite (iszero_eq0 _ H). + simpl; auto. + + unfold tail031, recr. + change On with (phi_inv (Z.of_nat (31-size))). + replace (tail031_alt size x) with + (tail031_alt size x + (31 - size))%nat by auto. + assert (size <= 31)%nat by auto with arith. + + revert x H; induction size; intros. + simpl; auto. + unfold recr_aux; fold recr_aux. + unfold tail031_alt; fold tail031_alt. + rewrite H. + assert ([|phi_inv (Z.of_nat (31-S n))|] = Z.of_nat (31 - 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 31). + apply inj_le; omega. + compute; auto. + case_eq (firstr x); intros; auto. + rewrite plus_Sn_m, plus_n_Sm. + replace (S (31 - S n)) with (31 - n)%nat by omega. + rewrite <- IHn; [ | omega | ]. + f_equal; f_equal. + unfold add31. + rewrite H1. + f_equal. + change [|In|] with 1. + replace (31-n)%nat with (S (31 - 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 ^ [|tail031 x|]). + Proof. + intros. + rewrite tail031_equiv. + assert (nshiftr x size = 0%int31). + apply nshiftr_size. + revert x H H0. + induction size. + simpl Z.of_nat. + intros. + compute in H0; rewrite H0 in H; discriminate. + + intros. + simpl tail031_alt. + case_eq (firstr x); intros. + rewrite (Nat2Z.inj_succ (tail031_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 sqrt31_step_def rec i j: + sqrt31_step rec i j = + match (fst (i/j) ?= j)%int31 with + Lt => rec i (fst ((j + fst(i/j))/2))%int31 + | _ => j + end. + Proof. + unfold sqrt31_step; case div31; intros. + simpl; case compare31; auto. + Qed. + + Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. + intros Hj; generalize (spec_div i j Hj). + case div31; intros q r; simpl @fst. + intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. + rewrite H1; ring. + Qed. + + Lemma sqrt31_step_correct rec i j: + 0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 -> + 2 * [|j|] < wB -> + (forall j1 : int31, + 0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 -> + [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> + [|sqrt31_step rec i j|] ^ 2 <= [|i|] < ([|sqrt31_step rec i j|] + 1) ^ 2. + Proof. + assert (Hp2: 0 < [|2|]) by exact (eq_refl Lt). + intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. + rewrite spec_compare, div31_phi; auto. + case Z.compare_spec; auto; intros Hc; + try (split; auto; apply sqrt_test_true; auto with zarith; fail). + assert (E : [|(j + fst (i / j)%int31)|] = [|j|] + [|i|] / [|j|]). + { rewrite spec_add, div31_phi; auto using Z.mod_small with zarith. } + apply Hrec; rewrite !div31_phi, E; auto using sqrt_main with zarith. + split; try apply sqrt_test_false; auto with zarith. + 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|])) by ring. + rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= [|i|]/ [|j|]) by auto with zarith. + assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]); auto with zarith. + - rewrite <- Hj, Zdiv_1_r. + replace (1 + [|i|]) with (1 * 2 + ([|i|] - 1)) by ring. + rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= ([|i|] - 1) /2) by auto with zarith. + change ([|2|]) with 2; auto with zarith. + Qed. + + Lemma iter31_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) -> + [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2. + Proof. + revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_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 H31 HHrec. + apply sqrt31_step_correct; auto. + intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j2 Hj2 H2j2 Hjp2 Hj31; 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, + [|sqrt31 x|] ^ 2 <= [|x|] < ([|sqrt31 x|] + 1) ^ 2. + Proof. + intros i; unfold sqrt31. + 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 iter31_sqrt_correct; auto with zarith. + rewrite div31_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 div31_phi; change ([|2|]) with 2; auto with zarith. + apply sqrt_init; auto. + rewrite div31_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 div31_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 sqrt312_step_def rec ih il j: + sqrt312_step rec ih il j = + match (ih ?= j)%int31 with + Eq => j + | Gt => j + | _ => + match (fst (div3121 ih il j) ?= j)%int31 with + Lt => let m := match j +c fst (div3121 ih il j) with + C0 m1 => fst (m1/2)%int31 + | C1 m1 => (fst (m1/2) + v30)%int31 + end in rec ih il m + | _ => j + end + end. + Proof. + unfold sqrt312_step; case div3121; intros. + simpl; case compare31; auto. + Qed. + + Lemma sqrt312_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); auto with zarith. + apply Z.square_lt_simpl_nonneg; auto with zarith. + rewrite <- ?Z.pow_2_r; apply Z.le_lt_trans with (2 := H1). + apply Z.le_trans with ([|ih|] * wB). + - rewrite ? Z.pow_2_r; auto with zarith. + - unfold phi2. change base with wB; auto with zarith. + Qed. + + Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] -> + [|fst (div3121 ih il j)|] = phi2 ih il/[|j|])%Z. + Proof. + intros Hj Hj1. + generalize (spec_div21 ih il j Hj Hj1). + case div3121; 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 sqrt312_step_correct rec ih il j: + 2 ^ 29 <= [|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) -> + [|sqrt312_step rec ih il j|] ^ 2 <= phi2 ih il + < ([|sqrt312_step rec ih il j|] + 1) ^ 2. + Proof. + assert (Hp2: (0 < [|2|])%Z) by exact (eq_refl Lt). + intros Hih Hj Hij Hrec; rewrite sqrt312_step_def. + assert (H1: ([|ih|] <= [|j|])) by (apply sqrt312_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); 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; auto with zarith. + change base with wB. auto with zarith. + - case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj. + + rewrite spec_compare; case Z.compare_spec; + rewrite div312_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 auto with zarith. + apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj. + Z.le_elim Hj; + [ | 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|]) 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 (div3121 ih il j))). + unfold interp_carry; case add31c; intros r; + rewrite div312_phi; auto with zarith. + { rewrite div31_phi; change [|2|] with 2; auto with zarith. + intros HH; rewrite HH; clear HH; auto with zarith. } + { rewrite spec_add, div31_phi; change [|2|] with 2; 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 _) with (([|j|] + (phi2 ih il)/([|j|]))/2); + [ apply sqrt_main; auto with zarith | ]. + generalize (spec_add_c j (fst (div3121 ih il j))). + unfold interp_carry; case add31c; intros r; + rewrite div312_phi; auto with zarith. + { rewrite div31_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 div31_phi; auto. + - split; auto with zarith. + + case (phi_bounded (fst (r/2)%int31)); + case (phi_bounded v30); auto with zarith. + + rewrite div31_phi; change (phi 2) with 2; 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 ^ 30); auto with zarith. + apply Z.le_trans with ((2 ^ 30) * (2 ^ 30)); auto with zarith. + * assert (0 <= 1 + [|j|]); auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + * change ((2 ^ 30) * (2 ^ 30)) with ((2 ^ 29) * base). + apply Z.le_trans with ([|ih|] * base); + change wB with base in *; 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 iter312_sqrt_correct n rec ih il j: + 2^29 <= [|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) -> + [|iter312_sqrt n rec ih il j|] ^ 2 <= phi2 ih il + < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2. + Proof. + revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_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 sqrt312_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|]); auto with zarith. + apply Nat2Z.is_nonneg. + Qed. + + (* Avoid expanding [iter312_sqrt] before variables in the context. *) + Strategy 1 [iter312_sqrt]. + + Lemma spec_sqrt2 : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := sqrt312 x y in + [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]. + Proof. + intros ih il Hih; unfold sqrt312. + 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^62). + apply Z.le_lt_trans with ((2^31 -1) * base + (2^31 - 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 (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith. + change [|Tn|] with 2147483647; auto with zarith. + intros j1 _ HH; contradict HH. + apply Z.lt_nge. + change [|Tn|] with 2147483647; auto with zarith. + change (2 ^ Z.of_nat 31) with 2147483648; auto with zarith. + case (phi_bounded j1); auto with zarith. + set (s := iter312_sqrt 31 (fun _ _ j : int31 => j) ih il Tn). + intros Hs1 Hs2. + generalize (spec_mul_c s s); case mul31c. + 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 sub31c; 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 536870912. + 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, int31_ops. + unfold compare31; 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, int31_ops; intros. + generalize (spec_div x 2). + destruct (x/2)%int31 as (q,r); intros. + unfold compare31. + 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,int31_ops. unfold lor31. + 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, int31_ops. unfold land31. + 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, int31_ops. unfold lxor31. + 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 int31_specs : ZnZ.Specs int31_ops := { + spec_to_Z := phi_bounded; + spec_of_pos := positive_to_int31_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 Int31_Specs. + + +Module Int31Cyclic <: CyclicType. + Definition t := int31. + Definition ops := int31_ops. + Definition specs := int31_specs. +End Int31Cyclic. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v new file mode 100644 index 0000000000..ce540775e3 --- /dev/null +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -0,0 +1,495 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +Require Import NaryFunctions. +Require Import Wf_nat. +Require Export ZArith. +Require Export DoubleType. + +Local Unset Elimination Schemes. + +(** * 31-bit integers *) + +(** This file contains basic definitions of a 31-bit integer + arithmetic. In fact it is more general than that. The only reason + for this use of 31 is the underlying mechanism for hardware-efficient + computations by A. Spiwack. Apart from this, a switch to, say, + 63-bit integers is now just a matter of replacing every occurrences + of 31 by 63. This is actually made possible by the use of + dependently-typed n-ary constructions for the inductive type + [int31], its constructor [I31] and any pattern matching on it. + If you modify this file, please preserve this genericity. *) + +Definition size := 31%nat. + +(** Digits *) + +Inductive digits : Type := D0 | D1. + +(** The type of 31-bit integers *) + +(** The type [int31] has a unique constructor [I31] that expects + 31 arguments of type [digits]. *) + +Definition digits31 t := Eval compute in nfun digits size t. + +Inductive int31 : Type := I31 : digits31 int31. + +(* 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). *) +Register digits as int31.bits. +Register int31 as int31.type. + +Scheme int31_ind := Induction for int31 Sort Prop. +Scheme int31_rec := Induction for int31 Sort Set. +Scheme int31_rect := Induction for int31 Sort Type. + +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". +Delimit Scope int31_scope with int31. +Bind Scope int31_scope with int31. +Local Open Scope int31_scope. + +(** * Constants *) + +(** Zero is [I31 D0 ... D0] *) +Definition On : int31 := Eval compute in napply_cst _ _ D0 size I31. + +(** One is [I31 D0 ... D0 D1] *) +Definition In : int31 := Eval compute in (napply_cst _ _ D0 (size-1) I31) D1. + +(** The biggest integer is [I31 D1 ... D1], corresponding to [(2^size)-1] *) +Definition Tn : int31 := Eval compute in napply_cst _ _ D1 size I31. + +(** Two is [I31 D0 ... D0 D1 D0] *) +Definition Twon : int31 := Eval compute in (napply_cst _ _ D0 (size-2) I31) D1 D0. + +(** * 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 (I31 d0 ... dN) => I31 b d0 ... d(N-1) end ] +*) + +Definition sneakr : digits -> int31 -> int31 := Eval compute in + fun b => int31_rect _ (napply_except_last _ _ (size-1) (I31 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 (I31 d0 ... dN) => I31 d1 ... dN b end ] +*) + +Definition sneakl : digits -> int31 -> int31 := Eval compute in + fun b => int31_rect _ (fun _ => napply_then_last _ _ b (size-1) I31). + + +(** [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 (I31 d0 ... dN) => d0 end ] *) + +Definition firstl : int31 -> digits := Eval compute in + int31_rect _ (fun d => napply_discard _ _ d (size-1)). + +(** [firstr x] returns the rightmost digit of number [x]. + Pseudo-code is [ match x with (I31 d0 ... dN) => dN end ] *) + +Definition firstr : int31 -> digits := Eval compute in + int31_rect _ (napply_discard _ _ (fun d=>d) (size-1)). + +(** [iszero x] is true iff [x = I31 D0 ... D0]. Pseudo-code is + [ match x with (I31 D0 ... D0) => true | _ => false end ] *) + +Definition iszero : int31 -> bool := Eval compute in + let f d b := match d with D0 => b | D1 => false end + in int31_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^31], 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->int31->A->A) + (i:int31) : 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->int31->A->A) + (i:int31) : 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 int31 to Z, we simply iterates [Z.double] or [Z.succ_double]. *) + +Definition phi : int31 -> Z := + recr Z (0%Z) + (fun b _ => match b with D0 => Z.double | D1 => Z.succ_double end). + +(** From positive to int31. 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 : int31 -> int31 := + recr int31 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 int31. *) + +Definition phi_inv : Z -> int31 := 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 int31] *) + +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^31] *) + +Definition add31 (n m : int31) := phi_inv ((phi n)+(phi m)). +Notation "n + m" := (add31 n m) : int31_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 add31c (n m : int31) := + let npm := n+m in + match (phi npm ?= (phi n)+(phi m))%Z with + | Eq => C0 npm + | _ => C1 npm + end. +Notation "n '+c' m" := (add31c n m) (at level 50, no associativity) : int31_scope. + +(** Addition plus one with carry (the result is thus exact) *) + +Definition add31carryc (n m : int31) := + 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^31] *) + +Definition sub31 (n m : int31) := phi_inv ((phi n)-(phi m)). +Notation "n - m" := (sub31 n m) : int31_scope. + +(** Subtraction with carry (thus exact) *) + +Definition sub31c (n m : int31) := + let nmm := n-m in + match (phi nmm ?= (phi n)-(phi m))%Z with + | Eq => C0 nmm + | _ => C1 nmm + end. +Notation "n '-c' m" := (sub31c n m) (at level 50, no associativity) : int31_scope. + +(** subtraction minus one with carry (thus exact) *) + +Definition sub31carryc (n m : int31) := + 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 opp31 x := On - x. +Notation "- x" := (opp31 x) : int31_scope. + +(** Multiplication *) + +(** multiplication modulo [2^31] *) + +Definition mul31 (n m : int31) := phi_inv ((phi n)*(phi m)). +Notation "n * m" := (mul31 n m) : int31_scope. + +(** multiplication with double word result (thus exact) *) + +Definition mul31c (n m : int31) := phi_inv2 ((phi n)*(phi m)). +Notation "n '*c' m" := (mul31c n m) (at level 40, no associativity) : int31_scope. + + +(** * Division *) + +(** Division of a double size word modulo [2^31] *) + +Definition div3121 (nh nl m : int31) := + let (q,r) := Z.div_eucl (phi2 nh nl) (phi m) in + (phi_inv q, phi_inv r). + +(** Division modulo [2^31] *) + +Definition div31 (n m : int31) := + let (q,r) := Z.div_eucl (phi n) (phi m) in + (phi_inv q, phi_inv r). +Notation "n / m" := (div31 n m) : int31_scope. + + +(** * Unsigned comparison *) + +Definition compare31 (n m : int31) := ((phi n)?=(phi m))%Z. +Notation "n ?= m" := (compare31 n m) (at level 70, no associativity) : int31_scope. + +Definition eqb31 (n m : int31) := + match n ?= m with Eq => true | _ => false end. + + +(** Computing the [i]-th iterate of a function: + [iter_int31 i A f = f^i] *) + +Definition iter_int31 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 [(31-p)] low bits of [i] above the [p] high bits of [j]: + [addmuldiv31 p i j = i*2^p+j/2^(31-p)] (modulo [2^31]) *) + +Definition addmuldiv31 p i j := + let (res, _ ) := + iter_int31 p (int31*int31) + (fun ij => let (i,j) := ij in (sneakl (firstl j) i, shiftl j)) + (i,j) + in + res. + +(** Bitwise operations *) + +Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). +Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). +Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). + +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. + +Definition lnot31 n := lxor31 Tn n. +Definition ldiff31 n m := land31 n (lnot31 m). + +Fixpoint euler (guard:nat) (i j:int31) {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 gcd31 (i j:int31) := euler (2*size)%nat i j. + +(** Square root functions using newton iteration + we use a very naive upper-bound on the iteration + 2^31 instead of the usual 31. +**) + + + +Definition sqrt31_step (rec: int31 -> int31 -> int31) (i j: int31) := +Eval lazy delta [Twon] in + let (quo,_) := i/j in + match quo ?= j with + Lt => rec i (fst ((j + quo)/Twon)) + | _ => j + end. + +Fixpoint iter31_sqrt (n: nat) (rec: int31 -> int31 -> int31) + (i j: int31) {struct n} : int31 := + sqrt31_step + (match n with + O => rec + | S n => (iter31_sqrt n (iter31_sqrt n rec)) + end) i j. + +Definition sqrt31 i := +Eval lazy delta [On In Twon] in + match compare31 In i with + Gt => On + | Eq => In + | Lt => iter31_sqrt 31 (fun i j => j) i (fst (i/Twon)) + end. + +Definition v30 := Eval compute in (addmuldiv31 (phi_inv (Z.of_nat size - 1)) In On). + +Definition sqrt312_step (rec: int31 -> int31 -> int31 -> int31) + (ih il j: int31) := +Eval lazy delta [Twon v30] in + match ih ?= j with Eq => j | Gt => j | _ => + let (quo,_) := div3121 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 iter312_sqrt (n: nat) + (rec: int31 -> int31 -> int31 -> int31) + (ih il j: int31) {struct n} : int31 := + sqrt312_step + (match n with + O => rec + | S n => (iter312_sqrt n (iter312_sqrt n rec)) + end) ih il j. + +Definition sqrt312 ih il := +Eval lazy delta [On In] in + let s := iter312_sqrt 31 (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*int31)%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_int31 (p:positive) := p2i size p. + +(** Constant 31 converted into type int31. + It is used as default answer for numbers of zeros + in [head0] and [tail0] *) + +Definition T31 : int31 := Eval compute in phi_inv (Z.of_nat size). + +Definition head031 (i:int31) := + recl _ (fun _ => T31) + (fun b si rec n => match b with + | D0 => rec (add31 n In) + | D1 => n + end) + i On. + +Definition tail031 (i:int31) := + recr _ (fun _ => T31) + (fun b si rec n => match b with + | D0 => rec (add31 n In) + | D1 => n + end) + i On. + +Register head031 as int31.head0. +Register tail031 as int31.tail0. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v new file mode 100644 index 0000000000..b693529451 --- /dev/null +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -0,0 +1,104 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped + with a ring structure and a ring tactic *) + +Require Import Int31 Cyclic31 CyclicAxioms. + +Local Open Scope int31_scope. + +(** Detection of constants *) + +Local Open Scope list_scope. + +Ltac isInt31cst_lst l := + match l with + | nil => constr:(true) + | ?t::?l => match t with + | D1 => isInt31cst_lst l + | D0 => isInt31cst_lst l + | _ => constr:(false) + end + | _ => constr:(false) + end. + +Ltac isInt31cst t := + match t with + | I31 ?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 => + 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::nil) + in isInt31cst_lst l + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) + end. + +Ltac Int31cst t := + match isInt31cst t with + | true => constr:(t) + | false => constr:(NotConstant) + end. + +(** The generic ring structure inferred from the Cyclic structure *) + +Module Int31ring := CyclicRing Int31Cyclic. + +(** Unlike in the generic [CyclicRing], we can use Leibniz here. *) + +Lemma Int31_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 Int31Ring : ring_theory 0 1 add31 mul31 sub31 opp31 Logic.eq. +Proof. +exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int31_canonic Int31ring.CyclicRing). +Qed. + +Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y. +Proof. +unfold eqb31. intros x y. +rewrite Cyclic31.spec_compare. case Z.compare_spec. +intuition. apply Int31_canonic; auto. +intuition; subst; auto with zarith; try discriminate. +intuition; subst; auto with zarith; try discriminate. +Qed. + +Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y. +Proof. now apply eqb31_eq. Qed. + +Add Ring Int31Ring : Int31Ring + (decidable eqb31_correct, + constants [Int31cst]). + +Section TestRing. +Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x. +intros. ring. +Qed. +End TestRing. + diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v new file mode 100644 index 0000000000..4bcd22543f --- /dev/null +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -0,0 +1,967 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ] + as defined abstractly in CyclicAxioms. *) + +(** Even if the construction provided here is not reused for building + the efficient arbitrary precision numbers, it provides a simple + implementation of CyclicAxioms, hence ensuring its coherence. *) + +Set Implicit Arguments. + +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import Zpow_facts. +Require Import DoubleType. +Require Import CyclicAxioms. + +Local Open Scope Z_scope. + +Section ZModulo. + + Variable digits : positive. + Hypothesis digits_ne_1 : digits <> 1%positive. + + Definition wB := base digits. + + Definition t := Z. + Definition zdigits := Zpos digits. + Definition to_Z x := x mod wB. + + Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). + + Notation "[+| c |]" := + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). + + Notation "[-| c |]" := + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). + + Notation "[|| x ||]" := + (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). + + Lemma spec_more_than_1_digit: 1 < Zpos digits. + Proof. + generalize digits_ne_1; destruct digits; red; auto. + destruct 1; auto. + Qed. + Let digits_gt_1 := spec_more_than_1_digit. + + Lemma wB_pos : wB > 0. + Proof. + apply Z.lt_gt. + unfold wB, base; auto with zarith. + Qed. + Hint Resolve wB_pos : core. + + Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. + Proof. + unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. + Qed. + + Lemma spec_to_Z_2 : forall x, [|x|] < wB. + Proof. + unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. + Qed. + Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. + + Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. + Proof. + auto. + Qed. + + Definition of_pos x := + let (q,r) := Z.pos_div_eucl x wB in (N_of_Z q, r). + + Lemma spec_of_pos : forall p, + Zpos p = (Z.of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]. + Proof. + intros; unfold of_pos; simpl. + generalize (Z_div_mod_POS wB wB_pos p). + destruct (Z.pos_div_eucl p wB); simpl; destruct 1. + unfold to_Z; rewrite Zmod_small; auto. + assert (0 <= z). + replace z with (Zpos p / wB) by + (symmetry; apply Zdiv_unique with z0; auto). + apply Z_div_pos; auto with zarith. + replace (Z.of_N (N_of_Z z)) with z by + (destruct z; simpl; auto; elim H1; auto). + rewrite Z.mul_comm; auto. + Qed. + + Lemma spec_zdigits : [|zdigits|] = Zpos digits. + Proof. + unfold to_Z, zdigits. + apply Zmod_small. + unfold wB, base. + split; auto with zarith. + apply Zpower2_lt_lin; auto with zarith. + Qed. + + Definition zero := 0. + Definition one := 1. + Definition minus_one := wB - 1. + + Lemma spec_0 : [|zero|] = 0. + Proof. + unfold to_Z, zero. + apply Zmod_small; generalize wB_pos; auto with zarith. + Qed. + + Lemma spec_1 : [|one|] = 1. + Proof. + unfold to_Z, one. + apply Zmod_small; split; auto with zarith. + unfold wB, base. + apply Z.lt_trans with (Zpos digits); auto. + apply Zpower2_lt_lin; auto with zarith. + Qed. + + Lemma spec_Bm1 : [|minus_one|] = wB - 1. + Proof. + unfold to_Z, minus_one. + apply Zmod_small; split; auto with zarith. + unfold wB, base. + cut (1 <= 2 ^ Zpos digits); auto with zarith. + apply Z.le_trans with (Zpos digits); auto with zarith. + apply Zpower2_le_lin; auto with zarith. + Qed. + + Definition compare x y := Z.compare [|x|] [|y|]. + + Lemma spec_compare : forall x y, + compare x y = Z.compare [|x|] [|y|]. + Proof. reflexivity. Qed. + + Definition eq0 x := + match [|x|] with Z0 => true | _ => false end. + + Lemma spec_eq0 : forall x, eq0 x = true -> [|x|] = 0. + Proof. + unfold eq0; intros; now destruct [|x|]. + Qed. + + Definition opp_c x := + if eq0 x then C0 0 else C1 (- x). + Definition opp x := - x. + Definition opp_carry x := - x - 1. + + Lemma spec_opp_c : forall x, [-|opp_c x|] = -[|x|]. + Proof. + intros; unfold opp_c, to_Z; auto. + case_eq (eq0 x); intros; unfold interp_carry. + fold [|x|]; rewrite (spec_eq0 x H); auto. + assert (x mod wB <> 0). + unfold eq0, to_Z in H. + intro H0; rewrite H0 in H; discriminate. + rewrite Z_mod_nz_opp_full; auto with zarith. + Qed. + + Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB. + Proof. + intros; unfold opp, to_Z; auto. + change ((- x) mod wB = (0 - (x mod wB)) mod wB). + rewrite Zminus_mod_idemp_r; simpl; auto. + Qed. + + Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1. + Proof. + intros; unfold opp_carry, to_Z; auto. + replace (- x - 1) with (- 1 - x) by omega. + rewrite <- Zminus_mod_idemp_r. + replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by omega. + rewrite <- (Z_mod_same_full wB). + rewrite Zplus_mod_idemp_l. + replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by omega. + apply Zmod_small. + generalize (Z_mod_lt x wB wB_pos); omega. + Qed. + + Definition succ_c x := + let y := Z.succ x in + if eq0 y then C1 0 else C0 y. + + Definition add_c x y := + let z := [|x|] + [|y|] in + if Z_lt_le_dec z wB then C0 z else C1 (z-wB). + + Definition add_carry_c x y := + let z := [|x|]+[|y|]+1 in + if Z_lt_le_dec z wB then C0 z else C1 (z-wB). + + Definition succ := Z.succ. + Definition add := Z.add. + Definition add_carry x y := x + y + 1. + + Lemma Zmod_equal : + forall x y z, z>0 -> (x-y) mod z = 0 -> x mod z = y mod z. + Proof. + intros. + generalize (Z_div_mod_eq (x-y) z H); rewrite H0, Z.add_0_r. + remember ((x-y)/z) as k. + rewrite Z.sub_move_r, Z.add_comm, Z.mul_comm. intros ->. + now apply Z_mod_plus. + Qed. + + Lemma spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1. + Proof. + intros; unfold succ_c, to_Z, Z.succ. + case_eq (eq0 (x+1)); intros; unfold interp_carry. + + rewrite Z.mul_1_l. + replace (wB + 0 mod wB) with wB by auto with zarith. + symmetry. rewrite Z.add_move_r. + assert ((x+1) mod wB = 0) by (apply spec_eq0; auto). + replace (wB-1) with ((wB-1) mod wB) by + (apply Zmod_small; generalize wB_pos; omega). + rewrite <- Zminus_mod_idemp_l; rewrite Z_mod_same; simpl; auto. + apply Zmod_equal; auto. + + assert ((x+1) mod wB <> 0). + unfold eq0, to_Z in *; now destruct ((x+1) mod wB). + assert (x mod wB + 1 <> wB). + contradict H0. + rewrite Z.add_move_r in H0; simpl in H0. + rewrite <- Zplus_mod_idemp_l; rewrite H0. + replace (wB-1+1) with wB; auto with zarith; apply Z_mod_same; auto. + rewrite <- Zplus_mod_idemp_l. + apply Zmod_small. + generalize (Z_mod_lt x wB wB_pos); omega. + Qed. + + Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. + Proof. + intros; unfold add_c, to_Z, interp_carry. + destruct Z_lt_le_dec. + apply Zmod_small; + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. + apply Zmod_small; + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + Qed. + + Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1. + Proof. + intros; unfold add_carry_c, to_Z, interp_carry. + destruct Z_lt_le_dec. + apply Zmod_small; + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. + apply Zmod_small; + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + Qed. + + Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB. + Proof. + intros; unfold succ, to_Z, Z.succ. + symmetry; apply Zplus_mod_idemp_l. + Qed. + + Lemma spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB. + Proof. + intros; unfold add, to_Z; apply Zplus_mod. + Qed. + + Lemma spec_add_carry : + forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB. + Proof. + intros; unfold add_carry, to_Z. + rewrite <- Zplus_mod_idemp_l. + rewrite (Zplus_mod x y). + rewrite Zplus_mod_idemp_l; auto. + Qed. + + Definition pred_c x := + if eq0 x then C1 (wB-1) else C0 (x-1). + + Definition sub_c x y := + let z := [|x|]-[|y|] in + if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z. + + Definition sub_carry_c x y := + let z := [|x|]-[|y|]-1 in + if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z. + + Definition pred := Z.pred. + Definition sub := Z.sub. + Definition sub_carry x y := x - y - 1. + + Lemma spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1. + Proof. + intros; unfold pred_c, to_Z, interp_carry. + case_eq (eq0 x); intros. + fold [|x|]; rewrite spec_eq0; auto. + replace ((wB-1) mod wB) with (wB-1); auto with zarith. + symmetry; apply Zmod_small; generalize wB_pos; omega. + + assert (x mod wB <> 0). + unfold eq0, to_Z in *; now destruct (x mod wB). + rewrite <- Zminus_mod_idemp_l. + apply Zmod_small. + generalize (Z_mod_lt x wB wB_pos); omega. + Qed. + + Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. + Proof. + intros; unfold sub_c, to_Z, interp_carry. + destruct Z_lt_le_dec. + replace ((wB + (x mod wB - y mod wB)) mod wB) with + (wB + (x mod wB - y mod wB)). + omega. + symmetry; apply Zmod_small. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + + apply Zmod_small. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + Qed. + + Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1. + Proof. + intros; unfold sub_carry_c, to_Z, interp_carry. + destruct Z_lt_le_dec. + replace ((wB + (x mod wB - y mod wB - 1)) mod wB) with + (wB + (x mod wB - y mod wB -1)). + omega. + symmetry; apply Zmod_small. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + + apply Zmod_small. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + Qed. + + Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB. + Proof. + intros; unfold pred, to_Z, Z.pred. + rewrite <- Zplus_mod_idemp_l; auto. + Qed. + + Lemma spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB. + Proof. + intros; unfold sub, to_Z; apply Zminus_mod. + Qed. + + Lemma spec_sub_carry : + forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB. + Proof. + intros; unfold sub_carry, to_Z. + rewrite <- Zminus_mod_idemp_l. + rewrite (Zminus_mod x y). + rewrite Zminus_mod_idemp_l. + auto. + Qed. + + Definition mul_c x y := + let (h,l) := Z.div_eucl ([|x|]*[|y|]) wB in + if eq0 h then if eq0 l then W0 else WW h l else WW h l. + + Definition mul := Z.mul. + + Definition square_c x := mul_c x x. + + Lemma spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|]. + Proof. + intros; unfold mul_c, zn2z_to_Z. + assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). + unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. + generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). + destruct 1; injection H as ? ?. + rewrite H0. + assert ([|l|] = l). + apply Zmod_small; auto. + assert ([|h|] = h). + apply Zmod_small. + subst h. + split. + apply Z_div_pos; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + apply Z.mul_lt_mono_nonneg; auto with zarith. + clear H H0 H1 H2. + case_eq (eq0 h); simpl; intros. + case_eq (eq0 l); simpl; intros. + rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto with zarith. + rewrite H3, H4; auto with zarith. + rewrite H3, H4; auto with zarith. + Qed. + + Lemma spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB. + Proof. + intros; unfold mul, to_Z; apply Zmult_mod. + Qed. + + Lemma spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|]. + Proof. + intros x; exact (spec_mul_c x x). + Qed. + + Definition div x y := Z.div_eucl [|x|] [|y|]. + + Lemma spec_div : forall a b, 0 < [|b|] -> + let (q,r) := div a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + intros; unfold div. + assert ([|b|]>0) by auto with zarith. + assert (Z.div_eucl [|a|] [|b|] = ([|a|]/[|b|], [|a|] mod [|b|])). + unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. + generalize (Z_div_mod [|a|] [|b|] H0). + destruct Z.div_eucl as (q,r); destruct 1; intros. + injection H1 as ? ?. + assert ([|r|]=r). + apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; + auto with zarith. + assert ([|q|]=q). + apply Zmod_small. + subst q. + split. + apply Z_div_pos; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + apply Z.lt_le_trans with (wB*1). + rewrite Z.mul_1_r; auto with zarith. + apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + rewrite H5, H6; rewrite Z.mul_comm; auto with zarith. + Qed. + + Definition div_gt := div. + + Lemma spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + let (q,r) := div_gt a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + intros. + apply spec_div; auto. + Qed. + + Definition modulo x y := [|x|] mod [|y|]. + Definition modulo_gt x y := [|x|] mod [|y|]. + + Lemma spec_modulo : forall a b, 0 < [|b|] -> + [|modulo a b|] = [|a|] mod [|b|]. + Proof. + intros; unfold modulo. + apply Zmod_small. + assert ([|b|]>0) by auto with zarith. + generalize (Z_mod_lt [|a|] [|b|] H0) (Z_mod_lt b wB wB_pos). + fold [|b|]; omega. + Qed. + + Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + [|modulo_gt a b|] = [|a|] mod [|b|]. + Proof. + intros; apply spec_modulo; auto. + Qed. + + Definition gcd x y := Z.gcd [|x|] [|y|]. + Definition gcd_gt x y := Z.gcd [|x|] [|y|]. + + Lemma Zgcd_bound : forall a b, 0<=a -> 0<=b -> Z.gcd a b <= Z.max a b. + Proof. + intros. + generalize (Zgcd_is_gcd a b); inversion_clear 1. + destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. + assert (H4:=Z.gcd_nonneg a b). + destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq]. + generalize (Zmax_spec a b); omega. + assert (0 <= q). + apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith. + destruct (Z.eq_dec q 0). + + subst q; simpl in *; subst a; simpl; auto. + generalize (Zmax_spec 0 b) (Zabs_spec b); omega. + + apply Z.le_trans with a. + rewrite H2 at 2. + rewrite <- (Z.mul_1_l (Z.gcd a b)) at 1. + apply Z.mul_le_mono_nonneg; auto with zarith. + generalize (Zmax_spec a b); omega. + Qed. + + Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. + Proof. + intros; unfold gcd. + generalize (Z_mod_lt a wB wB_pos)(Z_mod_lt b wB wB_pos); intros. + fold [|a|] in *; fold [|b|] in *. + replace ([|Z.gcd [|a|] [|b|]|]) with (Z.gcd [|a|] [|b|]). + apply Zgcd_is_gcd. + symmetry; apply Zmod_small. + split. + apply Z.gcd_nonneg. + apply Z.le_lt_trans with (Z.max [|a|] [|b|]). + apply Zgcd_bound; auto with zarith. + generalize (Zmax_spec [|a|] [|b|]); omega. + Qed. + + Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] -> + Zis_gcd [|a|] [|b|] [|gcd_gt a b|]. + Proof. + intros. apply spec_gcd; auto. + Qed. + + Definition div21 a1 a2 b := + Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]. + + Lemma spec_div21 : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := div21 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. + Proof. + intros; unfold div21. + generalize (Z_mod_lt a1 wB wB_pos); fold [|a1|]; intros. + generalize (Z_mod_lt a2 wB wB_pos); fold [|a2|]; intros. + assert ([|b|]>0) by auto with zarith. + remember ([|a1|]*wB+[|a2|]) as a. + assert (Z.div_eucl a [|b|] = (a/[|b|], a mod [|b|])). + unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. + generalize (Z_div_mod a [|b|] H3). + destruct Z.div_eucl as (q,r); destruct 1; intros. + injection H4 as ? ?. + assert ([|r|]=r). + apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; + auto with zarith. + assert ([|q|]=q). + apply Zmod_small. + subst q. + split. + apply Z_div_pos; auto with zarith. + subst a; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + subst a. + replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring. + apply Z.lt_le_trans with ([|a1|]*wB+wB); auto with zarith. + rewrite H8, H9; rewrite Z.mul_comm; auto with zarith. + Qed. + + Definition add_mul_div p x y := + ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos digits) - [|p|]))). + Lemma spec_add_mul_div : forall x y p, + [|p|] <= Zpos digits -> + [| add_mul_div p x y |] = + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB. + Proof. + intros; unfold add_mul_div; auto. + Qed. + + Definition pos_mod p w := [|w|] mod (2 ^ [|p|]). + Lemma spec_pos_mod : forall w p, + [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]). + Proof. + intros; unfold pos_mod. + apply Zmod_small. + generalize (Z_mod_lt [|w|] (2 ^ [|p|])); intros. + split. + destruct H; auto using Z.lt_gt with zarith. + apply Z.le_lt_trans with [|w|]; auto with zarith. + apply Zmod_le; auto with zarith. + Qed. + + Definition is_even x := + if Z.eq_dec ([|x|] mod 2) 0 then true else false. + + Lemma spec_is_even : forall x, + if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. + Proof. + intros; unfold is_even; destruct Z.eq_dec; auto. + generalize (Z_mod_lt [|x|] 2); omega. + Qed. + + Definition sqrt x := Z.sqrt [|x|]. + Lemma spec_sqrt : forall x, + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. + Proof. + intros. + unfold sqrt. + repeat rewrite Z.pow_2_r. + replace [|Z.sqrt [|x|]|] with (Z.sqrt [|x|]). + apply Z.sqrt_spec; auto with zarith. + symmetry; apply Zmod_small. + split. apply Z.sqrt_nonneg; auto. + apply Z.le_lt_trans with [|x|]; auto. + apply Z.sqrt_le_lin; auto. + Qed. + + Definition sqrt2 x y := + let z := [|x|]*wB+[|y|] in + match z with + | Z0 => (0, C0 0) + | Zpos p => + let (s,r) := Z.sqrtrem (Zpos p) in + (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB)) + | Zneg _ => (0, C0 0) + end. + + Lemma spec_sqrt2 : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := sqrt2 x y in + [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]. + Proof. + intros; unfold sqrt2. + simpl zn2z_to_Z. + remember ([|x|]*wB+[|y|]) as z. + destruct z. + auto with zarith. + generalize (Z.sqrtrem_spec (Zpos p)). + destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith. + assert (s < wB). + destruct (Z_lt_le_dec s wB); auto. + assert (wB * wB <= Zpos p). + rewrite U. + apply Z.le_trans with (s*s); try omega. + apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + assert (Zpos p < wB*wB). + rewrite Heqz. + replace (wB*wB) with ((wB-1)*wB+wB) by ring. + apply Z.add_le_lt_mono; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + generalize (spec_to_Z x); auto with zarith. + generalize wB_pos; auto with zarith. + omega. + replace [|s|] with s by (symmetry; apply Zmod_small; auto with zarith). + destruct Z_lt_le_dec; unfold interp_carry. + replace [|r|] with r by (symmetry; apply Zmod_small; auto with zarith). + rewrite Z.pow_2_r; auto with zarith. + replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; auto with zarith). + rewrite Z.pow_2_r; omega. + + assert (0<=Zneg p). + rewrite Heqz; generalize wB_pos; auto with zarith. + compute in H0; elim H0; auto. + Qed. + + Lemma two_p_power2 : forall x, x>=0 -> two_p x = 2 ^ x. + Proof. + intros. + unfold two_p. + destruct x; simpl; auto. + apply two_power_pos_correct. + Qed. + + Definition head0 x := match [|x|] with + | Z0 => zdigits + | Zpos p => zdigits - log_inf p - 1 + | _ => 0 + end. + + Lemma spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits. + Proof. + unfold head0; intros. + rewrite H; simpl. + apply spec_zdigits. + Qed. + + Lemma log_inf_bounded : forall x p, Zpos x < 2^p -> log_inf x < p. + Proof. + induction x; simpl; intros. + + assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). + cut (log_inf x < p - 1); [omega| ]. + apply IHx. + change (Zpos x~1) with (2*(Zpos x)+1) in H. + replace p with (Z.succ (p-1)) in H; auto with zarith. + rewrite Z.pow_succ_r in H; auto with zarith. + + assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). + cut (log_inf x < p - 1); [omega| ]. + apply IHx. + change (Zpos x~0) with (2*(Zpos x)) in H. + replace p with (Z.succ (p-1)) in H; auto with zarith. + rewrite Z.pow_succ_r in H; auto with zarith. + + simpl; intros; destruct p; compute; auto with zarith. + Qed. + + + Lemma spec_head0 : forall x, 0 < [|x|] -> + wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. + Proof. + intros; unfold head0. + generalize (spec_to_Z x). + destruct [|x|]; try discriminate. + intros. + destruct (log_inf_correct p). + rewrite 2 two_p_power2 in H2; auto with zarith. + assert (0 <= zdigits - log_inf p - 1 < wB). + split. + cut (log_inf p < zdigits); try omega. + unfold zdigits. + unfold wB, base in *. + apply log_inf_bounded; auto with zarith. + apply Z.lt_trans with zdigits. + omega. + unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. + + unfold to_Z; rewrite (Zmod_small _ _ H3). + destruct H2. + split. + apply Z.le_trans with (2^(zdigits - log_inf p - 1)*(2^log_inf p)). + apply Zdiv_le_upper_bound; auto with zarith. + rewrite <- Zpower_exp; auto with zarith. + rewrite Z.mul_comm; rewrite <- Z.pow_succ_r; auto with zarith. + replace (Z.succ (zdigits - log_inf p -1 +log_inf p)) with zdigits + by ring. + unfold wB, base, zdigits; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. + + apply Z.lt_le_trans + with (2^(zdigits - log_inf p - 1)*(2^(Z.succ (log_inf p)))). + apply Z.mul_lt_mono_pos_l; auto with zarith. + rewrite <- Zpower_exp; auto with zarith. + replace (zdigits - log_inf p -1 +Z.succ (log_inf p)) with zdigits + by ring. + unfold wB, base, zdigits; auto with zarith. + Qed. + + Fixpoint Ptail p := match p with + | xO p => (Ptail p)+1 + | _ => 0 + end. + + Lemma Ptail_pos : forall p, 0 <= Ptail p. + Proof. + induction p; simpl; auto with zarith. + Qed. + Hint Resolve Ptail_pos : core. + + Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. + Proof. + induction p; try (compute; auto; fail). + intros; simpl. + assert (d <> xH). + intro; subst. + compute in H; destruct p; discriminate. + assert (Z.succ (Zpos (Pos.pred d)) = Zpos d). + simpl; f_equal. + rewrite Pos.add_1_r. + destruct (Pos.succ_pred_or d); auto. + rewrite H1 in H0; elim H0; auto. + assert (Ptail p < Zpos (Pos.pred d)). + apply IHp. + apply Z.mul_lt_mono_pos_r with 2; auto with zarith. + rewrite (Z.mul_comm (Zpos p)). + change (2 * Zpos p) with (Zpos p~0). + rewrite Z.mul_comm. + rewrite <- Z.pow_succ_r; auto with zarith. + rewrite H1; auto. + rewrite <- H1; omega. + Qed. + + Definition tail0 x := + match [|x|] with + | Z0 => zdigits + | Zpos p => Ptail p + | Zneg _ => 0 + end. + + Lemma spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits. + Proof. + unfold tail0; intros. + rewrite H; simpl. + apply spec_zdigits. + Qed. + + Lemma spec_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]). + Proof. + intros; unfold tail0. + generalize (spec_to_Z x). + destruct [|x|]; try discriminate; intros. + assert ([|Ptail p|] = Ptail p). + apply Zmod_small. + split; auto. + unfold wB, base in *. + apply Z.lt_trans with (Zpos digits). + apply Ptail_bounded; auto with zarith. + apply Zpower2_lt_lin; auto with zarith. + rewrite H1. + + clear; induction p. + exists (Zpos p); simpl; rewrite Pos.mul_1_r; auto with zarith. + destruct IHp as (y & Yp & Ye). + exists y. + split; auto. + change (Zpos p~0) with (2*Zpos p). + rewrite Ye. + change (Ptail p~0) with (Z.succ (Ptail p)). + rewrite Z.pow_succ_r; auto; ring. + + exists 0; simpl; auto with zarith. + Qed. + + Definition lor := Z.lor. + Definition land := Z.land. + Definition lxor := Z.lxor. + + Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|]. + Proof. + unfold lor, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.lor_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.lor_spec; auto with zarith. + Qed. + + Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|]. + Proof. + unfold land, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.land_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.land_spec; auto with zarith. + Qed. + + Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|]. + Proof. + unfold lxor, to_Z. + apply Z.bits_inj'; intros n Hn. rewrite Z.lxor_spec. + unfold wB, base. + destruct (Z.le_gt_cases (Z.pos digits) n). + - rewrite !Z.mod_pow2_bits_high; auto with zarith. + - rewrite !Z.mod_pow2_bits_low, Z.lxor_spec; auto with zarith. + Qed. + + (** Let's now group everything in two records *) + + Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps + (digits : positive) + (zdigits: t) + (to_Z : t -> Z) + (of_pos : positive -> N * t) + (head0 : t -> t) + (tail0 : t -> t) + + (zero : t) + (one : t) + (minus_one : t) + + (compare : t -> t -> comparison) + (eq0 : t -> bool) + + (opp_c : t -> carry t) + (opp : t -> t) + (opp_carry : t -> t) + + (succ_c : t -> carry t) + (add_c : t -> t -> carry t) + (add_carry_c : t -> t -> carry t) + (succ : t -> t) + (add : t -> t -> t) + (add_carry : t -> t -> t) + + (pred_c : t -> carry t) + (sub_c : t -> t -> carry t) + (sub_carry_c : t -> t -> carry t) + (pred : t -> t) + (sub : t -> t -> t) + (sub_carry : t -> t -> t) + + (mul_c : t -> t -> zn2z t) + (mul : t -> t -> t) + (square_c : t -> zn2z t) + + (div21 : t -> t -> t -> t*t) + (div_gt : t -> t -> t * t) + (div : t -> t -> t * t) + + (modulo_gt : t -> t -> t) + (modulo : t -> t -> t) + + (gcd_gt : t -> t -> t) + (gcd : t -> t -> t) + (add_mul_div : t -> t -> t -> t) + (pos_mod : t -> t -> t) + + (is_even : t -> bool) + (sqrt2 : t -> t -> t * carry t) + (sqrt : t -> t) + (lor : t -> t -> t) + (land : t -> t -> t) + (lxor : t -> t -> t). + + Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs + spec_to_Z + spec_of_pos + spec_zdigits + spec_more_than_1_digit + + spec_0 + spec_1 + spec_Bm1 + + spec_compare + spec_eq0 + + spec_opp_c + spec_opp + spec_opp_carry + + spec_succ_c + spec_add_c + spec_add_carry_c + spec_succ + spec_add + spec_add_carry + + spec_pred_c + spec_sub_c + spec_sub_carry_c + spec_pred + spec_sub + spec_sub_carry + + spec_mul_c + spec_mul + spec_square_c + + spec_div21 + spec_div_gt + spec_div + + spec_modulo_gt + spec_modulo + + spec_gcd_gt + spec_gcd + + spec_head00 + spec_head0 + spec_tail00 + spec_tail0 + + spec_add_mul_div + spec_pos_mod + + spec_is_even + spec_sqrt2 + spec_sqrt + spec_lor + spec_land + spec_lxor. + +End ZModulo. + +(** A modular version of the previous construction. *) + +Module Type PositiveNotOne. + Parameter p : positive. + Axiom not_one : p <> 1%positive. +End PositiveNotOne. + +Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType. + Definition t := Z. + Instance ops : ZnZ.Ops t := zmod_ops P.p. + Instance specs : ZnZ.Specs ops := zmod_specs P.not_one. +End ZModuloCyclicType. |