diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 192 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 524 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 929 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 64 |
4 files changed, 934 insertions, 775 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 16007656..cab4b154 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -6,28 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BigN.v 11576 2008-11-10 19:13:15Z msozeau $ i*) +(** * Efficient arbitrary large natural numbers in base 2^31 *) -(** * Natural numbers in base 2^31 *) - -(** -Author: Arnaud Spiwack -*) +(** Initial Author: Arnaud Spiwack *) Require Export Int31. -Require Import CyclicAxioms. -Require Import Cyclic31. -Require Import NSig. -Require Import NSigNAxioms. -Require Import NMake. -Require Import NSub. +Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake + NProperties NDiv GenericMinMax. + +(** The following [BigN] module regroups both the operations and + all the abstract properties: -Module BigN <: NType := NMake.Make Int31Cyclic. + - [NMake.Make Int31Cyclic] provides the operations and basic specs + w.r.t. ZArith + - [NTypeIsNAxioms] shows (mainly) that these operations implement + the interface [NAxioms] + - [NPropSig] adds all generic properties derived from [NAxioms] + - [NDivPropFunct] provides generic properties of [div] and [mod]. + - [MinMax*Properties] provides properties of [min] and [max]. + +*) -(** Module [BigN] implements [NAxiomsSig] *) +Module BigN <: NType <: OrderedTypeFull <: TotalOrder := + NMake.Make Int31Cyclic <+ NTypeIsNAxioms + <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec + <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. -Module Export BigNAxiomsMod := NSig_NAxioms BigN. -Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod. (** Notations about [BigN] *) @@ -37,49 +41,171 @@ Delimit Scope bigN_scope with bigN. Bind Scope bigN_scope with bigN. Bind Scope bigN_scope with BigN.t. Bind Scope bigN_scope with BigN.t_. - -Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *) +(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) +Arguments Scope BigN.to_Z [bigN_scope]. +Arguments Scope BigN.succ [bigN_scope]. +Arguments Scope BigN.pred [bigN_scope]. +Arguments Scope BigN.square [bigN_scope]. +Arguments Scope BigN.add [bigN_scope bigN_scope]. +Arguments Scope BigN.sub [bigN_scope bigN_scope]. +Arguments Scope BigN.mul [bigN_scope bigN_scope]. +Arguments Scope BigN.div [bigN_scope bigN_scope]. +Arguments Scope BigN.eq [bigN_scope bigN_scope]. +Arguments Scope BigN.lt [bigN_scope bigN_scope]. +Arguments Scope BigN.le [bigN_scope bigN_scope]. +Arguments Scope BigN.eq [bigN_scope bigN_scope]. +Arguments Scope BigN.compare [bigN_scope bigN_scope]. +Arguments Scope BigN.min [bigN_scope bigN_scope]. +Arguments Scope BigN.max [bigN_scope bigN_scope]. +Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. +Arguments Scope BigN.power_pos [bigN_scope positive_scope]. +Arguments Scope BigN.power [bigN_scope N_scope]. +Arguments Scope BigN.sqrt [bigN_scope]. +Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. +Arguments Scope BigN.modulo [bigN_scope bigN_scope]. +Arguments Scope BigN.gcd [bigN_scope bigN_scope]. + +Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) +Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) Infix "+" := BigN.add : bigN_scope. Infix "-" := BigN.sub : bigN_scope. Infix "*" := BigN.mul : bigN_scope. Infix "/" := BigN.div : bigN_scope. +Infix "^" := BigN.power : bigN_scope. Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. +Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. Infix "<=" := BigN.le : bigN_scope. Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. +Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope. +Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope. +Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. +Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope. -Open Scope bigN_scope. +Local Open Scope bigN_scope. (** Example of reasoning about [BigN] *) -Theorem succ_pred: forall q:bigN, +Theorem succ_pred: forall q : bigN, 0 < q -> BigN.succ (BigN.pred q) == q. Proof. -intros; apply succ_pred. +intros; apply BigN.succ_pred. intro H'; rewrite H' in H; discriminate. Qed. (** [BigN] is a semi-ring *) -Lemma BigNring : - semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. +Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq. +Proof. +constructor. +exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc. +exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm. +exact BigN.mul_assoc. exact BigN.mul_add_distr_r. +Qed. + +Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y. +Proof. now apply BigN.eqb_eq. Qed. + +Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power. Proof. constructor. -exact add_0_l. -exact add_comm. -exact add_assoc. -exact mul_1_l. -exact mul_0_l. -exact mul_comm. -exact mul_assoc. -exact mul_add_distr_r. +intros. red. rewrite BigN.spec_power. unfold id. +destruct Zpower_theory as [EQ]. rewrite EQ. +destruct n; simpl. reflexivity. +induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. +Qed. + +Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) + (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b). +Proof. +constructor. unfold id. intros a b. +BigN.zify. +generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +BigN.zify. auto with zarith. +intros NEQ. +generalize (BigN.spec_div_eucl a b). +generalize (Z_div_mod_full [a] [b] NEQ). +destruct BigN.div_eucl as (q,r), Zdiv_eucl as (q',r'). +intros (EQ,_). injection 1. intros EQr EQq. +BigN.zify. rewrite EQr, EQq; auto. +Qed. + + +(** Detection of constants *) + +Ltac isStaticWordCst t := + match t with + | W0 => constr:true + | WW ?t1 ?t2 => + match isStaticWordCst t1 with + | false => constr:false + | true => isStaticWordCst t2 + end + | _ => isInt31cst t + end. + +Ltac isBigNcst t := + match t with + | BigN.N0 ?t => isStaticWordCst t + | BigN.N1 ?t => isStaticWordCst t + | BigN.N2 ?t => isStaticWordCst t + | BigN.N3 ?t => isStaticWordCst t + | BigN.N4 ?t => isStaticWordCst t + | BigN.N5 ?t => isStaticWordCst t + | BigN.N6 ?t => isStaticWordCst t + | BigN.Nn ?n ?t => match isnatcst n with + | true => isStaticWordCst t + | false => constr:false + end + | BigN.zero => constr:true + | BigN.one => constr:true + | _ => constr:false + end. + +Ltac BigNcst t := + match isBigNcst t with + | true => constr:t + | false => constr:NotConstant + end. + +Ltac Ncst t := + match isNcst t with + | true => constr:t + | false => constr:NotConstant + end. + +(** Registration for the "ring" tactic *) + +Add Ring BigNr : BigNring + (decidable BigNeqb_correct, + constants [BigNcst], + power_tac BigNpower [Ncst], + div BigNdiv). + +Section TestRing. +Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +intros. ring_simplify. reflexivity. Qed. +End TestRing. + +(** We benefit also from an "order" tactic *) + +Ltac bigN_order := BigN.order. + +Section TestOrder. +Let test : forall x y : bigN, x<=y -> y<=x -> x==y. +Proof. bigN_order. Qed. +End TestOrder. -Add Ring BigNr : BigNring. +(** We can use at least a bit of (r)omega by translating to [Z]. *) -(** Todo: tactic translating from [BigN] to [Z] + omega *) +Section TestOmega. +Let test : forall x y : bigN, x<=y -> y<=x -> x==y. +Proof. intros x y. BigN.zify. omega. Qed. +End TestOmega. (** Todo: micromega *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v new file mode 100644 index 00000000..925b0535 --- /dev/null +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -0,0 +1,524 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(** * NMake *) + +(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*) + +(** NB: This file contain the part which is independent from the underlying + representation. The representation-dependent (and macro-generated) part + is now in [NMake_gen]. *) + +Require Import BigNumPrelude ZArith CyclicAxioms. +Require Import Nbasic Wf_nat StreamMemo NSig NMake_gen. + +Module Make (Import W0:CyclicType) <: NType. + + (** Macro-generated part *) + + Include NMake_gen.Make W0. + + + (** * Predecessor *) + + Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1). + Proof. + intros. destruct (Zle_lt_or_eq _ _ (spec_pos x)). + rewrite Zmax_r; auto with zarith. + apply spec_pred_pos; auto. + rewrite <- H; apply spec_pred0; auto. + Qed. + + + (** * Subtraction *) + + Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]). + Proof. + intros. destruct (Zle_or_lt [y] [x]). + rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto. + rewrite Zmax_l; auto with zarith. apply spec_sub0; auto. + Qed. + + (** * Comparison *) + + Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y]. + Proof. + intros x y. generalize (spec_compare_aux x y); destruct compare; + intros; symmetry; try rewrite Zcompare_Eq_iff_eq; assumption. + Qed. + + Definition eq_bool x y := + match compare x y with + | Eq => true + | _ => false + end. + + Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y]. + Proof. + intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity. + Qed. + + Theorem spec_eq_bool_aux: forall x y, + if eq_bool x y then [x] = [y] else [x] <> [y]. + Proof. + intros x y; unfold eq_bool. + generalize (spec_compare_aux x y); case compare; auto with zarith. + Qed. + + Definition lt n m := [n] < [m]. + Definition le n m := [n] <= [m]. + + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Theorem spec_max : forall n m, [max n m] = Zmax [n] [m]. + Proof. + intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity. + Qed. + + Theorem spec_min : forall n m, [min n m] = Zmin [n] [m]. + Proof. + intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity. + Qed. + + + (** * Power *) + + Fixpoint power_pos (x:t) (p:positive) {struct p} : t := + match p with + | xH => x + | xO p => square (power_pos x p) + | xI p => mul (square (power_pos x p)) x + end. + + Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Proof. + intros x n; generalize x; elim n; clear n x; simpl power_pos. + intros; rewrite spec_mul; rewrite spec_square; rewrite H. + rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith. + rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. + rewrite Zpower_2; rewrite Zpower_1_r; auto. + intros; rewrite spec_square; rewrite H. + rewrite Zpos_xO; auto with zarith. + rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. + rewrite Zpower_2; auto. + intros; rewrite Zpower_1_r; auto. + Qed. + + Definition power x (n:N) := match n with + | BinNat.N0 => one + | BinNat.Npos p => power_pos x p + end. + + Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. + Proof. + destruct n; simpl. apply (spec_1 w0_spec). + apply spec_power_pos. + Qed. + + + (** * Div *) + + Definition div_eucl x y := + if eq_bool y zero then (zero,zero) else + match compare x y with + | Eq => (one, zero) + | Lt => (zero, x) + | Gt => div_gt x y + end. + + Theorem spec_div_eucl: forall x y, + let (q,r) := div_eucl x y in + ([q], [r]) = Zdiv_eucl [x] [y]. + Proof. + assert (F0: [zero] = 0). + exact (spec_0 w0_spec). + assert (F1: [one] = 1). + exact (spec_1 w0_spec). + intros x y. unfold div_eucl. + generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. + intro H. rewrite H. destruct [x]; auto. + intro H'. + assert (0 < [y]) by (generalize (spec_pos y); auto with zarith). + clear H'. + generalize (spec_compare_aux x y); case compare; try rewrite F0; + try rewrite F1; intros; auto with zarith. + rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H)) + (Z_mod_same [y] (Zlt_gt _ _ H)); + unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. + assert (F2: 0 <= [x] < [y]). + generalize (spec_pos x); auto. + generalize (Zdiv_small _ _ F2) + (Zmod_small _ _ F2); + unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. + generalize (spec_div_gt _ _ H0 H); auto. + unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt. + intros a b c d (H1, H2); subst; auto. + Qed. + + Definition div x y := fst (div_eucl x y). + + Theorem spec_div: + forall x y, [div x y] = [x] / [y]. + Proof. + intros x y; unfold div; generalize (spec_div_eucl x y); + case div_eucl; simpl fst. + intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; + injection H; auto. + Qed. + + + (** * Modulo *) + + Definition modulo x y := + if eq_bool y zero then zero else + match compare x y with + | Eq => zero + | Lt => x + | Gt => mod_gt x y + end. + + Theorem spec_modulo: + forall x y, [modulo x y] = [x] mod [y]. + Proof. + assert (F0: [zero] = 0). + exact (spec_0 w0_spec). + assert (F1: [one] = 1). + exact (spec_1 w0_spec). + intros x y. unfold modulo. + generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. + intro H; rewrite H. destruct [x]; auto. + intro H'. + assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). + clear H'. + generalize (spec_compare_aux x y); case compare; try rewrite F0; + try rewrite F1; intros; try split; auto with zarith. + rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith. + apply sym_equal; apply Zmod_small; auto with zarith. + generalize (spec_pos x); auto with zarith. + apply spec_mod_gt; auto. + Qed. + + + (** * Gcd *) + + Definition gcd_gt_body a b cont := + match compare b zero with + | Gt => + let r := mod_gt a b in + match compare r zero with + | Gt => cont r (mod_gt b r) + | _ => b + end + | _ => a + end. + + Theorem Zspec_gcd_gt_body: forall a b cont p, + [a] > [b] -> [a] < 2 ^ p -> + (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] -> + Zis_gcd [a1] [b1] [cont a1 b1]) -> + Zis_gcd [a] [b] [gcd_gt_body a b cont]. + Proof. + assert (F1: [zero] = 0). + unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. + intros a b cont p H2 H3 H4; unfold gcd_gt_body. + generalize (spec_compare_aux b zero); case compare; try rewrite F1. + intros HH; rewrite HH; apply Zis_gcd_0. + intros HH; absurd (0 <= [b]); auto with zarith. + case (spec_digits b); auto with zarith. + intros H5; generalize (spec_compare_aux (mod_gt a b) zero); + case compare; try rewrite F1. + intros H6; rewrite <- (Zmult_1_r [b]). + rewrite (Z_div_mod_eq [a] [b]); auto with zarith. + rewrite <- spec_mod_gt; auto with zarith. + rewrite H6; rewrite Zplus_0_r. + apply Zis_gcd_mult; apply Zis_gcd_1. + intros; apply False_ind. + case (spec_digits (mod_gt a b)); auto with zarith. + intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith. + apply DoubleDiv.Zis_gcd_mod; auto with zarith. + rewrite <- spec_mod_gt; auto with zarith. + assert (F2: [b] > [mod_gt a b]). + case (Z_mod_lt [a] [b]); auto with zarith. + repeat rewrite <- spec_mod_gt; auto with zarith. + assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)]). + case (Z_mod_lt [b] [mod_gt a b]); auto with zarith. + rewrite <- spec_mod_gt; auto with zarith. + repeat rewrite <- spec_mod_gt; auto with zarith. + apply H4; auto with zarith. + apply Zmult_lt_reg_r with 2; auto with zarith. + apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith. + apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. + apply Zplus_le_compat_r. + pattern [b] at 1; rewrite <- (Zmult_1_l [b]). + apply Zmult_le_compat_r; auto with zarith. + case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith. + intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2; + try rewrite <- HH in H2; auto with zarith. + case (Z_mod_lt [a] [b]); auto with zarith. + rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith. + rewrite <- Z_div_mod_eq; auto with zarith. + pattern 2 at 2; rewrite <- (Zpower_1_r 2). + rewrite <- Zpower_exp; auto with zarith. + ring_simplify (p - 1 + 1); auto. + case (Zle_lt_or_eq 0 p); auto with zarith. + generalize H3; case p; simpl Zpower; auto with zarith. + intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith. + Qed. + + Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t := + gcd_gt_body a b + (fun a b => + match p with + | xH => cont a b + | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b + | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b + end). + + Theorem Zspec_gcd_gt_aux: forall p n a b cont, + [a] > [b] -> [a] < 2 ^ (Zpos p + n) -> + (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] -> + Zis_gcd [a1] [b1] [cont a1 b1]) -> + Zis_gcd [a] [b] [gcd_gt_aux p cont a b]. + intros p; elim p; clear p. + intros p Hrec n a b cont H2 H3 H4. + unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto. + intros a1 b1 H6 H7. + apply Hrec with (Zpos p + n); auto. + replace (Zpos p + (Zpos p + n)) with + (Zpos (xI p) + n - 1); auto. + rewrite Zpos_xI; ring. + intros a2 b2 H9 H10. + apply Hrec with n; auto. + intros p Hrec n a b cont H2 H3 H4. + unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto. + intros a1 b1 H6 H7. + apply Hrec with (Zpos p + n - 1); auto. + replace (Zpos p + (Zpos p + n - 1)) with + (Zpos (xO p) + n - 1); auto. + rewrite Zpos_xO; ring. + intros a2 b2 H9 H10. + apply Hrec with (n - 1); auto. + replace (Zpos p + (n - 1)) with + (Zpos p + n - 1); auto with zarith. + intros a3 b3 H12 H13; apply H4; auto with zarith. + apply Zlt_le_trans with (1 := H12). + case (Zle_or_lt 1 n); intros HH. + apply Zpower_le_monotone; auto with zarith. + apply Zle_trans with 0; auto with zarith. + assert (HH1: n - 1 < 0); auto with zarith. + generalize HH1; case (n - 1); auto with zarith. + intros p1 HH2; discriminate. + intros n a b cont H H2 H3. + simpl gcd_gt_aux. + apply Zspec_gcd_gt_body with (n + 1); auto with zarith. + rewrite Zplus_comm; auto. + intros a1 b1 H5 H6; apply H3; auto. + replace n with (n + 1 - 1); auto; try ring. + Qed. + + Definition gcd_cont a b := + match compare one b with + | Eq => one + | _ => a + end. + + Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b. + + Theorem spec_gcd_gt: forall a b, + [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b]. + Proof. + intros a b H2. + case (spec_digits (gcd_gt a b)); intros H3 H4. + case (spec_digits a); intros H5 H6. + apply sym_equal; apply Zis_gcd_gcd; auto with zarith. + unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith. + intros a1 a2; rewrite Zpower_0_r. + case (spec_digits a2); intros H7 H8; + intros; apply False_ind; auto with zarith. + Qed. + + Definition gcd a b := + match compare a b with + | Eq => a + | Lt => gcd_gt b a + | Gt => gcd_gt a b + end. + + Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]. + Proof. + intros a b. + case (spec_digits a); intros H1 H2. + case (spec_digits b); intros H3 H4. + unfold gcd; generalize (spec_compare_aux a b); case compare. + intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto. + apply Zis_gcd_refl. + intros; apply trans_equal with (Zgcd [b] [a]). + apply spec_gcd_gt; auto with zarith. + apply Zis_gcd_gcd; auto with zarith. + apply Zgcd_is_pos. + apply Zis_gcd_sym; apply Zgcd_is_gcd. + intros; apply spec_gcd_gt; auto. + Qed. + + + (** * Conversion *) + + Definition of_N x := + match x with + | BinNat.N0 => zero + | Npos p => of_pos p + end. + + Theorem spec_of_N: forall x, + [of_N x] = Z_of_N x. + Proof. + intros x; case x. + simpl of_N. + unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. + intros p; exact (spec_of_pos p). + Qed. + + + (** * Shift *) + + Definition shiftr n x := + match compare n (Ndigits x) with + | Lt => unsafe_shiftr n x + | _ => N0 w_0 + end. + + Theorem spec_shiftr: forall n x, + [shiftr n x] = [x] / 2 ^ [n]. + Proof. + intros n x; unfold shiftr; + generalize (spec_compare_aux n (Ndigits x)); case compare; intros H. + apply trans_equal with (1 := spec_0 w0_spec). + apply sym_equal; apply Zdiv_small; rewrite H. + rewrite spec_Ndigits; exact (spec_digits x). + rewrite <- spec_unsafe_shiftr; auto with zarith. + apply trans_equal with (1 := spec_0 w0_spec). + apply sym_equal; apply Zdiv_small. + rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2. + split; auto. + apply Zlt_le_trans with (1 := H2). + apply Zpower_le_monotone; auto with zarith. + Qed. + + Definition shiftl_aux_body cont n x := + match compare n (head0 x) with + Gt => cont n (double_size x) + | _ => unsafe_shiftl n x + end. + + Theorem spec_shiftl_aux_body: forall n p x cont, + 2^ Zpos p <= [head0 x] -> + (forall x, 2 ^ (Zpos p + 1) <= [head0 x]-> + [cont n x] = [x] * 2 ^ [n]) -> + [shiftl_aux_body cont n x] = [x] * 2 ^ [n]. + Proof. + intros n p x cont H1 H2; unfold shiftl_aux_body. + generalize (spec_compare_aux n (head0 x)); case compare; intros H. + apply spec_unsafe_shiftl; auto with zarith. + apply spec_unsafe_shiftl; auto with zarith. + rewrite H2. + rewrite spec_double_size; auto. + rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith. + apply Zle_trans with (2 := spec_double_size_head0 x). + rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith. + Qed. + + Fixpoint shiftl_aux p cont n x {struct p} := + shiftl_aux_body + (fun n x => match p with + | xH => cont n x + | xO p => shiftl_aux p (shiftl_aux p cont) n x + | xI p => shiftl_aux p (shiftl_aux p cont) n x + end) n x. + + Theorem spec_shiftl_aux: forall p q n x cont, + 2 ^ (Zpos q) <= [head0 x] -> + (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] -> + [cont n x] = [x] * 2 ^ [n]) -> + [shiftl_aux p cont n x] = [x] * 2 ^ [n]. + Proof. + intros p; elim p; unfold shiftl_aux; fold shiftl_aux; clear p. + intros p Hrec q n x cont H1 H2. + apply spec_shiftl_aux_body with (q); auto. + intros x1 H3; apply Hrec with (q + 1)%positive; auto. + intros x2 H4; apply Hrec with (p + q + 1)%positive; auto. + rewrite <- Pplus_assoc. + rewrite Zpos_plus_distr; auto. + intros x3 H5; apply H2. + rewrite Zpos_xI. + replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1)); + auto. + repeat rewrite Zpos_plus_distr; ring. + intros p Hrec q n x cont H1 H2. + apply spec_shiftl_aux_body with (q); auto. + intros x1 H3; apply Hrec with (q); auto. + apply Zle_trans with (2 := H3); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + intros x2 H4; apply Hrec with (p + q)%positive; auto. + intros x3 H5; apply H2. + rewrite (Zpos_xO p). + replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q)); + auto. + repeat rewrite Zpos_plus_distr; ring. + intros q n x cont H1 H2. + apply spec_shiftl_aux_body with (q); auto. + rewrite Zplus_comm; auto. + Qed. + + Definition shiftl n x := + shiftl_aux_body + (shiftl_aux_body + (shiftl_aux (digits n) unsafe_shiftl)) n x. + + Theorem spec_shiftl: forall n x, + [shiftl n x] = [x] * 2 ^ [n]. + Proof. + intros n x; unfold shiftl, shiftl_aux_body. + generalize (spec_compare_aux n (head0 x)); case compare; intros H. + apply spec_unsafe_shiftl; auto with zarith. + apply spec_unsafe_shiftl; auto with zarith. + rewrite <- (spec_double_size x). + generalize (spec_compare_aux n (head0 (double_size x))); case compare; intros H1. + apply spec_unsafe_shiftl; auto with zarith. + apply spec_unsafe_shiftl; auto with zarith. + rewrite <- (spec_double_size (double_size x)). + apply spec_shiftl_aux with 1%positive. + apply Zle_trans with (2 := spec_double_size_head0 (double_size x)). + replace (2 ^ 1) with (2 * 1). + apply Zmult_le_compat_l; auto with zarith. + generalize (spec_double_size_head0_pos x); auto with zarith. + rewrite Zpower_1_r; ring. + intros x1 H2; apply spec_unsafe_shiftl. + apply Zle_trans with (2 := H2). + apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith. + case (spec_digits n); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + Qed. + + + (** * Zero and One *) + + Theorem spec_0: [zero] = 0. + Proof. + exact (spec_0 w0_spec). + Qed. + + Theorem spec_1: [one] = 1. + Proof. + exact (spec_1 w0_spec). + Qed. + + +End Make. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 04c7b96d..b8552a39 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,14 +8,14 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMake_gen.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) (*S NMake_gen.ml : this file generates NMake.v *) (*s The two parameters that control the generation: *) -let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ +let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ process before relying on a generic construct *) let gen_proof = true (* should we generate proofs ? *) @@ -27,18 +27,18 @@ let c = "N" let pz n = if n == 0 then "w_0" else "W0" let rec gen2 n = if n == 0 then "1" else if n == 1 then "2" else "2 * " ^ (gen2 (n - 1)) -let rec genxO n s = +let rec genxO n s = if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")" -(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to - /dev/null, but for being compatible with earlier ocaml and not - relying on system-dependent stuff like open_out "/dev/null", +(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to + /dev/null, but for being compatible with earlier ocaml and not + relying on system-dependent stuff like open_out "/dev/null", let's use instead a magical hack *) (* Standard printer, with a final newline *) let pr s = Printf.printf (s^^"\n") (* Printing to /dev/null *) -let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) +let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) : ('a, out_channel, unit) format -> 'a) (* Proof printer : prints iff gen_proof is true *) let pp = if gen_proof then pr else pn @@ -51,7 +51,7 @@ let pp0 = if gen_proof then pr0 else pn (*s The actual printing *) -let _ = +let _ = pr "(************************************************************************)"; pr "(* v * The Coq Proof Assistant / The Coq Development Team *)"; @@ -67,21 +67,13 @@ let _ = pr ""; pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)"; pr ""; - pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; + pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; pr ""; - pr "Require Import BigNumPrelude."; - pr "Require Import ZArith."; - pr "Require Import CyclicAxioms."; - pr "Require Import DoubleType."; - pr "Require Import DoubleMul."; - pr "Require Import DoubleDivn1."; - pr "Require Import DoubleCyclic."; - pr "Require Import Nbasic."; - pr "Require Import Wf_nat."; - pr "Require Import StreamMemo."; - pr "Require Import NSig."; + pr "Require Import BigNumPrelude ZArith CyclicAxioms"; + pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic"; + pr " Wf_nat StreamMemo."; pr ""; - pr "Module Make (Import W0:CyclicType) <: NType."; + pr "Module Make (Import W0:CyclicType)."; pr ""; pr " Definition w0 := W0.w."; @@ -132,7 +124,7 @@ let _ = pr ""; pr " Inductive %s_ :=" t; - for i = 0 to size do + for i = 0 to size do pr " | %s%i : w%i -> %s_" c i i t done; pr " | %sn : forall n, word w%i (S n) -> %s_." c size t; @@ -167,20 +159,20 @@ let _ = pr " Definition to_N x := Zabs_N (to_Z x)."; pr ""; - + pr " Definition eq x y := (to_Z x = to_Z y)."; pr ""; pp " (* Regular make op (no karatsuba) *)"; - pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : "; + pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) :"; pp " znz_op (word ww n) :="; - pp " match n return znz_op (word ww n) with "; + pp " match n return znz_op (word ww n) with"; pp " O => ww_op"; - pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1) "; + pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1)"; pp " end."; pp ""; pp " (* Simplification by rewriting for nmake_op *)"; - pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x, "; + pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x,"; pp " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x)."; pp " auto."; pp " Qed."; @@ -191,7 +183,7 @@ let _ = for i = 0 to size do pp " Let nmake_op%i := nmake_op _ w%i_op." i i; pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i; - if i == 0 then + if i == 0 then pr " Let extend%i := DoubleBase.extend (WW w_0)." i else pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; @@ -199,8 +191,8 @@ let _ = pr ""; - pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww), "; - pp " znz_digits (nmake_op _ w_op n) = "; + pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww),"; + pp " znz_digits (nmake_op _ w_op n) ="; pp " DoubleBase.double_digits (znz_digits w_op) n."; pp " Proof."; pp " intros n; elim n; auto; clear n."; @@ -208,7 +200,7 @@ let _ = pp " rewrite <- Hrec; auto."; pp " Qed."; pp ""; - pp " Theorem nmake_double: forall n ww (w_op: znz_op ww), "; + pp " Theorem nmake_double: forall n ww (w_op: znz_op ww),"; pp " znz_to_Z (nmake_op _ w_op n) ="; pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n."; pp " Proof."; @@ -220,8 +212,8 @@ let _ = pp ""; - pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww), "; - pp " znz_digits (nmake_op _ w_op (S n)) = "; + pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww),"; + pp " znz_digits (nmake_op _ w_op (S n)) ="; pp " xO (znz_digits (nmake_op _ w_op n))."; pp " Proof."; pp " auto."; @@ -257,30 +249,30 @@ let _ = pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n))))."; pp " rewrite Hrec; auto with arith."; pp " Qed."; - pp " "; + pp ""; for i = 1 to size + 2 do pp " Let znz_to_Z_%i: forall x y," i; - pp " znz_to_Z w%i_op (WW x y) = " i; + pp " znz_to_Z w%i_op (WW x y) =" i; pp " znz_to_Z w%i_op x * base (znz_digits w%i_op) + znz_to_Z w%i_op y." (i-1) (i-1) (i-1); pp " Proof."; pp " auto."; - pp " Qed. "; + pp " Qed."; pp ""; done; pp " Let znz_to_Z_n: forall n x y,"; - pp " znz_to_Z (make_op (S n)) (WW x y) = "; + pp " znz_to_Z (make_op (S n)) (WW x y) ="; pp " znz_to_Z (make_op n) x * base (znz_digits (make_op n)) + znz_to_Z (make_op n) y."; pp " Proof."; pp " intros n x y; rewrite make_op_S; auto."; - pp " Qed. "; + pp " Qed."; pp ""; pp " Let w0_spec: znz_spec w0_op := W0.w_spec."; for i = 1 to 3 do - pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1) + pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1) done; for i = 4 to size + 3 do pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1) @@ -309,14 +301,14 @@ let _ = for i = 0 to size do - pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i; + pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i; if i == 0 then pp " auto." else pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1); pp " Qed."; pp ""; - pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; + pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; pp " Proof."; pp " intros n; exact (nmake_double n w%i w%i_op)." i i; pp " Qed."; @@ -325,7 +317,7 @@ let _ = for i = 0 to size do for j = 0 to (size - i) do - pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j; + pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j; pp " Proof."; if j == 0 then if i == 0 then @@ -346,7 +338,7 @@ let _ = end; pp " Qed."; pp ""; - pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; + pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; pp " Proof."; if j == 0 then pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i @@ -363,7 +355,7 @@ let _ = pp " Qed."; if i + j <> size then begin - pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j; + pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j; if j == 0 then begin pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j); @@ -393,7 +385,7 @@ let _ = pp " Qed."; pp ""; - pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1); + pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1); pp " Proof."; pp " intros x; case x."; pp " auto."; @@ -405,7 +397,7 @@ let _ = pp " Qed."; pp ""; - pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2); + pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2); pp " intros x; case x."; pp " auto."; pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2); @@ -430,7 +422,7 @@ let _ = pp " Qed."; pp ""; - pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size; + pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size; pp " intros n; elim n; clear n."; pp " exact spec_eval%in1." size; pp " intros n Hrec x; case x; clear x."; @@ -446,7 +438,7 @@ let _ = pp " Qed."; pp ""; - pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ; + pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ; pp " intros n; elim n; clear n."; pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size; pp " unfold to_Z."; @@ -478,7 +470,6 @@ let _ = pp " unfold to_Z."; pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto."; pp " Qed."; - pp " Hint Rewrite spec_extendn_0: extr."; pp ""; pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c; pp " Proof."; @@ -489,7 +480,6 @@ let _ = pp " case n; auto."; pp " intros n1; rewrite make_op_S; auto."; pp " Qed."; - pp " Hint Rewrite spec_extendn_0: extr."; pp ""; pp " Let spec_extend_tr: forall m n (w: word _ (S n)),"; pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c; @@ -498,7 +488,6 @@ let _ = pp " intros n x; simpl extend_tr."; pp " simpl plus; rewrite spec_extendn0_0; auto."; pp " Qed."; - pp " Hint Rewrite spec_extend_tr: extr."; pp ""; pp " Let spec_cast_l: forall n m x1,"; pp " [%sn (Max.max n m)" c; @@ -508,7 +497,6 @@ let _ = pp " intros n m x1; case (diff_r n m); simpl castm."; pp " rewrite spec_extend_tr; auto."; pp " Qed."; - pp " Hint Rewrite spec_cast_l: extr."; pp ""; pp " Let spec_cast_r: forall n m x1,"; pp " [%sn (Max.max n m)" c; @@ -518,7 +506,6 @@ let _ = pp " intros n m x1; case (diff_l n m); simpl castm."; pp " rewrite spec_extend_tr; auto."; pp " Qed."; - pp " Hint Rewrite spec_cast_r: extr."; pp ""; @@ -578,14 +565,14 @@ let _ = pr " | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1); done; if i == size then - pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size - else + pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size + else pr " | %s%i wx, %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1); done; for i = 0 to size do if i == size then - pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size - else + pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size + else pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1); done; pr " | %sn n wx, Nn m wy =>" c; @@ -611,17 +598,17 @@ let _ = done; if i == size then pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size - else + else pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; done; pp " intros n x y; case y; clear y."; for i = 0 to size do if i == size then pp " intros y; rewrite (spec_extend%in n); apply Pfnn." size - else + else pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; done; - pp " intros m y; rewrite <- (spec_cast_l n m x); "; + pp " intros m y; rewrite <- (spec_cast_l n m x);"; pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; pp " Qed."; pp ""; @@ -644,7 +631,7 @@ let _ = pr " match y with"; for j = 0 to i - 1 do pr " | %s%i wy =>" c j; - if j == 0 then + if j == 0 then pr " if w0_eq0 wy then ft0 x else"; pr " f%i wx (extend%i %i wy)" i j (i - j -1); done; @@ -653,8 +640,8 @@ let _ = pr " | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1); done; if i == size then - pr " | %sn m wy => fnn m (extend%i m wx) wy" c size - else + pr " | %sn m wy => fnn m (extend%i m wx) wy" c size + else pr " | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1); pr" end"; done; @@ -665,8 +652,8 @@ let _ = if i == 0 then pr " if w0_eq0 wy then ft0 x else"; if i == size then - pr " fnn n wx (extend%i n wy)" size - else + pr " fnn n wx (extend%i n wy)" size + else pr " fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1); done; pr " | %sn m wy =>" c; @@ -707,7 +694,7 @@ let _ = done; if i == size then pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size - else + else pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; done; pp " intros n x y; case y; clear y."; @@ -721,16 +708,16 @@ let _ = end; if i == size then pp " rewrite (spec_extend%in n); apply Pfnn." size - else + else pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; done; - pp " intros m y; rewrite <- (spec_cast_l n m x); "; + pp " intros m y; rewrite <- (spec_cast_l n m x);"; pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; pp " Qed."; pp ""; pr " (* We iter the smaller argument with the bigger *)"; - pr " Definition iter (x y: t_): res := "; + pr " Definition iter (x y: t_): res :="; pr0 " Eval lazy zeta beta iota delta ["; for i = 0 to size do pr0 "extend%i " i; @@ -748,14 +735,14 @@ let _ = pr " | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1); done; if i == size then - pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size - else + pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size + else pr " | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1); done; for i = 0 to size do if i == size then - pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size - else + pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size + else pr " | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1); done; pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c; @@ -765,6 +752,7 @@ let _ = pp " Ltac zg_tac := try"; pp " (red; simpl Zcompare; auto;"; pp " let t := fresh \"H\" in (intros t; discriminate t))."; + pp ""; pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y)."; pp " Proof."; pp " intros x; case x; clear x; unfold iter."; @@ -779,14 +767,14 @@ let _ = done; if i == size then pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size - else + else pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; done; pp " intros n x y; case y; clear y."; for i = 0 to size do if i == size then pp " intros y; rewrite spec_eval%in; apply Pfn%i." size size - else + else pp " intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; done; pp " intros m y; apply Pfnm."; @@ -820,8 +808,8 @@ let _ = pr " | %s%i wy => f%in %i wx wy" c j i (j - i - 1); done; if i == size then - pr " | %sn m wy => f%in m wx wy" c size - else + pr " | %sn m wy => f%in m wx wy" c size + else pr " | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1); pr " end"; done; @@ -832,8 +820,8 @@ let _ = if i == 0 then pr " if w0_eq0 wy then ft0 x else"; if i == size then - pr " fn%i n wx wy" size - else + pr " fn%i n wx wy" size + else pr " fn%i n wx (extend%i %i wy)" size i (size - i - 1); done; pr " | %sn m wy => fnm n m wx wy" c; @@ -869,7 +857,7 @@ let _ = done; if i == size then pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size - else + else pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; done; pp " intros n x y; case y; clear y."; @@ -883,7 +871,7 @@ let _ = end; if i == size then pp " rewrite spec_eval%in; apply Pfn%i." size size - else + else pp " rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; done; pp " intros m y; apply Pfnm."; @@ -897,27 +885,27 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Reduction *)"; + pr " (** * Reduction *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; - pr " Definition reduce_0 (x:w) := %s0 x." c; + pr " Definition reduce_0 (x:w) := %s0 x." c; pr " Definition reduce_1 :="; pr " Eval lazy beta iota delta[reduce_n1] in"; pr " reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c; for i = 2 to size do pr " Definition reduce_%i :=" i; pr " Eval lazy beta iota delta[reduce_n1] in"; - pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i." + pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i." (i-1) (i-1) c i done; pr " Definition reduce_%i :=" (size+1); pr " Eval lazy beta iota delta[reduce_n1] in"; - pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)." - size size c; + pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)." + size size c; - pr " Definition reduce_n n := "; + pr " Definition reduce_n n :="; pr " Eval lazy beta iota delta[reduce_n] in"; pr " reduce_n _ _ zero reduce_%i %sn n." (size + 1) c; pr ""; @@ -927,7 +915,7 @@ let _ = pp " intros x; unfold to_Z, reduce_0."; pp " auto."; pp " Qed."; - pp " "; + pp ""; for i = 1 to size + 1 do if i == size + 1 then @@ -938,14 +926,14 @@ let _ = pp " intros x; case x; unfold reduce_%i." i; pp " exact (spec_0 w0_spec)."; pp " intros x1 y1."; - pp " generalize (spec_w%i_eq0 x1); " (i - 1); + pp " generalize (spec_w%i_eq0 x1);" (i - 1); pp " case w%i_eq0; intros H1; auto." (i - 1); - if i <> 1 then + if i <> 1 then pp " rewrite spec_reduce_%i." (i - 1); pp " unfold to_Z; rewrite znz_to_Z_%i." i; pp " unfold to_Z in H1; rewrite H1; auto."; pp " Qed."; - pp " "; + pp ""; done; pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c; @@ -959,11 +947,11 @@ let _ = pp " rewrite Hrec."; pp " rewrite spec_extendn0_0; auto."; pp " Qed."; - pp " "; + pp ""; pr " (***************************************************************)"; pr " (* *)"; - pr " (* Successor *)"; + pr " (** * Successor *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -983,19 +971,19 @@ let _ = for i = 0 to size-1 do pr " | %s%i wx =>" c i; pr " match w%i_succ_c wx with" i; - pr " | C0 r => %s%i r" c i; + pr " | C0 r => %s%i r" c i; pr " | C1 r => %s%i (WW one%i r)" c (i+1) i; pr " end"; done; pr " | %s%i wx =>" c size; pr " match w%i_succ_c wx with" size; - pr " | C0 r => %s%i r" c size; + pr " | C0 r => %s%i r" c size; pr " | C1 r => %sn 0 (WW one%i r)" c size ; pr " end"; pr " | %sn n wx =>" c; pr " let op := make_op n in"; pr " match op.(znz_succ_c) wx with"; - pr " | C0 r => %sn n r" c; + pr " | C0 r => %sn n r" c; pr " | C1 r => %sn (S n) (WW op.(znz_1) r)" c; pr " end"; pr " end."; @@ -1027,13 +1015,13 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Adddition *)"; + pr " (** * Adddition *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; for i = 0 to size do - pr " Definition w%i_add_c := znz_add_c w%i_op." i i; + pr " Definition w%i_add_c := znz_add_c w%i_op." i i; pr " Definition w%i_add x y :=" i; pr " match w%i_add_c x y with" i; pr " | C0 r => %s%i r" c i; @@ -1057,26 +1045,24 @@ let _ = pp " Proof."; pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i; pp " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i; - pp " intros ww H; rewrite <- H."; + pp " intros ww H; rewrite <- H."; pp " rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1); pp " apply f_equal2 with (f := Zplus); auto;"; pp " apply f_equal2 with (f := Zmult); auto;"; pp " exact (spec_1 w%i_spec)." i; pp " Qed."; - pp " Hint Rewrite spec_w%i_add: addr." i; pp ""; done; pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c; pp " Proof."; pp " intros k n m; unfold to_Z, addn."; pp " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto."; - pp " intros ww H; rewrite <- H."; + pp " intros ww H; rewrite <- H."; pp " rewrite (znz_to_Z_n k); unfold interp_carry;"; pp " apply f_equal2 with (f := Zplus); auto;"; pp " apply f_equal2 with (f := Zmult); auto;"; pp " exact (spec_1 (wn_spec k))."; pp " Qed."; - pp " Hint Rewrite spec_wn_add: addr."; pr " Definition add := Eval lazy beta delta [same_level] in"; pr0 " (same_level t_ "; @@ -1101,7 +1087,7 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Predecessor *)"; + pr " (** * Predecessor *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1116,25 +1102,25 @@ let _ = for i = 0 to size do pr " | %s%i wx =>" c i; pr " match w%i_pred_c wx with" i; - pr " | C0 r => reduce_%i r" i; + pr " | C0 r => reduce_%i r" i; pr " | C1 r => zero"; pr " end"; done; pr " | %sn n wx =>" c; pr " let op := make_op n in"; pr " match op.(znz_pred_c) wx with"; - pr " | C0 r => reduce_n n r"; + pr " | C0 r => reduce_n n r"; pr " | C1 r => zero"; pr " end"; pr " end."; pr ""; - pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1."; + pr " Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1."; pa " Admitted."; pp " Proof."; pp " intros x; case x; unfold pred."; for i = 0 to size do - pp " intros x1 H1; unfold w%i_pred_c; " i; + pp " intros x1 H1; unfold w%i_pred_c;" i; pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; pp " rewrite spec_reduce_%i; auto." i; pp " unfold interp_carry; unfold to_Z."; @@ -1143,7 +1129,7 @@ let _ = pp " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith." i; pp " unfold to_Z in H1; auto with zarith."; done; - pp " intros n x1 H1; "; + pp " intros n x1 H1;"; pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; pp " rewrite spec_reduce_n; auto."; pp " unfold interp_carry; unfold to_Z."; @@ -1152,32 +1138,31 @@ let _ = pp " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith."; pp " unfold to_Z in H1; auto with zarith."; pp " Qed."; - pp " "; - + pp ""; + pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0."; pp " Proof."; pp " intros x; case x; unfold pred."; for i = 0 to size do - pp " intros x1 H1; unfold w%i_pred_c; " i; + pp " intros x1 H1; unfold w%i_pred_c;" i; pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; pp " unfold interp_carry; unfold to_Z."; pp " unfold to_Z in H1; auto with zarith."; pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith." i; pp " intros; exact (spec_0 w0_spec)."; done; - pp " intros n x1 H1; "; + pp " intros n x1 H1;"; pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; pp " unfold interp_carry; unfold to_Z."; pp " unfold to_Z in H1; auto with zarith."; pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith."; pp " intros; exact (spec_0 w0_spec)."; pp " Qed."; - pr " "; - + pr ""; pr " (***************************************************************)"; pr " (* *)"; - pr " (* Subtraction *)"; + pr " (** * Subtraction *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1187,7 +1172,7 @@ let _ = done; pr ""; - for i = 0 to size do + for i = 0 to size do pr " Definition w%i_sub x y :=" i; pr " match w%i_sub_c x y with" i; pr " | C0 r => reduce_%i r" i; @@ -1208,8 +1193,8 @@ let _ = pp " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y]." i c i c i i c i c i; pp " Proof."; pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; - pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i; - if i == 0 then + pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i; + if i == 0 then pp " intros x; auto." else pp " intros x; try rewrite spec_reduce_%i; auto." i; @@ -1219,11 +1204,11 @@ let _ = pp " Qed."; pp ""; done; - + pp " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y]." c c c c; pp " Proof."; pp " intros k n m; unfold subn."; - pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; "; + pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;"; pp " intros x; auto."; pp " unfold interp_carry, to_Z."; pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; @@ -1238,7 +1223,7 @@ let _ = pr "subn)."; pr ""; - pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; + pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; pa " Admitted."; pp " Proof."; pp " unfold sub."; @@ -1255,7 +1240,7 @@ let _ = pp " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0." i c i c i i; pp " Proof."; pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; - pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i; + pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i; pp " intros x; unfold interp_carry."; pp " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith." i; pp " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto."; @@ -1266,7 +1251,7 @@ let _ = pp " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0." c c; pp " Proof."; pp " intros k n m; unfold subn."; - pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; "; + pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;"; pp " intros x; unfold interp_carry."; pp " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; pp " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto."; @@ -1289,7 +1274,7 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Comparison *)"; + pr " (** * Comparison *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1299,7 +1284,7 @@ let _ = pr " Definition comparen_%i :=" i; pr " compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i done; - pr ""; + pr ""; pr " Definition comparenm n m wx wy :="; pr " let mn := Max.max n m in"; @@ -1310,8 +1295,8 @@ let _ = pr " (castm (diff_l n m) (extend_tr wy (fst d)))."; pr ""; - pr " Definition compare := Eval lazy beta delta [iter] in "; - pr " (iter _ "; + pr " Definition compare := Eval lazy beta delta [iter] in"; + pr " (iter _"; for i = 0 to size do pr " compare_%i" i; pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; @@ -1320,15 +1305,9 @@ let _ = pr " comparenm)."; pr ""; - pr " Definition lt n m := compare n m = Lt."; - pr " Definition le n m := compare n m <> Gt."; - pr " Definition min n m := match compare n m with Gt => m | _ => n end."; - pr " Definition max n m := match compare n m with Lt => m | _ => n end."; - pr ""; - for i = 0 to size do pp " Let spec_compare_%i: forall x y," i; - pp " match compare_%i x y with " i; + pp " match compare_%i x y with" i; pp " Eq => [%s%i x] = [%s%i y]" c i c i; pp " | Lt => [%s%i x] < [%s%i y]" c i c i; pp " | Gt => [%s%i x] > [%s%i y]" c i c i; @@ -1337,7 +1316,7 @@ let _ = pp " unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i; pp " Qed."; pp ""; - + pp " Let spec_comparen_%i:" i; pp " forall (n : nat) (x : word w%i n) (y : w%i)," i i; pp " match comparen_%i n x y with" i; @@ -1367,16 +1346,16 @@ let _ = pp ""; - pr " Theorem spec_compare: forall x y,"; - pr " match compare x y with "; + pr " Theorem spec_compare_aux: forall x y,"; + pr " match compare x y with"; pr " Eq => [x] = [y]"; pr " | Lt => [x] < [y]"; pr " | Gt => [x] > [y]"; pr " end."; pa " Admitted."; pp " Proof."; - pp " refine (spec_iter _ (fun x y res => "; - pp " match res with "; + pp " refine (spec_iter _ (fun x y res =>"; + pp " match res with"; pp " Eq => x = y"; pp " | Lt => x < y"; pp " | Gt => x > y"; @@ -1387,12 +1366,12 @@ let _ = pp " (fun n => comparen_%i (S n)) _ _ _" i; done; pp " comparenm _)."; - + for i = 0 to size - 1 do pp " exact spec_compare_%i." i; pp " intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i; pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i; - done; + done; pp " exact spec_compare_%i." size; pp " intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size; pp " intros n; exact (spec_comparen_%i (S n))." size; @@ -1402,28 +1381,9 @@ let _ = pp " Qed."; pr ""; - pr " Definition eq_bool x y :="; - pr " match compare x y with"; - pr " | Eq => true"; - pr " | _ => false"; - pr " end."; - pr ""; - - - pr " Theorem spec_eq_bool: forall x y,"; - pr " if eq_bool x y then [x] = [y] else [x] <> [y]."; - pa " Admitted."; - pp " Proof."; - pp " intros x y; unfold eq_bool."; - pp " generalize (spec_compare x y); case compare; auto with zarith."; - pp " Qed."; - pr ""; - - - pr " (***************************************************************)"; pr " (* *)"; - pr " (* Multiplication *)"; + pr " (** * Multiplication *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1461,7 +1421,7 @@ let _ = pr " match n return word w%i (S n) -> t_ with" i; for j = 0 to size - i do if (i + j) == size then - begin + begin pr " | %i%s => fun x => %sn 0 x" j "%nat" c; pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c end @@ -1471,7 +1431,7 @@ let _ = pr " | _ => fun _ => N0 w_0"; pr " end."; pr ""; - done; + done; for i = 0 to size - 1 do @@ -1486,7 +1446,7 @@ let _ = pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith."; pp " Qed."; pp ""; - done; + done; for i = 0 to size do @@ -1497,8 +1457,8 @@ let _ = pr " if w%i_eq0 w then %sn n r" i c; pr " else %sn (S n) (WW (extend%i n w) r)." c i; end - else - begin + else + begin pr " if w%i_eq0 w then to_Z%i n r" i i; pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i; end; @@ -1514,10 +1474,10 @@ let _ = pr " (castm (diff_l n m) (extend_tr y (fst d))))."; pr ""; - pr " Definition mul := Eval lazy beta delta [iter0] in "; - pr " (iter0 t_ "; + pr " Definition mul := Eval lazy beta delta [iter0] in"; + pr " (iter0 t_"; for i = 0 to size do - pr " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i; + pr " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i; pr " (fun n x y => w%i_mul n y x)" i; pr " w%i_mul" i; done; @@ -1556,7 +1516,7 @@ let _ = pp " Qed."; pp ""; done; - + pp " Lemma nmake_op_WW: forall ww ww1 n x y,"; pp " znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) ="; pp " znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +"; @@ -1564,21 +1524,21 @@ let _ = pp " auto."; pp " Qed."; pp ""; - + for i = 0 to size do pp " Lemma extend%in_spec: forall n x1," i; - pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i; + pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i; pp " znz_to_Z w%i_op x1." i; pp " Proof."; pp " intros n1 x2; rewrite nmake_double."; pp " unfold extend%i." i; pp " rewrite DoubleBase.spec_extend; auto."; - if i == 0 then + if i == 0 then pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring."; pp " Qed."; pp ""; done; - + pp " Lemma spec_muln:"; pp " forall n (x: word _ (S n)) y,"; pp " [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c; @@ -1588,12 +1548,13 @@ let _ = pp " rewrite make_op_S."; pp " case znz_mul_c; auto."; pp " Qed."; + pr ""; pr " Theorem spec_mul: forall x y, [mul x y] = [x] * [y]."; pa " Admitted."; pp " Proof."; for i = 0 to size do - pp " assert(F%i: " i; + pp " assert(F%i:" i; pp " forall n x y,"; if i <> size then pp0 " Z_of_nat n <= %i -> " (size - i); @@ -1614,7 +1575,7 @@ let _ = pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i; pp " unfold to_Z in HH; rewrite HH."; if i == size then - begin + begin pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i; pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i end @@ -1627,7 +1588,7 @@ let _ = done; pp " refine (spec_iter0 t_ (fun x y res => [res] = x * y)"; for i = 0 to size do - pp " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i; + pp " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i; pp " (fun n x y => w%i_mul n y x)" i; pp " w%i_mul _ _ _" i; done; @@ -1643,12 +1604,12 @@ let _ = if i == size then begin pp " intros n x y; rewrite F%i; auto with zarith." i; - pp " intros n x y; rewrite F%i; auto with zarith. " i; + pp " intros n x y; rewrite F%i; auto with zarith." i; end else begin pp " intros n x y H; rewrite F%i; auto with zarith." i; - pp " intros n x y H; rewrite F%i; auto with zarith. " i; + pp " intros n x y H; rewrite F%i; auto with zarith." i; end; done; pp " intros n m x y; unfold mulnm."; @@ -1663,7 +1624,7 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Square *)"; + pr " (** * Square *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1702,42 +1663,9 @@ let _ = pp "Qed."; pr ""; - pr " (***************************************************************)"; pr " (* *)"; - pr " (* Power *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - pr " Fixpoint power_pos (x:%s) (p:positive) {struct p} : %s :=" t t; - pr " match p with"; - pr " | xH => x"; - pr " | xO p => square (power_pos x p)"; - pr " | xI p => mul (square (power_pos x p)) x"; - pr " end."; - pr ""; - - pr " Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n."; - pa " Admitted."; - pp " Proof."; - pp " intros x n; generalize x; elim n; clear n x; simpl power_pos."; - pp " intros; rewrite spec_mul; rewrite spec_square; rewrite H."; - pp " rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith."; - pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith."; - pp " rewrite Zpower_2; rewrite Zpower_1_r; auto."; - pp " intros; rewrite spec_square; rewrite H."; - pp " rewrite Zpos_xO; auto with zarith."; - pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith."; - pp " rewrite Zpower_2; auto."; - pp " intros; rewrite Zpower_1_r; auto."; - pp " Qed."; - pp ""; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (* Square root *)"; + pr " (** * Square root *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; @@ -1772,26 +1700,26 @@ let _ = pr " (***************************************************************)"; pr " (* *)"; - pr " (* Division *)"; + pr " (** * Division *)"; pr " (* *)"; pr " (***************************************************************)"; - pr ""; + pr ""; for i = 0 to size do pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i done; pr ""; - pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; - pp " (spec_double_divn1 "; + pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :="; + pp " (spec_double_divn1"; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; pp " (znz_WW ww_op) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; - pp " (spec_to_Z ww_spec) "; + pp " (spec_to_Z ww_spec)"; pp " (spec_zdigits ww_spec)"; pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; - pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; + pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)"; pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; pp ""; @@ -1811,7 +1739,7 @@ let _ = for i = 0 to size do pp " Lemma spec_get_end%i: forall n x y," i; - pp " eval%in n x <= [%s%i y] -> " i c i; + pp " eval%in n x <= [%s%i y] ->" i c i; pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i; pp " Proof."; pp " intros n x y H."; @@ -1843,8 +1771,8 @@ let _ = pr ""; pr " Definition div_gt := Eval lazy beta delta [iter] in"; - pr " (iter _ "; - for i = 0 to size do + pr " (iter _"; + for i = 0 to size do pr " div_gt%i" i; pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); pr " w%i_divn1" i; @@ -1862,10 +1790,10 @@ let _ = pp " forall x y, [x] > [y] -> 0 < [y] ->"; pp " let (q,r) := div_gt x y in"; pp " [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y])."; - pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->"; + pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->"; pp " let (q,r) := res in"; pp " x = [q] * y + [r] /\\ 0 <= [r] < y)"; - for i = 0 to size do + for i = 0 to size do pp " div_gt%i" i; pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); pp " w%i_divn1 _ _ _" i; @@ -1879,11 +1807,11 @@ let _ = pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i else pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i; - pp " generalize (spec_div_gt w%i_spec x " i; + pp " generalize (spec_div_gt w%i_spec x" i; pp " (DoubleBase.get_low %s (S n) y))." (pz i); - pp0 " "; + pp0 ""; for j = 0 to i do - pp0 "unfold w%i; " (i-j); + pp0 "unfold w%i; " (i-j); done; pp "case znz_div_gt."; pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i; @@ -1897,7 +1825,7 @@ let _ = pp " (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i; pp0 " unfold w%i_divn1; " i; for j = 0 to i do - pp0 "unfold w%i; " (i-j); + pp0 "unfold w%i; " (i-j); done; pp "case double_divn1."; pp " intros xx yy H4."; @@ -1936,61 +1864,12 @@ let _ = pp " Qed."; pr ""; - pr " Definition div_eucl x y :="; - pr " match compare x y with"; - pr " | Eq => (one, zero)"; - pr " | Lt => (zero, x)"; - pr " | Gt => div_gt x y"; - pr " end."; - pr ""; - - pr " Theorem spec_div_eucl: forall x y,"; - pr " 0 < [y] ->"; - pr " let (q,r) := div_eucl x y in"; - pr " ([q], [r]) = Zdiv_eucl [x] [y]."; - pa " Admitted."; - pp " Proof."; - pp " assert (F0: [zero] = 0)."; - pp " exact (spec_0 w0_spec)."; - pp " assert (F1: [one] = 1)."; - pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold div_eucl; case compare; try rewrite F0;"; - pp " try rewrite F1; intros; auto with zarith."; - pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))"; - pp " (Z_mod_same [y] (Zlt_gt _ _ H));"; - pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto."; - pp " assert (F2: 0 <= [x] < [y])."; - pp " generalize (spec_pos x); auto."; - pp " generalize (Zdiv_small _ _ F2)"; - pp " (Zmod_small _ _ F2);"; - pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto."; - pp " generalize (spec_div_gt _ _ H0 H); auto."; - pp " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt."; - pp " intros a b c d (H1, H2); subst; auto."; - pp " Qed."; - pr ""; - - pr " Definition div x y := fst (div_eucl x y)."; - pr ""; - - pr " Theorem spec_div:"; - pr " forall x y, 0 < [y] -> [div x y] = [x] / [y]."; - pa " Admitted."; - pp " Proof."; - pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);"; - pp " case div_eucl; simpl fst."; - pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; "; - pp " injection H; auto."; - pp " Qed."; - pr ""; - pr " (***************************************************************)"; pr " (* *)"; - pr " (* Modulo *)"; + pr " (** * Modulo *)"; pr " (* *)"; pr " (***************************************************************)"; - pr ""; + pr ""; for i = 0 to size do pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i @@ -2015,7 +1894,7 @@ let _ = pr ""; pr " Definition mod_gt := Eval lazy beta delta[iter] in"; - pr " (iter _ "; + pr " (iter _"; for i = 0 to size do pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); @@ -2024,16 +1903,16 @@ let _ = pr " mod_gtnm)."; pr ""; - pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; - pp " (spec_double_modn1 "; + pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :="; + pp " (spec_double_modn1"; pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; pp " (znz_WW ww_op) ww_op.(znz_head0)"; pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; - pp " (spec_to_Z ww_spec) "; + pp " (spec_to_Z ww_spec)"; pp " (spec_zdigits ww_spec)"; pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; - pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; + pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)"; pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; pp ""; @@ -2063,7 +1942,7 @@ let _ = pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i; if i == size then pp " intros n x y H2 H3; rewrite spec_reduce_%i." i - else + else pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i; pp " apply (spec_modn1 _ _ w%i_spec); auto." i; @@ -2079,39 +1958,9 @@ let _ = pp " Qed."; pr ""; - pr " Definition modulo x y := "; - pr " match compare x y with"; - pr " | Eq => zero"; - pr " | Lt => x"; - pr " | Gt => mod_gt x y"; - pr " end."; + pr " (** digits: a measure for gcd *)"; pr ""; - pr " Theorem spec_modulo:"; - pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]."; - pa " Admitted."; - pp " Proof."; - pp " assert (F0: [zero] = 0)."; - pp " exact (spec_0 w0_spec)."; - pp " assert (F1: [one] = 1)."; - pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold modulo; case compare; try rewrite F0;"; - pp " try rewrite F1; intros; try split; auto with zarith."; - pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith."; - pp " apply sym_equal; apply Zmod_small; auto with zarith."; - pp " generalize (spec_pos x); auto with zarith."; - pp " apply spec_mod_gt; auto."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (* Gcd *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - pr " Definition digits x :="; pr " match x with"; for i = 0 to size do @@ -2134,189 +1983,18 @@ let _ = pp " Qed."; pr ""; - pr " Definition gcd_gt_body a b cont :="; - pr " match compare b zero with"; - pr " | Gt =>"; - pr " let r := mod_gt a b in"; - pr " match compare r zero with"; - pr " | Gt => cont r (mod_gt b r)"; - pr " | _ => b"; - pr " end"; - pr " | _ => a"; - pr " end."; - pr ""; - - pp " Theorem Zspec_gcd_gt_body: forall a b cont p,"; - pp " [a] > [b] -> [a] < 2 ^ p ->"; - pp " (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->"; - pp " Zis_gcd [a1] [b1] [cont a1 b1]) -> "; - pp " Zis_gcd [a] [b] [gcd_gt_body a b cont]."; - pp " Proof."; - pp " assert (F1: [zero] = 0)."; - pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto."; - pp " intros a b cont p H2 H3 H4; unfold gcd_gt_body."; - pp " generalize (spec_compare b zero); case compare; try rewrite F1."; - pp " intros HH; rewrite HH; apply Zis_gcd_0."; - pp " intros HH; absurd (0 <= [b]); auto with zarith."; - pp " case (spec_digits b); auto with zarith."; - pp " intros H5; generalize (spec_compare (mod_gt a b) zero); "; - pp " case compare; try rewrite F1."; - pp " intros H6; rewrite <- (Zmult_1_r [b])."; - pp " rewrite (Z_div_mod_eq [a] [b]); auto with zarith."; - pp " rewrite <- spec_mod_gt; auto with zarith."; - pp " rewrite H6; rewrite Zplus_0_r."; - pp " apply Zis_gcd_mult; apply Zis_gcd_1."; - pp " intros; apply False_ind."; - pp " case (spec_digits (mod_gt a b)); auto with zarith."; - pp " intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith."; - pp " apply DoubleDiv.Zis_gcd_mod; auto with zarith."; - pp " rewrite <- spec_mod_gt; auto with zarith."; - pp " assert (F2: [b] > [mod_gt a b])."; - pp " case (Z_mod_lt [a] [b]); auto with zarith."; - pp " repeat rewrite <- spec_mod_gt; auto with zarith."; - pp " assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)])."; - pp " case (Z_mod_lt [b] [mod_gt a b]); auto with zarith."; - pp " rewrite <- spec_mod_gt; auto with zarith."; - pp " repeat rewrite <- spec_mod_gt; auto with zarith."; - pp " apply H4; auto with zarith."; - pp " apply Zmult_lt_reg_r with 2; auto with zarith."; - pp " apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith."; - pp " apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith."; - pp " apply Zplus_le_compat_r."; - pp " pattern [b] at 1; rewrite <- (Zmult_1_l [b])."; - pp " apply Zmult_le_compat_r; auto with zarith."; - pp " case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith."; - pp " intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2;"; - pp " try rewrite <- HH in H2; auto with zarith."; - pp " case (Z_mod_lt [a] [b]); auto with zarith."; - pp " rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith."; - pp " rewrite <- Z_div_mod_eq; auto with zarith."; - pp " pattern 2 at 2; rewrite <- (Zpower_1_r 2)."; - pp " rewrite <- Zpower_exp; auto with zarith."; - pp " ring_simplify (p - 1 + 1); auto."; - pp " case (Zle_lt_or_eq 0 p); auto with zarith."; - pp " generalize H3; case p; simpl Zpower; auto with zarith."; - pp " intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith."; - pp " Qed."; - pp ""; - - pr " Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :="; - pr " gcd_gt_body a b"; - pr " (fun a b =>"; - pr " match p with"; - pr " | xH => cont a b"; - pr " | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b"; - pr " | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b"; - pr " end)."; - pr ""; - - pp " Theorem Zspec_gcd_gt_aux: forall p n a b cont,"; - pp " [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->"; - pp " (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->"; - pp " Zis_gcd [a1] [b1] [cont a1 b1]) ->"; - pp " Zis_gcd [a] [b] [gcd_gt_aux p cont a b]."; - pp " intros p; elim p; clear p."; - pp " intros p Hrec n a b cont H2 H3 H4."; - pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto."; - pp " intros a1 b1 H6 H7."; - pp " apply Hrec with (Zpos p + n); auto."; - pp " replace (Zpos p + (Zpos p + n)) with"; - pp " (Zpos (xI p) + n - 1); auto."; - pp " rewrite Zpos_xI; ring."; - pp " intros a2 b2 H9 H10."; - pp " apply Hrec with n; auto."; - pp " intros p Hrec n a b cont H2 H3 H4."; - pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto."; - pp " intros a1 b1 H6 H7."; - pp " apply Hrec with (Zpos p + n - 1); auto."; - pp " replace (Zpos p + (Zpos p + n - 1)) with"; - pp " (Zpos (xO p) + n - 1); auto."; - pp " rewrite Zpos_xO; ring."; - pp " intros a2 b2 H9 H10."; - pp " apply Hrec with (n - 1); auto."; - pp " replace (Zpos p + (n - 1)) with"; - pp " (Zpos p + n - 1); auto with zarith."; - pp " intros a3 b3 H12 H13; apply H4; auto with zarith."; - pp " apply Zlt_le_trans with (1 := H12)."; - pp " case (Zle_or_lt 1 n); intros HH."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " apply Zle_trans with 0; auto with zarith."; - pp " assert (HH1: n - 1 < 0); auto with zarith."; - pp " generalize HH1; case (n - 1); auto with zarith."; - pp " intros p1 HH2; discriminate."; - pp " intros n a b cont H H2 H3."; - pp " simpl gcd_gt_aux."; - pp " apply Zspec_gcd_gt_body with (n + 1); auto with zarith."; - pp " rewrite Zplus_comm; auto."; - pp " intros a1 b1 H5 H6; apply H3; auto."; - pp " replace n with (n + 1 - 1); auto; try ring."; - pp " Qed."; - pp ""; - - pr " Definition gcd_cont a b :="; - pr " match compare one b with"; - pr " | Eq => one"; - pr " | _ => a"; - pr " end."; - pr ""; - - pr " Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b."; - pr ""; - - pr " Theorem spec_gcd_gt: forall a b,"; - pr " [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b]."; - pa " Admitted."; - pp " Proof."; - pp " intros a b H2."; - pp " case (spec_digits (gcd_gt a b)); intros H3 H4."; - pp " case (spec_digits a); intros H5 H6."; - pp " apply sym_equal; apply Zis_gcd_gcd; auto with zarith."; - pp " unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith."; - pp " intros a1 a2; rewrite Zpower_0_r."; - pp " case (spec_digits a2); intros H7 H8;"; - pp " intros; apply False_ind; auto with zarith."; - pp " Qed."; - pr ""; - - pr " Definition gcd a b :="; - pr " match compare a b with"; - pr " | Eq => a"; - pr " | Lt => gcd_gt b a"; - pr " | Gt => gcd_gt a b"; - pr " end."; - pr ""; - - pr " Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]."; - pa " Admitted."; - pp " Proof."; - pp " intros a b."; - pp " case (spec_digits a); intros H1 H2."; - pp " case (spec_digits b); intros H3 H4."; - pp " unfold gcd; generalize (spec_compare a b); case compare."; - pp " intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto."; - pp " apply Zis_gcd_refl."; - pp " intros; apply trans_equal with (Zgcd [b] [a])."; - pp " apply spec_gcd_gt; auto with zarith."; - pp " apply Zis_gcd_gcd; auto with zarith."; - pp " apply Zgcd_is_pos."; - pp " apply Zis_gcd_sym; apply Zgcd_is_gcd."; - pp " intros; apply spec_gcd_gt; auto."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; pr " (* *)"; - pr " (* Conversion *)"; + pr " (** * Conversion *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; - pr " Definition pheight p := "; + pr " Definition pheight p :="; pr " Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p)))."; pr ""; - pr " Theorem pheight_correct: forall p, "; + pr " Theorem pheight_correct: forall p,"; pr " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p)))."; pr " Proof."; pr " intros p; unfold pheight."; @@ -2400,30 +2078,12 @@ let _ = pp " Qed."; pr ""; - pr " Definition of_N x :="; - pr " match x with"; - pr " | BinNat.N0 => zero"; - pr " | Npos p => of_pos p"; - pr " end."; - pr ""; - - pr " Theorem spec_of_N: forall x,"; - pr " [of_N x] = Z_of_N x."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x."; - pp " simpl of_N."; - pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto."; - pp " intros p; exact (spec_of_pos p)."; - pp " Qed."; - pr ""; - pr " (***************************************************************)"; pr " (* *)"; - pr " (* Shift *)"; + pr " (** * Shift *)"; pr " (* *)"; pr " (***************************************************************)"; - pr ""; + pr ""; (* Head0 *) pr " Definition head0 w := match w with"; @@ -2443,21 +2103,21 @@ let _ = done; pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x)."; pp " Qed."; - pr " "; + pr ""; pr " Theorem spec_head0: forall x, 0 < [x] ->"; pr " 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x)."; pa " Admitted."; pp " Proof."; pp " assert (F0: forall x, (x - 1) + 1 = x)."; - pp " intros; ring. "; + pp " intros; ring."; pp " intros x; case x; unfold digits, head0; clear x."; for i = 0 to size do pp " intros x Hx; rewrite spec_reduce_%i." i; pp " assert (F1:= spec_more_than_1_digit w%i_spec)." i; pp " generalize (spec_head0 w%i_spec x Hx)." i; pp " unfold base."; - pp " pattern (Zpos (znz_digits w%i_op)) at 1; " i; + pp " pattern (Zpos (znz_digits w%i_op)) at 1;" i; pp " rewrite <- (fun x => (F0 (Zpos x)))."; pp " rewrite Zpower_exp; auto with zarith."; pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; @@ -2466,7 +2126,7 @@ let _ = pp " assert (F1:= spec_more_than_1_digit (wn_spec n))."; pp " generalize (spec_head0 (wn_spec n) x Hx)."; pp " unfold base."; - pp " pattern (Zpos (znz_digits (make_op n))) at 1; "; + pp " pattern (Zpos (znz_digits (make_op n))) at 1;"; pp " rewrite <- (fun x => (F0 (Zpos x)))."; pp " rewrite Zpower_exp; auto with zarith."; pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; @@ -2493,7 +2153,7 @@ let _ = done; pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x)."; pp " Qed."; - pr " "; + pr ""; pr " Theorem spec_tail0: forall x,"; @@ -2513,7 +2173,7 @@ let _ = pr " Definition %sdigits x :=" c; pr " match x with"; pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c; - for i = 1 to size do + for i = 1 to size do pr " | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i; done; pr " | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c; @@ -2534,22 +2194,22 @@ let _ = (* Shiftr *) for i = 0 to size do - pr " Definition shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i; + pr " Definition unsafe_shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i; done; - pr " Definition shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x."; + pr " Definition unsafe_shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x."; pr ""; - pr " Definition shiftr := Eval lazy beta delta [same_level] in "; - pr " same_level _ (fun n x => %s0 (shiftr0 n x))" c; + pr " Definition unsafe_shiftr := Eval lazy beta delta [same_level] in"; + pr " same_level _ (fun n x => %s0 (unsafe_shiftr0 n x))" c; for i = 1 to size do - pr " (fun n x => reduce_%i (shiftr%i n x))" i i; + pr " (fun n x => reduce_%i (unsafe_shiftr%i n x))" i i; done; - pr " (fun n p x => reduce_n n (shiftrn n p x))."; + pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x))."; pr ""; - pr " Theorem spec_shiftr: forall n x,"; - pr " [n] <= [Ndigits x] -> [shiftr n x] = [x] / 2 ^ [n]."; + pr " Theorem spec_unsafe_shiftr: forall n x,"; + pr " [n] <= [Ndigits x] -> [unsafe_shiftr n x] = [x] / 2 ^ [n]."; pa " Admitted."; pp " Proof."; pp " assert (F0: forall x y, x - (x - y) = y)."; @@ -2568,7 +2228,7 @@ let _ = pp " split; auto with zarith."; pp " apply Zle_lt_trans with xx; auto with zarith."; pp " apply Zpower2_lt_lin; auto with zarith."; - pp " assert (F4: forall ww ww1 ww2 "; + pp " assert (F4: forall ww ww1 ww2"; pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; pp " xx yy xx1 yy1,"; pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_zdigits ww1_op) ->"; @@ -2586,7 +2246,7 @@ let _ = pp " rewrite <- Hy."; pp " generalize (spec_add_mul_div Hw"; pp " (znz_0 ww_op) xx1"; - pp " (znz_sub ww_op (znz_zdigits ww_op) "; + pp " (znz_sub ww_op (znz_zdigits ww_op)"; pp " yy1)"; pp " )."; pp " rewrite (spec_0 Hw)."; @@ -2612,11 +2272,11 @@ let _ = pp " rewrite Zpos_xO."; pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; pp " apply F5; auto with arith."; - pp " intros x; case x; clear x; unfold shiftr, same_level."; + pp " intros x; case x; clear x; unfold unsafe_shiftr, same_level."; for i = 0 to size do pp " intros x y; case y; clear y."; for j = 0 to i - 1 do - pp " intros y; unfold shiftr%i, Ndigits." i; + pp " intros y; unfold unsafe_shiftr%i, Ndigits." i; pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; pp " rewrite (spec_zdigits w%i_spec)." i; @@ -2628,25 +2288,25 @@ let _ = pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; done; - pp " intros y; unfold shiftr%i, Ndigits." i; + pp " intros y; unfold unsafe_shiftr%i, Ndigits." i; pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; for j = i + 1 to size do - pp " intros y; unfold shiftr%i, Ndigits." j; + pp " intros y; unfold unsafe_shiftr%i, Ndigits." j; pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; done; if i == size then begin - pp " intros m y; unfold shiftrn, Ndigits."; + pp " intros m y; unfold unsafe_shiftrn, Ndigits."; pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; pp " try (apply sym_equal; exact (spec_extend%in m x))." size; end - else + else begin - pp " intros m y; unfold shiftrn, Ndigits."; + pp " intros m y; unfold unsafe_shiftrn, Ndigits."; pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; @@ -2654,7 +2314,7 @@ let _ = end done; pp " intros n x y; case y; clear y;"; - pp " intros y; unfold shiftrn, Ndigits; try rewrite spec_reduce_n."; + pp " intros y; unfold unsafe_shiftrn, Ndigits; try rewrite spec_reduce_n."; for i = 0 to size do pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; @@ -2684,52 +2344,23 @@ let _ = pp " Qed."; pr ""; - pr " Definition safe_shiftr n x := "; - pr " match compare n (Ndigits x) with"; - pr " | Lt => shiftr n x "; - pr " | _ => %s0 w_0" c; - pr " end."; - pr ""; - - - pr " Theorem spec_safe_shiftr: forall n x,"; - pr " [safe_shiftr n x] = [x] / 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " intros n x; unfold safe_shiftr;"; - pp " generalize (spec_compare n (Ndigits x)); case compare; intros H."; - pp " apply trans_equal with (1 := spec_0 w0_spec)."; - pp " apply sym_equal; apply Zdiv_small; rewrite H."; - pp " rewrite spec_Ndigits; exact (spec_digits x)."; - pp " rewrite <- spec_shiftr; auto with zarith."; - pp " apply trans_equal with (1 := spec_0 w0_spec)."; - pp " apply sym_equal; apply Zdiv_small."; - pp " rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2."; - pp " split; auto."; - pp " apply Zlt_le_trans with (1 := H2)."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " Qed."; - pr ""; - - pr ""; - - (* Shiftl *) + (* Unsafe_Shiftl *) for i = 0 to size do - pr " Definition shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i + pr " Definition unsafe_shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i done; - pr " Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0)."; - pr " Definition shiftl := Eval lazy beta delta [same_level] in"; - pr " same_level _ (fun n x => %s0 (shiftl0 n x))" c; + pr " Definition unsafe_shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0)."; + pr " Definition unsafe_shiftl := Eval lazy beta delta [same_level] in"; + pr " same_level _ (fun n x => %s0 (unsafe_shiftl0 n x))" c; for i = 1 to size do - pr " (fun n x => reduce_%i (shiftl%i n x))" i i; + pr " (fun n x => reduce_%i (unsafe_shiftl%i n x))" i i; done; - pr " (fun n p x => reduce_n n (shiftln n p x))."; + pr " (fun n p x => reduce_n n (unsafe_shiftln n p x))."; pr ""; pr ""; - pr " Theorem spec_shiftl: forall n x,"; - pr " [n] <= [head0 x] -> [shiftl n x] = [x] * 2 ^ [n]."; + pr " Theorem spec_unsafe_shiftl: forall n x,"; + pr " [n] <= [head0 x] -> [unsafe_shiftl n x] = [x] * 2 ^ [n]."; pa " Admitted."; pp " Proof."; pp " assert (F0: forall x y, x - (x - y) = y)."; @@ -2748,7 +2379,7 @@ let _ = pp " split; auto with zarith."; pp " apply Zle_lt_trans with xx; auto with zarith."; pp " apply Zpower2_lt_lin; auto with zarith."; - pp " assert (F4: forall ww ww1 ww2 "; + pp " assert (F4: forall ww ww1 ww2"; pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; pp " xx yy xx1 yy1,"; pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->"; @@ -2788,7 +2419,7 @@ let _ = pp " rewrite Zmod_small; auto with zarith."; pp " intros HH; apply HH."; pp " rewrite Hy; apply Zle_trans with (1:= Hl)."; - pp " rewrite <- (spec_zdigits Hw). "; + pp " rewrite <- (spec_zdigits Hw)."; pp " apply Zle_trans with (2 := Hl1); auto."; pp " rewrite (spec_zdigits Hw1); auto with zarith."; pp " split; auto with zarith ."; @@ -2826,11 +2457,11 @@ let _ = pp " rewrite Zpos_xO."; pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; pp " apply F5; auto with arith."; - pp " intros x; case x; clear x; unfold shiftl, same_level."; + pp " intros x; case x; clear x; unfold unsafe_shiftl, same_level."; for i = 0 to size do pp " intros x y; case y; clear y."; for j = 0 to i - 1 do - pp " intros y; unfold shiftl%i, head0." i; + pp " intros y; unfold unsafe_shiftl%i, head0." i; pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; pp " rewrite (spec_zdigits w%i_spec)." i; @@ -2841,25 +2472,25 @@ let _ = pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; done; - pp " intros y; unfold shiftl%i, head0." i; + pp " intros y; unfold unsafe_shiftl%i, head0." i; pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; for j = i + 1 to size do - pp " intros y; unfold shiftl%i, head0." j; + pp " intros y; unfold unsafe_shiftl%i, head0." j; pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; done; if i == size then begin - pp " intros m y; unfold shiftln, head0."; + pp " intros m y; unfold unsafe_shiftln, head0."; pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; pp " try (apply sym_equal; exact (spec_extend%in m x))." size; end - else + else begin - pp " intros m y; unfold shiftln, head0."; + pp " intros m y; unfold unsafe_shiftln, head0."; pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; @@ -2867,7 +2498,7 @@ let _ = end done; pp " intros n x y; case y; clear y;"; - pp " intros y; unfold shiftln, head0; try rewrite spec_reduce_n."; + pp " intros y; unfold unsafe_shiftln, head0; try rewrite spec_reduce_n."; for i = 0 to size do pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; @@ -2907,7 +2538,7 @@ let _ = pr " end."; pr ""; - pr " Theorem spec_double_size_digits: "; + pr " Theorem spec_double_size_digits:"; pr " forall x, digits (double_size x) = xO (digits x)."; pa " Admitted."; pp " Proof."; @@ -2922,7 +2553,7 @@ let _ = pp " Proof."; pp " intros x; case x; unfold double_size; clear x."; for i = 0 to size do - pp " intros x; unfold to_Z, make_op; "; + pp " intros x; unfold to_Z, make_op;"; pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto with zarith." (i + 1) i; done; pp " intros n x; unfold to_Z;"; @@ -2934,7 +2565,7 @@ let _ = pr ""; - pr " Theorem spec_double_size_head0: "; + pr " Theorem spec_double_size_head0:"; pr " forall x, 2 * [head0 x] <= [head0 (double_size x)]."; pa " Admitted."; pp " Proof."; @@ -2963,7 +2594,7 @@ let _ = pp " apply Zmult_le_compat_l; auto with zarith."; pp " rewrite Zpower_1_r; auto with zarith."; pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith. "; + pp " split; auto with zarith."; pp " case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6."; pp " absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith."; pp " rewrite <- HH5; rewrite Zmult_1_r."; @@ -2988,7 +2619,7 @@ let _ = pp " Qed."; pr ""; - pr " Theorem spec_double_size_head0_pos: "; + pr " Theorem spec_double_size_head0_pos:"; pr " forall x, 0 < [head0 (double_size x)]."; pa " Admitted."; pp " Proof."; @@ -3015,114 +2646,6 @@ let _ = pp " Qed."; pr ""; - - (* Safe shiftl *) - - pr " Definition safe_shiftl_aux_body cont n x :="; - pr " match compare n (head0 x) with"; - pr " Gt => cont n (double_size x)"; - pr " | _ => shiftl n x"; - pr " end."; - pr ""; - - pr " Theorem spec_safe_shift_aux_body: forall n p x cont,"; - pr " 2^ Zpos p <= [head0 x] ->"; - pr " (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->"; - pr " [cont n x] = [x] * 2 ^ [n]) ->"; - pr " [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body."; - pp " generalize (spec_compare n (head0 x)); case compare; intros H."; - pp " apply spec_shiftl; auto with zarith."; - pp " apply spec_shiftl; auto with zarith."; - pp " rewrite H2."; - pp " rewrite spec_double_size; auto."; - pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith."; - pp " apply Zle_trans with (2 := spec_double_size_head0 x)."; - pp " rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith."; - pp " Qed."; - pr ""; - - pr " Fixpoint safe_shiftl_aux p cont n x {struct p} :="; - pr " safe_shiftl_aux_body "; - pr " (fun n x => match p with"; - pr " | xH => cont n x"; - pr " | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x"; - pr " | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x"; - pr " end) n x."; - pr ""; - - pr " Theorem spec_safe_shift_aux: forall p q n x cont,"; - pr " 2 ^ (Zpos q) <= [head0 x] ->"; - pr " (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->"; - pr " [cont n x] = [x] * 2 ^ [n]) -> "; - pr " [safe_shiftl_aux p cont n x] = [x] * 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " intros p; elim p; unfold safe_shiftl_aux; fold safe_shiftl_aux; clear p."; - pp " intros p Hrec q n x cont H1 H2."; - pp " apply spec_safe_shift_aux_body with (q); auto."; - pp " intros x1 H3; apply Hrec with (q + 1)%spositive; auto." "%"; - pp " intros x2 H4; apply Hrec with (p + q + 1)%spositive; auto." "%"; - pp " rewrite <- Pplus_assoc."; - pp " rewrite Zpos_plus_distr; auto."; - pp " intros x3 H5; apply H2."; - pp " rewrite Zpos_xI."; - pp " replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));"; - pp " auto."; - pp " repeat rewrite Zpos_plus_distr; ring."; - pp " intros p Hrec q n x cont H1 H2."; - pp " apply spec_safe_shift_aux_body with (q); auto."; - pp " intros x1 H3; apply Hrec with (q); auto."; - pp " apply Zle_trans with (2 := H3); auto with zarith."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " intros x2 H4; apply Hrec with (p + q)%spositive; auto." "%"; - pp " intros x3 H5; apply H2."; - pp " rewrite (Zpos_xO p)."; - pp " replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));"; - pp " auto."; - pp " repeat rewrite Zpos_plus_distr; ring."; - pp " intros q n x cont H1 H2."; - pp " apply spec_safe_shift_aux_body with (q); auto."; - pp " rewrite Zplus_comm; auto."; - pp " Qed."; - pr ""; - - - pr " Definition safe_shiftl n x :="; - pr " safe_shiftl_aux_body"; - pr " (safe_shiftl_aux_body"; - pr " (safe_shiftl_aux (digits n) shiftl)) n x."; - pr ""; - - pr " Theorem spec_safe_shift: forall n x,"; - pr " [safe_shiftl n x] = [x] * 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " intros n x; unfold safe_shiftl, safe_shiftl_aux_body."; - pp " generalize (spec_compare n (head0 x)); case compare; intros H."; - pp " apply spec_shiftl; auto with zarith."; - pp " apply spec_shiftl; auto with zarith."; - pp " rewrite <- (spec_double_size x)."; - pp " generalize (spec_compare n (head0 (double_size x))); case compare; intros H1."; - pp " apply spec_shiftl; auto with zarith."; - pp " apply spec_shiftl; auto with zarith."; - pp " rewrite <- (spec_double_size (double_size x))."; - pp " apply spec_safe_shift_aux with 1%spositive." "%"; - pp " apply Zle_trans with (2 := spec_double_size_head0 (double_size x))."; - pp " replace (2 ^ 1) with (2 * 1)."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " generalize (spec_double_size_head0_pos x); auto with zarith."; - pp " rewrite Zpower_1_r; ring."; - pp " intros x1 H2; apply spec_shiftl."; - pp " apply Zle_trans with (2 := H2)."; - pp " apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith."; - pp " case (spec_digits n); auto with zarith."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " Qed."; - pr ""; - (* even *) pr " Definition is_even x :="; pr " match x with"; @@ -3146,20 +2669,6 @@ let _ = pp " Qed."; pr ""; - pr " Theorem spec_0: [zero] = 0."; - pa " Admitted."; - pp " Proof."; - pp " exact (spec_0 w0_spec)."; - pp " Qed."; - pr ""; - - pr " Theorem spec_1: [one] = 1."; - pa " Admitted."; - pp " Proof."; - pp " exact (spec_1 w0_spec)."; - pp " Qed."; - pr ""; - pr "End Make."; pr ""; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index ae2cfd30..d42db97d 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 10964 2008-05-22 11:08:13Z letouzey $ i*) +(*i $Id$ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -21,7 +21,7 @@ Require Import DoubleCyclic. (* To compute the necessary height *) Fixpoint plength (p: positive) : positive := - match p with + match p with xH => xH | xO p1 => Psucc (plength p1) | xI p1 => Psucc (plength p1) @@ -34,10 +34,10 @@ rewrite Zpower_exp; auto with zarith. rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. intros p; elim p; simpl plength; auto. intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. -assert (tmp: (forall p, 2 * p = p + p)%Z); +assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). -assert (tmp: (forall p, 2 * p = p + p)%Z); +assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. rewrite Zpower_1_r; auto with zarith. Qed. @@ -73,7 +73,7 @@ case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. intros q1 H2. replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. -generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; +generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; case Zmod. intros HH _; rewrite HH; auto with zarith. intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism. @@ -121,9 +121,9 @@ Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n. Defined. Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) := - match n return forall w:Type, zn2z w -> word w (S n) with + match n return forall w:Type, zn2z w -> word w (S n) with | O => fun w x => x - | S m => + | S m => let aux := extend m in fun w x => WW W0 (aux w x) end. @@ -169,7 +169,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := | S n1 => let v := fst (diff m1 n1) + n1 in let v1 := fst (diff m1 n1) + S n1 in - eq_ind v (fun n => v1 = S n) + eq_ind v (fun n => v1 = S n) (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _)) _ (diff_l _ _) end @@ -182,7 +182,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := | 0 => refl_equal _ | S _ => plusn0 _ end - | S m => + | S m => match n return (snd (diff (S m) n) + S m = max (S m) n) with | 0 => refl_equal (snd (diff (S m) 0) + S m) | S n1 => @@ -253,9 +253,9 @@ Section ReduceRec. | WW xh xl => match xh with | W0 => @reduce_n m xl - | _ => @c (S m) x + | _ => @c (S m) x end - end + end end. End ReduceRec. @@ -276,14 +276,14 @@ Section CompareRec. Variable compare_m : wm -> w -> comparison. Fixpoint compare0_mn (n:nat) : word wm n -> comparison := - match n return word wm n -> comparison with - | O => compare0_m + match n return word wm n -> comparison with + | O => compare0_m | S m => fun x => match x with | W0 => Eq - | WW xh xl => + | WW xh xl => match compare0_mn m xh with - | Eq => compare0_mn m xl + | Eq => compare0_mn m xl | r => Lt end end @@ -296,7 +296,7 @@ Section CompareRec. Variable spec_compare0_m: forall x, match compare0_m x with Eq => w_to_Z w_0 = wm_to_Z x - | Lt => w_to_Z w_0 < wm_to_Z x + | Lt => w_to_Z w_0 < wm_to_Z x | Gt => w_to_Z w_0 > wm_to_Z x end. Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. @@ -341,14 +341,14 @@ Section CompareRec. Qed. Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := - match n return word wm n -> w -> comparison with - | O => compare_m - | S m => fun x y => + match n return word wm n -> w -> comparison with + | O => compare_m + | S m => fun x y => match x with | W0 => compare w_0 y - | WW xh xl => + | WW xh xl => match compare0_mn m xh with - | Eq => compare_mn_1 m xl y + | Eq => compare_mn_1 m xl y | r => Gt end end @@ -366,7 +366,7 @@ Section CompareRec. | Lt => wm_to_Z x < w_to_Z y | Gt => wm_to_Z x > w_to_Z y end. - Variable wm_base_lt: forall x, + Variable wm_base_lt: forall x, 0 <= w_to_Z x < base (wm_base). Let double_wB_lt: forall n x, @@ -385,7 +385,7 @@ Section CompareRec. unfold Zpower_pos; simpl; ring. Qed. - + Lemma spec_compare_mn_1: forall n x y, match compare_mn_1 n x y with Eq => double_to_Z n x = w_to_Z y @@ -434,7 +434,7 @@ Section AddS. | C1 z => match incr hy with C0 z1 => C0 (WW z1 z) | C1 z1 => C1 (WW z1 z) - end + end end end. @@ -458,12 +458,12 @@ End AddS. Fixpoint length_pos x := match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. - + Theorem length_pos_lt: forall x y, (length_pos x < length_pos y)%nat -> Zpos x < Zpos y. Proof. intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; - intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; + intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1)); try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1)); try (inversion H; fail); @@ -492,20 +492,20 @@ End AddS. Qed. Theorem make_zop: forall w (x: znz_op w), - znz_to_Z (mk_zn2z_op x) = - fun z => match z with + znz_to_Z (mk_zn2z_op x) = + fun z => match z with W0 => 0 - | WW xh xl => znz_to_Z x xh * base (znz_digits x) + | WW xh xl => znz_to_Z x xh * base (znz_digits x) + znz_to_Z x xl end. intros ww x; auto. Qed. Theorem make_kzop: forall w (x: znz_op w), - znz_to_Z (mk_zn2z_op_karatsuba x) = - fun z => match z with + znz_to_Z (mk_zn2z_op_karatsuba x) = + fun z => match z with W0 => 0 - | WW xh xl => znz_to_Z x xh * base (znz_digits x) + | WW xh xl => znz_to_Z x xh * base (znz_digits x) + znz_to_Z x xl end. intros ww x; auto. |