summaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN')
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v109
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v1576
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml3511
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v323
4 files changed, 2522 insertions, 2997 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 7c480862..072b75f7 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -12,7 +12,7 @@
Require Export Int31.
Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
- NProperties NDiv GenericMinMax.
+ NProperties GenericMinMax.
(** The following [BigN] module regroups both the operations and
all the abstract properties:
@@ -21,73 +21,63 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
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].
+ - [NProp] adds all generic properties derived from [NAxioms]
- [MinMax*Properties] provides properties of [min] and [max].
*)
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
- NMake.Make Int31Cyclic <+ NTypeIsNAxioms
- <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec
- <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+Delimit Scope bigN_scope with bigN.
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
+ Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
+ Bind Scope bigN_scope with t t'.
+ Include NTypeIsNAxioms
+ <+ NProp [no inline]
+ <+ HasEqBool2Dec [no inline]
+ <+ MinMaxLogicalProperties [no inline]
+ <+ MinMaxDecProperties [no inline].
+End BigN.
+
+(** Nota concerning scopes : for the first Include, we cannot bind
+ the scope bigN_scope to a type that doesn't exists yet.
+ We hence need to explicitely declare the scope substitution.
+ For the next Include, the abstract type t (in scope abstract_scope)
+ gets substituted to concrete BigN.t (in scope bigN_scope),
+ and the corresponding argument scope are fixed automatically.
+*)
(** Notations about [BigN] *)
-Notation bigN := BigN.t.
-
-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_.
-(* 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 Open Scope bigN_scope.
+Notation bigN := BigN.t.
+Bind Scope bigN_scope with bigN BigN.t BigN.t'.
+Arguments BigN.N0 _%int31.
Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
+Local Notation "2" := BigN.two : 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.pow : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
+Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
+Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
+Infix "<?" := BigN.ltb (at level 70, no associativity) : 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.
+Notation "x != y" := (~x==y) (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 "x > y" := (y < x) (only parsing) : bigN_scope.
+Notation "x >= y" := (y <= x) (only parsing) : bigN_scope.
+Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
+Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
+Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
-Local Open Scope bigN_scope.
-
(** Example of reasoning about [BigN] *)
Theorem succ_pred: forall q : bigN,
@@ -107,29 +97,29 @@ 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.
+Lemma BigNeqb_correct : forall x y, (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.
+Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
Proof.
constructor.
-intros. red. rewrite BigN.spec_power. unfold id.
-destruct Zpower_theory as [EQ]. rewrite EQ.
+intros. red. rewrite BigN.spec_pow, BigN.spec_of_N.
+rewrite Zpower_theory.(rpow_pow_N).
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).
+ (fun a b => if 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).
+case Z.eqb_spec.
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').
+destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
intros (EQ,_). injection 1. intros EQr EQq.
BigN.zify. rewrite EQr, EQq; auto.
Qed.
@@ -163,6 +153,7 @@ Ltac isBigNcst t :=
end
| BigN.zero => constr:true
| BigN.one => constr:true
+ | BigN.two => constr:true
| _ => constr:false
end.
@@ -172,6 +163,12 @@ Ltac BigNcst t :=
| false => constr:NotConstant
end.
+Ltac BigN_to_N t :=
+ match isBigNcst t with
+ | true => eval vm_compute in (BigN.to_N t)
+ | false => constr:NotConstant
+ end.
+
Ltac Ncst t :=
match isNcst t with
| true => constr:t
@@ -183,11 +180,11 @@ Ltac Ncst t :=
Add Ring BigNr : BigNring
(decidable BigNeqb_correct,
constants [BigNcst],
- power_tac BigNpower [Ncst],
+ power_tac BigNpower [BigN_to_N],
div BigNdiv).
Section TestRing.
-Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
+Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
intros. ring_simplify. reflexivity.
Qed.
End TestRing.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 2b70f1bb..5012a1b9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,118 +16,577 @@
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.
+Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType
+ Nbasic Wf_nat StreamMemo NSig NMake_gen.
-Module Make (Import W0:CyclicType) <: NType.
+Module Make (W0:CyclicType) <: NType.
- (** Macro-generated part *)
+ (** Let's include the macro-generated part. Even if we can't functorize
+ things (due to Eval red_t below), the rest of the module only uses
+ elements mentionned in interface [NAbstract]. *)
Include NMake_gen.Make W0.
+ Open Scope Z_scope.
+
+ Local Notation "[ x ]" := (to_Z x).
+
+ Definition eq (x y : t) := [x] = [y].
+
+ Declare Reduction red_t :=
+ lazy beta iota delta
+ [iter_t reduce same_level mk_t mk_t_S succ_t dom_t dom_op].
+
+ Ltac red_t :=
+ match goal with |- ?u => let v := (eval red_t in u) in change v end.
+
+ (** * Generic results *)
+
+ Tactic Notation "destr_t" constr(x) "as" simple_intropattern(pat) :=
+ destruct (destr_t x) as pat; cbv zeta;
+ rewrite ?iter_mk_t, ?spec_mk_t, ?spec_reduce.
+
+ Lemma spec_same_level : forall A (P:Z->Z->A->Prop)
+ (f : forall n, dom_t n -> dom_t n -> A),
+ (forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) ->
+ forall x y, P [x] [y] (same_level f x y).
+ Proof.
+ intros. apply spec_same_level_dep with (P:=fun _ => P); auto.
+ Qed.
+
+ Theorem spec_pos: forall x, 0 <= [x].
+ Proof.
+ intros x. destr_t x as (n,x). now case (ZnZ.spec_to_Z x).
+ Qed.
+
+ Lemma digits_dom_op_incr : forall n m, (n<=m)%nat ->
+ (ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive.
+ Proof.
+ intros.
+ change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))).
+ rewrite !digits_dom_op, !Pshiftl_nat_Zpower.
+ apply Z.mul_le_mono_nonneg_l; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
+ Qed.
+
+ Definition to_N (x : t) := Z.to_N (to_Z x).
+
+ (** * Zero, One *)
+
+ Definition zero := mk_t O ZnZ.zero.
+ Definition one := mk_t O ZnZ.one.
+
+ Theorem spec_0: [zero] = 0.
+ Proof.
+ unfold zero. rewrite spec_mk_t. exact ZnZ.spec_0.
+ Qed.
+
+ Theorem spec_1: [one] = 1.
+ Proof.
+ unfold one. rewrite spec_mk_t. exact ZnZ.spec_1.
+ Qed.
+
+ (** * Successor *)
+
+ (** NB: it is crucial here and for the rest of this file to preserve
+ the let-in's. They allow to pre-compute once and for all the
+ field access to Z/nZ initial structures (when n=0..6). *)
+
+ Local Notation succn := (fun n =>
+ let op := dom_op n in
+ let succ_c := ZnZ.succ_c in
+ let one := ZnZ.one in
+ fun x => match succ_c x with
+ | C0 r => mk_t n r
+ | C1 r => mk_t_S n (WW one r)
+ end).
+
+ Definition succ : t -> t := Eval red_t in iter_t succn.
+
+ Lemma succ_fold : succ = iter_t succn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_succ: forall n, [succ n] = [n] + 1.
+ Proof.
+ intros x. rewrite succ_fold. destr_t x as (n,x).
+ generalize (ZnZ.spec_succ_c x); case ZnZ.succ_c.
+ intros. rewrite spec_mk_t. assumption.
+ intros. unfold interp_carry in *.
+ rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption.
+ Qed.
+
+ (** Two *)
+
+ (** Not really pretty, but since W0 might be Z/2Z, we're not sure
+ there's a proper 2 there. *)
+
+ Definition two := succ one.
+
+ Lemma spec_2 : [two] = 2.
+ Proof.
+ unfold two. now rewrite spec_succ, spec_1.
+ Qed.
+
+ (** * Addition *)
+
+ Local Notation addn := (fun n =>
+ let op := dom_op n in
+ let add_c := ZnZ.add_c in
+ let one := ZnZ.one in
+ fun x y =>match add_c x y with
+ | C0 r => mk_t n r
+ | C1 r => mk_t_S n (WW one r)
+ end).
+
+ Definition add : t -> t -> t := Eval red_t in same_level addn.
+
+ Lemma add_fold : add = same_level addn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_add: forall x y, [add x y] = [x] + [y].
+ Proof.
+ intros x y. rewrite add_fold. apply spec_same_level; clear x y.
+ intros n x y. simpl.
+ generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H.
+ rewrite spec_mk_t. assumption.
+ rewrite spec_mk_t_S. unfold interp_carry in H.
+ simpl. rewrite ZnZ.spec_1. assumption.
+ Qed.
(** * Predecessor *)
- Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1).
+ Local Notation predn := (fun n =>
+ let pred_c := ZnZ.pred_c in
+ fun x => match pred_c x with
+ | C0 r => reduce n r
+ | C1 _ => zero
+ end).
+
+ Definition pred : t -> t := Eval red_t in iter_t predn.
+
+ Lemma pred_fold : pred = iter_t predn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [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.
+ intros x. rewrite pred_fold. destr_t x as (n,x). intros H.
+ generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'.
+ rewrite spec_reduce. assumption.
+ exfalso. unfold interp_carry in *.
+ generalize (ZnZ.spec_to_Z x) (ZnZ.spec_to_Z y); auto with zarith.
Qed.
+ Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0.
+ Proof.
+ intros x. rewrite pred_fold. destr_t x as (n,x). intros H.
+ generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'.
+ rewrite spec_reduce.
+ unfold interp_carry in H'.
+ generalize (ZnZ.spec_to_Z y); auto with zarith.
+ exact spec_0.
+ Qed.
+
+ Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1).
+ Proof.
+ rewrite Z.max_comm.
+ destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)].
+ - apply spec_pred0; generalize (spec_pos x); auto with zarith.
+ - apply spec_pred_pos; auto with zarith.
+ Qed.
(** * Subtraction *)
- Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]).
+ Local Notation subn := (fun n =>
+ let sub_c := ZnZ.sub_c in
+ fun x y => match sub_c x y with
+ | C0 r => reduce n r
+ | C1 r => zero
+ end).
+
+ Definition sub : t -> t -> t := Eval red_t in same_level subn.
+
+ Lemma sub_fold : sub = same_level subn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
+ Proof.
+ intros x y. rewrite sub_fold. apply spec_same_level. clear x y.
+ intros n x y. simpl.
+ generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE.
+ rewrite spec_reduce. assumption.
+ unfold interp_carry in H.
+ exfalso.
+ generalize (ZnZ.spec_to_Z z); auto with zarith.
+ Qed.
+
+ Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0.
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.
+ intros x y. rewrite sub_fold. apply spec_same_level. clear x y.
+ intros n x y. simpl.
+ generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE.
+ rewrite spec_reduce.
+ unfold interp_carry in H.
+ generalize (ZnZ.spec_to_Z z); auto with zarith.
+ exact spec_0.
+ Qed.
+
+ Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]).
+ Proof.
+ intros. destruct (Z.le_gt_cases [y] [x]).
+ rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto.
+ rewrite Z.max_l; auto with zarith. apply spec_sub0; auto.
Qed.
(** * Comparison *)
- Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y].
+ Definition comparen_m n :
+ forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
+ let op := dom_op n in
+ let zero := @ZnZ.zero _ op in
+ let compare := @ZnZ.compare _ op in
+ let compare0 := compare zero in
+ fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
+
+ Let spec_comparen_m:
+ forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
+ comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
+ Proof.
+ intros n m x y.
+ unfold comparen_m, eval.
+ rewrite nmake_double.
+ apply spec_compare_mn_1.
+ exact ZnZ.spec_0.
+ intros. apply ZnZ.spec_compare.
+ exact ZnZ.spec_to_Z.
+ exact ZnZ.spec_compare.
+ exact ZnZ.spec_compare.
+ exact ZnZ.spec_to_Z.
+ Qed.
+
+ Definition comparenm n m wx wy :=
+ let mn := Max.max n m in
+ let d := diff n m in
+ let op := make_op mn in
+ ZnZ.compare
+ (castm (diff_r n m) (extend_tr wx (snd d)))
+ (castm (diff_l n m) (extend_tr wy (fst d))).
+
+ Local Notation compare_folded :=
+ (iter_sym _
+ (fun n => @ZnZ.compare _ (dom_op n))
+ comparen_m
+ comparenm
+ CompOpp).
+
+ Definition compare : t -> t -> comparison :=
+ Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in
+ compare_folded.
+
+ Lemma compare_fold : compare = compare_folded.
+ Proof.
+ lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity.
+ Qed.
+
+ Theorem spec_compare : forall x y,
+ compare x y = Z.compare [x] [y].
Proof.
- intros x y. generalize (spec_compare_aux x y); destruct compare;
- intros; symmetry; try rewrite Zcompare_Eq_iff_eq; assumption.
+ intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y.
+ intros. apply ZnZ.spec_compare.
+ intros. cbv beta zeta. apply spec_comparen_m.
+ intros n m x y; unfold comparenm.
+ rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+ unfold to_Z; apply ZnZ.spec_compare.
+ intros. subst. now rewrite <- Z.compare_antisym.
Qed.
- Definition eq_bool x y :=
+ Definition eqb (x y : t) : bool :=
match compare x y with
| Eq => true
| _ => false
end.
- Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y].
+ Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].
+ Proof.
+ apply eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition lt (n m : t) := [n] < [m].
+ Definition le (n m : t) := [n] <= [m].
+
+ Definition ltb (x y : t) : bool :=
+ match compare x y with
+ | Lt => true
+ | _ => false
+ end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb [x] [y].
Proof.
- intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity.
+ apply eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
Qed.
- Theorem spec_eq_bool_aux: forall x y,
- if eq_bool x y then [x] = [y] else [x] <> [y].
+ Definition leb (x y : t) : bool :=
+ match compare x y with
+ | Gt => false
+ | _ => true
+ end.
+
+ Theorem spec_leb x y : leb x y = Z.leb [x] [y].
Proof.
- intros x y; unfold eq_bool.
- generalize (spec_compare_aux x y); case compare; auto with zarith.
+ apply eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
Qed.
- Definition lt n m := [n] < [m].
- Definition le n m := [n] <= [m].
+ Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
+ Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
- 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] = Z.max [n] [m].
+ Proof.
+ intros. unfold max, Z.max. rewrite spec_compare; destruct Z.compare; reflexivity.
+ Qed.
- Theorem spec_max : forall n m, [max n m] = Zmax [n] [m].
+ Theorem spec_min : forall n m, [min n m] = Z.min [n] [m].
Proof.
- intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity.
+ intros. unfold min, Z.min. rewrite spec_compare; destruct Z.compare; reflexivity.
Qed.
- Theorem spec_min : forall n m, [min n m] = Zmin [n] [m].
+ (** * Multiplication *)
+
+ Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
+ let op := dom_op n in
+ let zero := @ZnZ.zero _ op in
+ let succ := @ZnZ.succ _ op in
+ let add_c := @ZnZ.add_c _ op in
+ let mul_c := @ZnZ.mul_c _ op in
+ let ww := @ZnZ.WW _ op in
+ let ow := @ZnZ.OW _ op in
+ let eq0 := @ZnZ.eq0 _ op in
+ let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
+ let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
+ fun m x y =>
+ let (w,r) := mul_add_n1 (S m) x y zero in
+ if eq0 w then mk_t_w' n m r
+ else mk_t_w' n (S m) (WW (extend n m w) r).
+
+ Definition mulnm n m x y :=
+ let mn := Max.max n m in
+ let d := diff n m in
+ let op := make_op mn in
+ reduce_n (S mn) (ZnZ.mul_c
+ (castm (diff_r n m) (extend_tr x (snd d)))
+ (castm (diff_l n m) (extend_tr y (fst d)))).
+
+ Local Notation mul_folded :=
+ (iter_sym _
+ (fun n => let mul_c := ZnZ.mul_c in
+ fun x y => reduce (S n) (succ_t _ (mul_c x y)))
+ wn_mul
+ mulnm
+ (fun x => x)).
+
+ Definition mul : t -> t -> t :=
+ Eval lazy beta iota delta
+ [iter_sym dom_op dom_t reduce succ_t extend zeron
+ wn_mul DoubleMul.w_mul_add mk_t_w'] in
+ mul_folded.
+
+ Lemma mul_fold : mul = mul_folded.
Proof.
- intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity.
+ lazy beta iota delta
+ [iter_sym dom_op dom_t reduce succ_t extend zeron
+ wn_mul DoubleMul.w_mul_add mk_t_w']. reflexivity.
Qed.
+ Lemma spec_muln:
+ forall n (x: word _ (S n)) y,
+ [Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [Nn n x] * [Nn n y].
+ Proof.
+ intros n x y; unfold to_Z.
+ rewrite <- ZnZ.spec_mul_c.
+ rewrite make_op_S.
+ case ZnZ.mul_c; auto.
+ Qed.
- (** * Power *)
+ Lemma spec_mul_add_n1: forall n m x y z,
+ let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW
+ (DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c)
+ (S m) x y z in
+ ZnZ.to_Z q * (base (ZnZ.digits (nmake_op _ (dom_op n) (S m))))
+ + eval n (S m) r =
+ eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z.
+ Proof.
+ intros n m x y z.
+ rewrite digits_nmake.
+ unfold eval. rewrite nmake_double.
+ apply DoubleMul.spec_double_mul_add_n1.
+ apply ZnZ.spec_0.
+ exact ZnZ.spec_WW.
+ exact ZnZ.spec_OW.
+ apply DoubleCyclic.spec_mul_add.
+ Qed.
- 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.
+ Lemma spec_wn_mul : forall n m x y,
+ [wn_mul n m x y] = (eval n (S m) x) * ZnZ.to_Z y.
+ Proof.
+ intros; unfold wn_mul.
+ generalize (spec_mul_add_n1 n m x y ZnZ.zero).
+ case DoubleMul.double_mul_add_n1; intros q r Hqr.
+ rewrite ZnZ.spec_0, Z.add_0_r in Hqr. rewrite <- Hqr.
+ generalize (ZnZ.spec_eq0 q); case ZnZ.eq0; intros HH.
+ rewrite HH; auto. simpl. apply spec_mk_t_w'.
+ clear.
+ rewrite spec_mk_t_w'.
+ set (m' := S m) in *.
+ unfold eval.
+ rewrite nmake_WW. f_equal. f_equal.
+ rewrite <- spec_mk_t.
+ symmetry. apply spec_extend.
+ Qed.
- Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Theorem spec_mul : forall x y, [mul x y] = [x] * [y].
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.
+ intros x y. rewrite mul_fold. apply spec_iter_sym; clear x y.
+ intros n x y. cbv zeta beta.
+ rewrite spec_reduce, spec_succ_t, <- ZnZ.spec_mul_c; auto.
+ apply spec_wn_mul.
+ intros n m x y; unfold mulnm. rewrite spec_reduce_n.
+ rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+ apply spec_muln.
+ intros. rewrite Z.mul_comm; auto.
Qed.
- Definition power x (n:N) := match n with
- | BinNat.N0 => one
- | BinNat.Npos p => power_pos x p
- end.
+ (** * Division by a smaller number *)
+
+ Definition wn_divn1 n :=
+ let op := dom_op n in
+ let zd := ZnZ.zdigits op in
+ let zero := @ZnZ.zero _ op in
+ let ww := @ZnZ.WW _ op in
+ let head0 := @ZnZ.head0 _ op in
+ let add_mul_div := @ZnZ.add_mul_div _ op in
+ let div21 := @ZnZ.div21 _ op in
+ let compare := @ZnZ.compare _ op in
+ let sub := @ZnZ.sub _ op in
+ let ddivn1 :=
+ DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
+ fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).
+
+ Let div_gtnm n m wx wy :=
+ let mn := Max.max n m in
+ let d := diff n m in
+ let op := make_op mn in
+ let (q, r):= ZnZ.div_gt
+ (castm (diff_r n m) (extend_tr wx (snd d)))
+ (castm (diff_l n m) (extend_tr wy (fst d))) in
+ (reduce_n mn q, reduce_n mn r).
+
+ Local Notation div_gt_folded :=
+ (iter _
+ (fun n => let div_gt := ZnZ.div_gt in
+ fun x y => let (u,v) := div_gt x y in (reduce n u, reduce n v))
+ (fun n =>
+ let div_gt := ZnZ.div_gt in
+ fun m x y =>
+ let y' := DoubleBase.get_low (zeron n) (S m) y in
+ let (u,v) := div_gt x y' in (reduce n u, reduce n v))
+ wn_divn1
+ div_gtnm).
+
+ Definition div_gt :=
+ Eval lazy beta iota delta
+ [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t] in
+ div_gt_folded.
+
+ Lemma div_gt_fold : div_gt = div_gt_folded.
+ Proof.
+ lazy beta iota delta [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t].
+ reflexivity.
+ Qed.
+
+ Lemma spec_get_endn: forall n m x y,
+ eval n m x <= [mk_t n y] ->
+ [mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x.
+ Proof.
+ intros n m x y H.
+ unfold eval. rewrite nmake_double.
+ rewrite spec_mk_t in *.
+ apply DoubleBase.spec_get_low.
+ apply spec_zeron.
+ exact ZnZ.spec_to_Z.
+ apply Z.le_lt_trans with (ZnZ.to_Z y); auto.
+ rewrite <- nmake_double; auto.
+ case (ZnZ.spec_to_Z y); auto.
+ Qed.
- Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Let spec_divn1 n :=
+ DoubleDivn1.spec_double_divn1
+ (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
+ ZnZ.WW ZnZ.head0
+ ZnZ.add_mul_div ZnZ.div21
+ ZnZ.compare ZnZ.sub ZnZ.to_Z
+ ZnZ.spec_to_Z
+ ZnZ.spec_zdigits
+ ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
+ ZnZ.spec_add_mul_div ZnZ.spec_div21
+ ZnZ.spec_compare ZnZ.spec_sub.
+
+ Lemma spec_div_gt_aux : forall x y, [x] > [y] -> 0 < [y] ->
+ let (q,r) := div_gt x y in
+ [x] = [q] * [y] + [r] /\ 0 <= [r] < [y].
Proof.
- destruct n; simpl. apply (spec_1 w0_spec).
- apply spec_power_pos.
+ intros x y. rewrite div_gt_fold. apply spec_iter; clear x y.
+ intros n x y H1 H2. simpl.
+ generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt.
+ intros u v. rewrite 2 spec_reduce. auto.
+ intros n m x y H1 H2. cbv zeta beta.
+ generalize (ZnZ.spec_div_gt x
+ (DoubleBase.get_low (zeron n) (S m) y)).
+ case ZnZ.div_gt.
+ intros u v H3; repeat rewrite spec_reduce.
+ generalize (spec_get_endn n (S m) y x). rewrite !spec_mk_t. intros H4.
+ rewrite H4 in H3; auto with zarith.
+ intros n m x y H1 H2.
+ generalize (spec_divn1 n (S m) x y H2).
+ unfold wn_divn1; case DoubleDivn1.double_divn1.
+ intros u v H3.
+ rewrite spec_mk_t_w', spec_mk_t.
+ rewrite <- !nmake_double in H3; auto.
+ intros n m x y H1 H2; unfold div_gtnm.
+ generalize (ZnZ.spec_div_gt
+ (castm (diff_r n m)
+ (extend_tr x (snd (diff n m))))
+ (castm (diff_l n m)
+ (extend_tr y (fst (diff n m))))).
+ case ZnZ.div_gt.
+ intros xx yy HH.
+ repeat rewrite spec_reduce_n.
+ rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+ unfold to_Z; apply HH.
+ rewrite (spec_cast_l n m x) in H1; auto.
+ rewrite (spec_cast_r n m y) in H1; auto.
+ rewrite (spec_cast_r n m y) in H2; auto.
Qed.
+ Theorem spec_div_gt: forall x y, [x] > [y] -> 0 < [y] ->
+ let (q,r) := div_gt x y in
+ [q] = [x] / [y] /\ [r] = [x] mod [y].
+ Proof.
+ intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt.
+ intros q r (H3, H4); split.
+ apply (Zdiv_unique [x] [y] [q] [r]); auto.
+ rewrite Z.mul_comm; auto.
+ apply (Zmod_unique [x] [y] [q] [r]); auto.
+ rewrite Z.mul_comm; auto.
+ Qed.
- (** * Div *)
+ (** * General Division *)
- Definition div_eucl x y :=
- if eq_bool y zero then (zero,zero) else
+ Definition div_eucl (x y : t) : t * t :=
+ if eqb y zero then (zero,zero) else
match compare x y with
| Eq => (one, zero)
| Lt => (zero, x)
@@ -136,49 +595,123 @@ Module Make (Import W0:CyclicType) <: NType.
Theorem spec_div_eucl: forall x y,
let (q,r) := div_eucl x y in
- ([q], [r]) = Zdiv_eucl [x] [y].
+ ([q], [r]) = Z.div_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).
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
+ intros ->. rewrite spec_0. destruct [x]; auto.
+ intros 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; 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.
+ case Z.compare_spec; intros Cmp;
+ rewrite ?spec_0, ?spec_1; intros; auto with zarith.
+ rewrite Cmp; generalize (Z_div_same [y] (Z.lt_gt _ _ H))
+ (Z_mod_same [y] (Z.lt_gt _ _ H));
+ unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto.
+ assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto).
+ generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt);
+ unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto.
+ generalize (spec_div_gt _ _ (Z.lt_gt _ _ Cmp) H); auto.
+ unfold Z.div, Z.modulo; case Z.div_eucl; case div_gt.
intros a b c d (H1, H2); subst; auto.
Qed.
- Definition div x y := fst (div_eucl x y).
+ Definition div (x y : t) : t := 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;
+ intros xx yy; unfold Z.div; case Z.div_eucl; intros qq rr H;
injection H; auto.
Qed.
+ (** * Modulo by a smaller number *)
+
+ Definition wn_modn1 n :=
+ let op := dom_op n in
+ let zd := ZnZ.zdigits op in
+ let zero := @ZnZ.zero _ op in
+ let head0 := @ZnZ.head0 _ op in
+ let add_mul_div := @ZnZ.add_mul_div _ op in
+ let div21 := @ZnZ.div21 _ op in
+ let compare := @ZnZ.compare _ op in
+ let sub := @ZnZ.sub _ op in
+ let dmodn1 :=
+ DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
+ fun m x y => reduce n (dmodn1 (S m) x y).
+
+ Let mod_gtnm n m wx wy :=
+ let mn := Max.max n m in
+ let d := diff n m in
+ let op := make_op mn in
+ reduce_n mn (ZnZ.modulo_gt
+ (castm (diff_r n m) (extend_tr wx (snd d)))
+ (castm (diff_l n m) (extend_tr wy (fst d)))).
+
+ Local Notation mod_gt_folded :=
+ (iter _
+ (fun n => let modulo_gt := ZnZ.modulo_gt in
+ fun x y => reduce n (modulo_gt x y))
+ (fun n => let modulo_gt := ZnZ.modulo_gt in
+ fun m x y =>
+ reduce n (modulo_gt x (DoubleBase.get_low (zeron n) (S m) y)))
+ wn_modn1
+ mod_gtnm).
+
+ Definition mod_gt :=
+ Eval lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron] in
+ mod_gt_folded.
+
+ Lemma mod_gt_fold : mod_gt = mod_gt_folded.
+ Proof.
+ lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron].
+ reflexivity.
+ Qed.
+
+ Let spec_modn1 n :=
+ DoubleDivn1.spec_double_modn1
+ (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
+ ZnZ.WW ZnZ.head0
+ ZnZ.add_mul_div ZnZ.div21
+ ZnZ.compare ZnZ.sub ZnZ.to_Z
+ ZnZ.spec_to_Z
+ ZnZ.spec_zdigits
+ ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
+ ZnZ.spec_add_mul_div ZnZ.spec_div21
+ ZnZ.spec_compare ZnZ.spec_sub.
+
+ Theorem spec_mod_gt:
+ forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].
+ Proof.
+ intros x y. rewrite mod_gt_fold. apply spec_iter; clear x y.
+ intros n x y H1 H2. simpl. rewrite spec_reduce.
+ exact (ZnZ.spec_modulo_gt x y H1 H2).
+ intros n m x y H1 H2. cbv zeta beta. rewrite spec_reduce.
+ rewrite <- spec_mk_t in H1.
+ rewrite <- (spec_get_endn n (S m) y x); auto with zarith.
+ rewrite spec_mk_t.
+ apply ZnZ.spec_modulo_gt; auto.
+ rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H1; auto with zarith.
+ rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H2; auto with zarith.
+ intros n m x y H1 H2. unfold wn_modn1. rewrite spec_reduce.
+ unfold eval; rewrite nmake_double.
+ apply (spec_modn1 n); auto.
+ intros n m x y H1 H2; unfold mod_gtnm.
+ repeat rewrite spec_reduce_n.
+ rewrite (spec_cast_l n m x), (spec_cast_r n m y).
+ unfold to_Z; apply ZnZ.spec_modulo_gt.
+ rewrite (spec_cast_l n m x) in H1; auto.
+ rewrite (spec_cast_r n m y) in H1; auto.
+ rewrite (spec_cast_r n m y) in H2; auto.
+ Qed.
- (** * Modulo *)
+ (** * General Modulo *)
- Definition modulo x y :=
- if eq_bool y zero then zero else
+ Definition modulo (x y : t) : t :=
+ if eqb y zero then zero else
match compare x y with
| Eq => zero
| Lt => x
@@ -188,25 +721,130 @@ Module Make (Import W0:CyclicType) <: NType.
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.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
+ intros ->; rewrite spec_0. 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.
+ case Z.compare_spec;
+ rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith.
+ rewrite H0; symmetry; apply Z_mod_same; auto with zarith.
+ symmetry; apply Zmod_small; auto with zarith.
generalize (spec_pos x); auto with zarith.
- apply spec_mod_gt; auto.
+ apply spec_mod_gt; auto with zarith.
+ Qed.
+
+ (** * Square *)
+
+ Local Notation squaren := (fun n =>
+ let square_c := ZnZ.square_c in
+ fun x => reduce (S n) (succ_t _ (square_c x))).
+
+ Definition square : t -> t := Eval red_t in iter_t squaren.
+
+ Lemma square_fold : square = iter_t squaren.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_square: forall x, [square x] = [x] * [x].
+ Proof.
+ intros x. rewrite square_fold. destr_t x as (n,x).
+ rewrite spec_succ_t. exact (ZnZ.spec_square_c x).
+ Qed.
+
+ (** * Square Root *)
+
+ Local Notation sqrtn := (fun n =>
+ let sqrt := ZnZ.sqrt in
+ fun x => reduce n (sqrt x)).
+
+ Definition sqrt : t -> t := Eval red_t in iter_t sqrtn.
+
+ Lemma sqrt_fold : sqrt = iter_t sqrtn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_sqrt_aux: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+ Proof.
+ intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x).
+ Qed.
+
+ Theorem spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Proof.
+ intros x.
+ symmetry. apply Z.sqrt_unique.
+ rewrite <- ! Z.pow_2_r. apply spec_sqrt_aux.
+ Qed.
+
+ (** * Power *)
+
+ Fixpoint pow_pos (x:t)(p:positive) : t :=
+ match p with
+ | xH => x
+ | xO p => square (pow_pos x p)
+ | xI p => mul (square (pow_pos x p)) x
+ end.
+
+ Theorem spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
+ Proof.
+ intros x n; generalize x; elim n; clear n x; simpl pow_pos.
+ intros; rewrite spec_mul; rewrite spec_square; rewrite H.
+ rewrite Pos2Z.inj_xI; rewrite Zpower_exp; auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r; rewrite Z.pow_1_r; auto.
+ intros; rewrite spec_square; rewrite H.
+ rewrite Pos2Z.inj_xO; auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r; auto.
+ intros; rewrite Z.pow_1_r; auto.
+ Qed.
+
+ Definition pow_N (x:t)(n:N) : t := match n with
+ | BinNat.N0 => one
+ | BinNat.Npos p => pow_pos x p
+ end.
+
+ Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.
+ Proof.
+ destruct n; simpl. apply spec_1.
+ apply spec_pow_pos.
+ Qed.
+
+ Definition pow (x y:t) : t := pow_N x (to_N y).
+
+ Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y].
+ Proof.
+ intros. unfold pow, to_N.
+ now rewrite spec_pow_N, Z2N.id by apply spec_pos.
Qed.
+ (** * digits
+
+ Number of digits in the representation of a numbers
+ (including head zero's).
+ NB: This function isn't a morphism for setoid [eq].
+ *)
+
+ Local Notation digitsn := (fun n =>
+ let digits := ZnZ.digits (dom_op n) in
+ fun _ => digits).
+
+ Definition digits : t -> positive := Eval red_t in iter_t digitsn.
+
+ Lemma digits_fold : digits = iter_t digitsn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x).
+ Proof.
+ intros x. rewrite digits_fold. destr_t x as (n,x). exact (ZnZ.spec_to_Z x).
+ Qed.
+
+ Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)).
+ Proof.
+ intros x. rewrite digits_fold. unfold level. destr_t x as (n,x). reflexivity.
+ Qed.
+
(** * Gcd *)
Definition gcd_gt_body a b cont :=
@@ -226,19 +864,16 @@ Module Make (Import W0:CyclicType) <: NType.
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.
+ rewrite ! spec_compare, spec_0. case Z.compare_spec.
+ intros ->; 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]).
+ intros H5; case Z.compare_spec.
+ intros H6; rewrite <- (Z.mul_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.
+ rewrite H6; rewrite Z.add_0_r.
apply Zis_gcd_mult; apply Zis_gcd_1.
intros; apply False_ind.
case (spec_digits (mod_gt a b)); auto with zarith.
@@ -253,27 +888,22 @@ Module Make (Import W0:CyclicType) <: NType.
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 :=
+ apply Z.mul_lt_mono_pos_r with 2; auto with zarith.
+ apply Z.le_lt_trans with ([b] + [mod_gt a b]); auto with zarith.
+ apply Z.le_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith.
+ - apply Z.add_le_mono_r.
+ rewrite <- (Z.mul_1_l [b]) at 1.
+ apply Z.mul_le_mono_nonneg_r; auto with zarith.
+ change 1 with (Z.succ 0). apply Z.le_succ_l.
+ apply Z.div_str_pos; auto with zarith.
+ - rewrite Z.mul_comm; rewrite spec_mod_gt; auto with zarith.
+ rewrite <- Z_div_mod_eq; auto with zarith.
+ rewrite Z.mul_comm, <- Z.pow_succ_r, Z.sub_1_r, Z.succ_pred; auto.
+ apply Z.le_0_sub. change 1 with (Z.succ 0). apply Z.le_succ_l.
+ destruct p; simpl in H3; auto with zarith.
+ Qed.
+
+ Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t :=
gcd_gt_body a b
(fun a b =>
match p with
@@ -294,7 +924,7 @@ Module Make (Import W0:CyclicType) <: NType.
apply Hrec with (Zpos p + n); auto.
replace (Zpos p + (Zpos p + n)) with
(Zpos (xI p) + n - 1); auto.
- rewrite Zpos_xI; ring.
+ rewrite Pos2Z.inj_xI; ring.
intros a2 b2 H9 H10.
apply Hrec with n; auto.
intros p Hrec n a b cont H2 H3 H4.
@@ -303,23 +933,18 @@ Module Make (Import W0:CyclicType) <: NType.
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.
+ rewrite Pos2Z.inj_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.
+ apply Z.lt_le_trans with (1 := H12).
+ apply Z.pow_le_mono_r; auto with zarith.
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.
+ rewrite Z.add_comm; auto.
intros a1 b1 H5 H6; apply H3; auto.
replace n with (n + 1 - 1); auto; try ring.
Qed.
@@ -333,192 +958,699 @@ Module Make (Import W0:CyclicType) <: NType.
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].
+ [a] > [b] -> [gcd_gt a b] = Z.gcd [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.
+ symmetry; 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.
+ intros a1 a2; rewrite Z.pow_0_r.
case (spec_digits a2); intros H7 H8;
intros; apply False_ind; auto with zarith.
Qed.
- Definition gcd a b :=
+ Definition gcd (a b : t) : t :=
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].
+ Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [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.
+ unfold gcd. rewrite spec_compare. case Z.compare_spec.
+ intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto.
apply Zis_gcd_refl.
- intros; apply trans_equal with (Zgcd [b] [a]).
+ intros; transitivity (Z.gcd [b] [a]).
apply spec_gcd_gt; auto with zarith.
apply Zis_gcd_gcd; auto with zarith.
- apply Zgcd_is_pos.
+ apply Z.gcd_nonneg.
apply Zis_gcd_sym; apply Zgcd_is_gcd.
- intros; apply spec_gcd_gt; auto.
+ intros; apply spec_gcd_gt; auto with zarith.
Qed.
+ (** * Parity test *)
+
+ Definition even : t -> bool := Eval red_t in
+ iter_t (fun n x => ZnZ.is_even x).
+
+ Definition odd x := negb (even x).
+
+ Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_even_aux: forall x,
+ if even x then [x] mod 2 = 0 else [x] mod 2 = 1.
+ Proof.
+ intros x. rewrite even_fold. destr_t x as (n,x).
+ exact (ZnZ.spec_is_even x).
+ Qed.
+
+ Theorem spec_even: forall x, even x = Z.even [x].
+ Proof.
+ intros x. assert (H := spec_even_aux x). symmetry.
+ rewrite (Z.div_mod [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Z.add_0_r.
+ rewrite Zeven_bool_iff. apply Zeven_2p.
+ apply not_true_is_false. rewrite Zeven_bool_iff.
+ apply Zodd_not_Zeven. apply Zodd_2p_plus_1.
+ Qed.
+
+ Theorem spec_odd: forall x, odd x = Z.odd [x].
+ Proof.
+ intros x. unfold odd.
+ assert (H := spec_even_aux x). symmetry.
+ rewrite (Z.div_mod [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Z.add_0_r; simpl negb.
+ apply not_true_is_false. rewrite Zodd_bool_iff.
+ apply Zeven_not_Zodd. apply Zeven_2p.
+ apply Zodd_bool_iff. apply Zodd_2p_plus_1.
+ Qed.
(** * Conversion *)
- Definition of_N x :=
+ Definition pheight p :=
+ Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))).
+
+ Theorem pheight_correct: forall p,
+ Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))).
+ Proof.
+ intros p; unfold pheight.
+ rewrite Nat2Z.inj_pred by apply Pos2Nat.is_pos.
+ rewrite positive_nat_Z.
+ rewrite <- Z.sub_1_r.
+ assert (F2:= (get_height_correct (ZnZ.digits (dom_op 0)) (plength p))).
+ apply Z.lt_le_trans with (Zpos (Pos.succ p)).
+ rewrite Pos2Z.inj_succ; auto with zarith.
+ apply Z.le_trans with (1 := plength_pred_correct (Pos.succ p)).
+ rewrite Pos.pred_succ.
+ apply Z.pow_le_mono_r; auto with zarith.
+ Qed.
+
+ Definition of_pos (x:positive) : t :=
+ let n := pheight x in
+ reduce n (snd (ZnZ.of_pos x)).
+
+ Theorem spec_of_pos: forall x,
+ [of_pos x] = Zpos x.
+ Proof.
+ intros x; unfold of_pos.
+ rewrite spec_reduce.
+ simpl.
+ apply ZnZ.of_pos_correct.
+ unfold base.
+ apply Z.lt_le_trans with (1 := pheight_correct x).
+ apply Z.pow_le_mono_r; auto with zarith.
+ rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith.
+ Qed.
+
+ Definition of_N (x:N) : t :=
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.
+ [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.
+ simpl of_N. exact spec_0.
intros p; exact (spec_of_pos p).
Qed.
+ (** * [head0] and [tail0]
- (** * Shift *)
+ Number of zero at the beginning and at the end of
+ the representation of the number.
+ NB: these functions are not morphism for setoid [eq].
+ *)
- Definition shiftr n x :=
- match compare n (Ndigits x) with
- | Lt => unsafe_shiftr n x
- | _ => N0 w_0
- end.
+ Local Notation head0n := (fun n =>
+ let head0 := ZnZ.head0 in
+ fun x => reduce n (head0 x)).
+
+ Definition head0 : t -> t := Eval red_t in iter_t head0n.
+
+ Lemma head0_fold : head0 = iter_t head0n.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_head00: forall x, [x] = 0 -> [head0 x] = Zpos (digits x).
+ Proof.
+ intros x. rewrite head0_fold, digits_fold. destr_t x as (n,x).
+ exact (ZnZ.spec_head00 x).
+ Qed.
+
+ Lemma pow2_pos_minus_1 : forall z, 0<z -> 2^(z-1) = 2^z / 2.
+ Proof.
+ intros. apply Zdiv_unique with 0; auto with zarith.
+ change 2 with (2^1) at 2.
+ rewrite <- Zpower_exp; auto with zarith.
+ rewrite Z.add_0_r. f_equal. auto with zarith.
+ Qed.
+
+ Theorem spec_head0: forall x, 0 < [x] ->
+ 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x).
+ Proof.
+ intros x. rewrite pow2_pos_minus_1 by (red; auto).
+ rewrite head0_fold, digits_fold. destr_t x as (n,x). exact (ZnZ.spec_head0 x).
+ Qed.
+
+ Local Notation tail0n := (fun n =>
+ let tail0 := ZnZ.tail0 in
+ fun x => reduce n (tail0 x)).
+
+ Definition tail0 : t -> t := Eval red_t in iter_t tail0n.
+
+ Lemma tail0_fold : tail0 = iter_t tail0n.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_tail00: forall x, [x] = 0 -> [tail0 x] = Zpos (digits x).
+ Proof.
+ intros x. rewrite tail0_fold, digits_fold. destr_t x as (n,x).
+ exact (ZnZ.spec_tail00 x).
+ Qed.
+
+ Theorem spec_tail0: forall x,
+ 0 < [x] -> exists y, 0 <= y /\ [x] = (2 * y + 1) * 2 ^ [tail0 x].
+ Proof.
+ intros x. rewrite tail0_fold. destr_t x as (n,x). exact (ZnZ.spec_tail0 x).
+ Qed.
+
+ (** * [Ndigits]
+
+ Same as [digits] but encoded using large integers
+ NB: this function is not a morphism for setoid [eq].
+ *)
+
+ Local Notation Ndigitsn := (fun n =>
+ let d := reduce n (ZnZ.zdigits (dom_op n)) in
+ fun _ => d).
+
+ Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn.
+
+ Lemma Ndigits_fold : Ndigits = iter_t Ndigitsn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x).
+ Proof.
+ intros x. rewrite Ndigits_fold, digits_fold. destr_t x as (n,x).
+ apply ZnZ.spec_zdigits.
+ Qed.
+
+ (** * Binary logarithm *)
+
+ Local Notation log2n := (fun n =>
+ let op := dom_op n in
+ let zdigits := ZnZ.zdigits op in
+ let head0 := ZnZ.head0 in
+ let sub_carry := ZnZ.sub_carry in
+ fun x => reduce n (sub_carry zdigits (head0 x))).
+
+ Definition log2 : t -> t := Eval red_t in
+ let log2 := iter_t log2n in
+ fun x => if eqb x zero then zero else log2 x.
+
+ Lemma log2_fold :
+ log2 = fun x => if eqb x zero then zero else iter_t log2n x.
+ Proof. red_t; reflexivity. Qed.
+
+ Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.
+ Proof.
+ intros x H. rewrite log2_fold.
+ rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0.
+ Qed.
+
+ Lemma head0_zdigits : forall n (x : dom_t n),
+ 0 < ZnZ.to_Z x ->
+ ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)).
+ Proof.
+ intros n x H.
+ destruct (ZnZ.spec_head0 x H) as (_,H0).
+ intros.
+ assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)).
+ assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))).
+ unfold base in *.
+ rewrite ZnZ.spec_zdigits in H2 |- *.
+ set (h := ZnZ.to_Z (ZnZ.head0 x)) in *; clearbody h.
+ set (d := ZnZ.digits (dom_op n)) in *; clearbody d.
+ destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso.
+ assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h).
+ apply Z.mul_le_mono_nonneg; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
+ rewrite Z.mul_comm in H0. auto with zarith.
+ Qed.
+
+ Lemma spec_log2_pos : forall x, [x]<>0 ->
+ 2^[log2 x] <= [x] < 2^([log2 x]+1).
+ Proof.
+ intros x H. rewrite log2_fold.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
+ auto with zarith.
+ clear H.
+ destr_t x as (n,x). intros H.
+ rewrite ZnZ.spec_sub_carry.
+ assert (H0 := ZnZ.spec_to_Z x).
+ assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)).
+ assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))).
+ assert (H3 := head0_zdigits n x).
+ rewrite Zmod_small by auto with zarith.
+ rewrite Z.sub_simpl_r.
+ rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x))));
+ auto with zarith.
+ rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x))));
+ auto with zarith.
+ rewrite <- 2 Zpower_exp; auto with zarith.
+ rewrite !Z.add_sub_assoc, !Z.add_simpl_l.
+ rewrite ZnZ.spec_zdigits.
+ rewrite pow2_pos_minus_1 by (red; auto).
+ apply ZnZ.spec_head0; auto with zarith.
+ Qed.
+
+ Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x].
+ Proof.
+ intros. destruct (Z_lt_ge_dec 0 [x]).
+ symmetry. apply Z.log2_unique. apply spec_pos.
+ apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith.
+ rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith.
+ generalize (spec_pos x); auto with zarith.
+ Qed.
+
+ Lemma log2_digits_head0 : forall x, 0 < [x] ->
+ [log2 x] = Zpos (digits x) - [head0 x] - 1.
+ Proof.
+ intros. rewrite log2_fold.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
+ auto with zarith.
+ intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x).
+ rewrite ZnZ.spec_sub_carry.
+ intros.
+ generalize (head0_zdigits n x H).
+ generalize (ZnZ.spec_to_Z (ZnZ.head0 x)).
+ generalize (ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))).
+ rewrite ZnZ.spec_zdigits. intros. apply Zmod_small.
+ auto with zarith.
+ Qed.
+
+ (** * Right shift *)
+
+ Local Notation shiftrn := (fun n =>
+ let op := dom_op n in
+ let zdigits := ZnZ.zdigits op in
+ let sub_c := ZnZ.sub_c in
+ let add_mul_div := ZnZ.add_mul_div in
+ let zzero := ZnZ.zero in
+ fun x p => match sub_c zdigits p with
+ | C0 d => reduce n (add_mul_div d zzero x)
+ | C1 _ => zero
+ end).
+
+ Definition shiftr : t -> t -> t := Eval red_t in
+ same_level shiftrn.
+
+ Lemma shiftr_fold : shiftr = same_level shiftrn.
+ Proof. red_t; reflexivity. Qed.
+
+ Lemma div_pow2_bound :forall x y z,
+ 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z.
+ Proof.
+ intros x y z HH HH1 HH2.
+ split; auto with zarith.
+ apply Z.le_lt_trans with (2 := HH2); auto with zarith.
+ apply Zdiv_le_upper_bound; auto with zarith.
+ pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.
+ apply Z.mul_le_mono_nonneg_l; auto.
+ apply Z.pow_le_mono_r; auto with zarith.
+ rewrite Z.pow_0_r; ring.
+ Qed.
+
+ Theorem spec_shiftr_pow2 : forall x n,
+ [shiftr x n] = [x] / 2 ^ [n].
+ Proof.
+ intros x y. rewrite shiftr_fold. apply spec_same_level. clear x y.
+ intros n x p. simpl.
+ assert (Hx := ZnZ.spec_to_Z x).
+ assert (Hy := ZnZ.spec_to_Z p).
+ generalize (ZnZ.spec_sub_c (ZnZ.zdigits (dom_op n)) p).
+ case ZnZ.sub_c; intros d H; unfold interp_carry in *; simpl.
+ (** Subtraction without underflow : [ p <= digits ] *)
+ rewrite spec_reduce.
+ rewrite ZnZ.spec_zdigits in H.
+ rewrite ZnZ.spec_add_mul_div by auto with zarith.
+ rewrite ZnZ.spec_0, Z.mul_0_l, Z.add_0_l.
+ rewrite Zmod_small.
+ f_equal. f_equal. auto with zarith.
+ split. auto with zarith.
+ apply div_pow2_bound; auto with zarith.
+ (** Subtraction with underflow : [ digits < p ] *)
+ rewrite ZnZ.spec_0. symmetry.
+ apply Zdiv_small.
+ split; auto with zarith.
+ apply Z.lt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith.
+ unfold base. apply Z.pow_le_mono_r; auto with zarith.
+ rewrite ZnZ.spec_zdigits in H.
+ generalize (ZnZ.spec_to_Z d); auto with zarith.
+ Qed.
+
+ Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Proof.
+ intros.
+ now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos.
+ Qed.
+
+ (** * Left shift *)
+
+ (** First an unsafe version, working correctly only if
+ the representation is large enough *)
+
+ Local Notation unsafe_shiftln := (fun n =>
+ let op := dom_op n in
+ let add_mul_div := ZnZ.add_mul_div in
+ let zero := ZnZ.zero in
+ fun x p => reduce n (add_mul_div p x zero)).
+
+ Definition unsafe_shiftl : t -> t -> t := Eval red_t in
+ same_level unsafe_shiftln.
+
+ Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_unsafe_shiftl_aux : forall x p K,
+ 0 <= K ->
+ [x] < 2^K ->
+ [p] + K <= Zpos (digits x) ->
+ [unsafe_shiftl x p] = [x] * 2 ^ [p].
+ Proof.
+ intros x p.
+ rewrite unsafe_shiftl_fold. rewrite digits_level.
+ apply spec_same_level_dep.
+ intros n m z z' r LE H K HK H1 H2. apply (H K); auto.
+ transitivity (Zpos (ZnZ.digits (dom_op n))); auto.
+ apply digits_dom_op_incr; auto.
+ clear x p.
+ intros n x p K HK Hx Hp. simpl. rewrite spec_reduce.
+ destruct (ZnZ.spec_to_Z x).
+ destruct (ZnZ.spec_to_Z p).
+ rewrite ZnZ.spec_add_mul_div by (omega with *).
+ rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r.
+ apply Zmod_small. unfold base.
+ split; auto with zarith.
+ rewrite Z.mul_comm.
+ apply Z.lt_le_trans with (2^(ZnZ.to_Z p + K)).
+ rewrite Zpower_exp; auto with zarith.
+ apply Z.mul_lt_mono_pos_l; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
+ Qed.
+
+ Theorem spec_unsafe_shiftl: forall x p,
+ [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p].
+ Proof.
+ intros.
+ destruct (Z.eq_dec [x] 0) as [EQ|NEQ].
+ (* [x] = 0 *)
+ apply spec_unsafe_shiftl_aux with 0; auto with zarith.
+ now rewrite EQ.
+ rewrite spec_head00 in *; auto with zarith.
+ (* [x] <> 0 *)
+ apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith.
+ generalize (spec_pos (log2 x)); auto with zarith.
+ destruct (spec_log2_pos x); auto with zarith.
+ rewrite log2_digits_head0; auto with zarith.
+ generalize (spec_pos x); auto with zarith.
+ Qed.
+
+ (** Then we define a function doubling the size of the representation
+ but without changing the value of the number. *)
+
+ Local Notation double_size_n := (fun n =>
+ let zero := ZnZ.zero in
+ fun x => mk_t_S n (WW zero x)).
+
+ Definition double_size : t -> t := Eval red_t in
+ iter_t double_size_n.
+
+ Lemma double_size_fold : double_size = iter_t double_size_n.
+ Proof. red_t; reflexivity. Qed.
- 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
+ Lemma double_size_level : forall x, level (double_size x) = S (level x).
+ Proof.
+ intros x. rewrite double_size_fold; unfold level at 2. destr_t x as (n,x).
+ apply mk_t_S_level.
+ Qed.
+
+ Theorem spec_double_size_digits:
+ forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)).
+ Proof.
+ intros x. rewrite ! digits_level, double_size_level.
+ rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower,
+ Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+ ring.
+ Qed.
+
+ Theorem spec_double_size: forall x, [double_size x] = [x].
+ Proof.
+ intros x. rewrite double_size_fold. destr_t x as (n,x).
+ rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_0. auto with zarith.
+ Qed.
+
+ Theorem spec_double_size_head0:
+ forall x, 2 * [head0 x] <= [head0 (double_size x)].
+ Proof.
+ intros x.
+ assert (F1:= spec_pos (head0 x)).
+ assert (F2: 0 < Zpos (digits x)).
+ red; auto.
+ assert (HH := spec_pos x). Z.le_elim HH.
+ generalize HH; rewrite <- (spec_double_size x); intros HH1.
+ case (spec_head0 x HH); intros _ HH2.
+ case (spec_head0 _ HH1).
+ rewrite (spec_double_size x); rewrite (spec_double_size_digits x).
+ intros HH3 _.
+ case (Z.le_gt_cases ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4.
+ absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto.
+ apply Z.le_ngt.
+ apply Z.mul_le_mono_nonneg_r; auto with zarith.
+ apply Z.pow_le_mono_r; auto; auto with zarith.
+ assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).
+ { apply Z.le_succ_l in HH. change (1 <= [x]) in HH.
+ Z.le_elim HH.
+ - apply Z.mul_le_mono_pos_r with (2 ^ 1); auto with zarith.
+ rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith.
+ rewrite Z.sub_add.
+ apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2).
+ apply Z.mul_le_mono_nonneg_l; auto with zarith.
+ rewrite Z.pow_1_r; auto with zarith.
+ - apply Z.pow_le_mono_r; auto with zarith.
+ case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.
+ absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith.
+ rewrite <- HH; rewrite Z.mul_1_r.
+ apply Z.pow_le_mono_r; auto with zarith. }
+ rewrite (Z.mul_comm 2).
+ rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Z.pow_2_r.
+ apply Z.lt_le_trans with (2 := HH3).
+ rewrite <- Z.mul_assoc.
+ replace (2 * Zpos (digits x) - 1) with
+ ((Zpos (digits x) - 1) + (Zpos (digits x))).
+ rewrite Zpower_exp; auto with zarith.
+ apply Zmult_lt_compat2; auto with zarith.
+ split; auto with zarith.
+ apply Z.mul_pos_pos; auto with zarith.
+ rewrite Pos2Z.inj_xO; ring.
+ apply Z.lt_le_incl; auto.
+ repeat rewrite spec_head00; auto.
+ rewrite spec_double_size_digits.
+ rewrite Pos2Z.inj_xO; auto with zarith.
+ rewrite spec_double_size; auto.
+ Qed.
+
+ Theorem spec_double_size_head0_pos:
+ forall x, 0 < [head0 (double_size x)].
+ Proof.
+ intros x.
+ assert (F := Pos2Z.is_pos (digits x)).
+ assert (F0 := spec_pos (head0 (double_size x))).
+ Z.le_elim F0; auto.
+ assert (F1 := spec_pos (head0 x)).
+ Z.le_elim F1.
+ apply Z.lt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.
+ assert (F3 := spec_pos x).
+ Z.le_elim F3.
+ generalize F3; rewrite <- (spec_double_size x); intros F4.
+ absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).
+ { apply Z.le_ngt.
+ apply Z.pow_le_mono_r; auto with zarith.
+ rewrite Pos2Z.inj_xO; auto with zarith. }
+ case (spec_head0 x F3).
+ rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH.
+ apply Z.le_lt_trans with (2 := HH).
+ case (spec_head0 _ F4).
+ rewrite (spec_double_size x); rewrite (spec_double_size_digits x).
+ rewrite <- F0; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto.
+ generalize F1; rewrite (spec_head00 _ (eq_sym F3)); auto with zarith.
+ Qed.
+
+ (** Finally we iterate [double_size] enough before [unsafe_shiftl]
+ in order to get a fully correct [shiftl]. *)
+
+ Definition shiftl_aux_body cont x n :=
+ match compare n (head0 x) with
+ Gt => cont (double_size x) n
+ | _ => unsafe_shiftl x n
end.
- Theorem spec_shiftl_aux_body: forall n p x cont,
+ Theorem spec_shiftl_aux_body: forall n x p 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].
+ [cont x n] = [x] * 2 ^ [n]) ->
+ [shiftl_aux_body cont x n] = [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.
+ intros n x p cont H1 H2; unfold shiftl_aux_body.
+ rewrite spec_compare; case Z.compare_spec; 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.
+ rewrite Z.add_comm; rewrite Zpower_exp; auto with zarith.
+ apply Z.le_trans with (2 := spec_double_size_head0 x).
+ rewrite Z.pow_1_r; apply Z.mul_le_mono_nonneg_l; auto with zarith.
Qed.
- Fixpoint shiftl_aux p cont n x {struct p} :=
+ Fixpoint shiftl_aux p cont x n :=
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.
+ (fun x n => match p with
+ | xH => cont x n
+ | xO p => shiftl_aux p (shiftl_aux p cont) x n
+ | xI p => shiftl_aux p (shiftl_aux p cont) x n
+ end) x n.
- Theorem spec_shiftl_aux: forall p q n x cont,
+ Theorem spec_shiftl_aux: forall p q x n 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].
+ [cont x n] = [x] * 2 ^ [n]) ->
+ [shiftl_aux p cont x n] = [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.
+ intros p Hrec q x n 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.
+ rewrite <- Pos.add_assoc.
+ rewrite Pos2Z.inj_add; auto.
intros x3 H5; apply H2.
- rewrite Zpos_xI.
+ rewrite Pos2Z.inj_xI.
replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));
auto.
- repeat rewrite Zpos_plus_distr; ring.
+ rewrite !Pos2Z.inj_add; 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.
+ apply Z.le_trans with (2 := H3); auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
intros x2 H4; apply Hrec with (p + q)%positive; auto.
intros x3 H5; apply H2.
- rewrite (Zpos_xO p).
+ rewrite (Pos2Z.inj_xO p).
replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));
auto.
- repeat rewrite Zpos_plus_distr; ring.
+ rewrite Pos2Z.inj_add; ring.
intros q n x cont H1 H2.
apply spec_shiftl_aux_body with (q); auto.
- rewrite Zplus_comm; auto.
+ rewrite Z.add_comm; auto.
Qed.
- Definition shiftl n x :=
+ Definition shiftl x n :=
shiftl_aux_body
(shiftl_aux_body
- (shiftl_aux (digits n) unsafe_shiftl)) n x.
+ (shiftl_aux (digits n) unsafe_shiftl)) x n.
- Theorem spec_shiftl: forall n x,
- [shiftl n x] = [x] * 2 ^ [n].
+ Theorem spec_shiftl_pow2 : forall x n,
+ [shiftl x n] = [x] * 2 ^ [n].
Proof.
- intros n x; unfold shiftl, shiftl_aux_body.
- generalize (spec_compare_aux n (head0 x)); case compare; intros H.
+ intros x n; unfold shiftl, shiftl_aux_body.
+ rewrite spec_compare; case Z.compare_spec; 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.
+ rewrite spec_compare; case Z.compare_spec; 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)).
+ apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)).
replace (2 ^ 1) with (2 * 1).
- apply Zmult_le_compat_l; auto with zarith.
+ apply Z.mul_le_mono_nonneg_l; auto with zarith.
generalize (spec_double_size_head0_pos x); auto with zarith.
- rewrite Zpower_1_r; ring.
+ rewrite Z.pow_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.
+ apply Z.le_trans with (2 := H2).
+ apply Z.le_trans with (2 ^ Zpos (digits n)); auto with zarith.
case (spec_digits n); auto with zarith.
- apply Zpower_le_monotone; auto with zarith.
+ apply Z.pow_le_mono_r; auto with zarith.
Qed.
+ Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Proof.
+ intros.
+ now rewrite spec_shiftl_pow2, Z.shiftl_mul_pow2 by apply spec_pos.
+ Qed.
- (** * Zero and One *)
+ (** Other bitwise operations *)
- Theorem spec_0: [zero] = 0.
+ Definition testbit x n := odd (shiftr x n).
+
+ Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
Proof.
- exact (spec_0 w0_spec).
+ intros. unfold testbit. symmetry.
+ rewrite spec_odd, spec_shiftr. apply Z.testbit_odd.
Qed.
- Theorem spec_1: [one] = 1.
+ Definition div2 x := shiftr x one.
+
+ Lemma spec_div2: forall x, [div2 x] = Z.div2 [x].
+ Proof.
+ intros. unfold div2. symmetry.
+ rewrite spec_shiftr, spec_1. apply Z.div2_spec.
+ Qed.
+
+ (** TODO : provide efficient versions instead of just converting
+ from/to N (see with Laurent) *)
+
+ Definition lor x y := of_N (N.lor (to_N x) (to_N y)).
+ Definition land x y := of_N (N.land (to_N x) (to_N y)).
+ Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)).
+ Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)).
+
+ Lemma spec_land: forall x y, [land x y] = Z.land [x] [y].
Proof.
- exact (spec_1 w0_spec).
+ intros x y. unfold land. rewrite spec_of_N. unfold to_N.
+ generalize (spec_pos x), (spec_pos y).
+ destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
Qed.
+ Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Proof.
+ intros x y. unfold lor. rewrite spec_of_N. unfold to_N.
+ generalize (spec_pos x), (spec_pos y).
+ destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Qed.
+
+ Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Proof.
+ intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N.
+ generalize (spec_pos x), (spec_pos y).
+ destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Qed.
+
+ Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Proof.
+ intros x y. unfold lxor. rewrite spec_of_N. unfold to_N.
+ generalize (spec_pos x), (spec_pos y).
+ destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Qed.
End Make.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 67a62c40..278cc8bf 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,100 +8,88 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NMake_gen.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*S NMake_gen.ml : this file generates NMake_gen.v *)
-(*S NMake_gen.ml : this file generates NMake.v *)
-
-(*s The two parameters that control the generation: *)
+(*s The parameter that control the generation: *)
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 ? *)
-
(*s Some utilities *)
-let t = "t"
-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 =
- if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"
+let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ 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",
- let's use instead a magical hack *)
+let rec iter_str_gen n f = if n < 0 then "" else (iter_str_gen (n-1) f) ^ (f n)
-(* Standard printer, with a final newline *)
-let pr s = Printf.printf (s^^"\n")
-(* Printing to /dev/null *)
-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
-(* Printer for admitted parts : prints iff gen_proof is false *)
-let pa = if not gen_proof then pr else pn
-(* Same as before, but without the final newline *)
-let pr0 = Printf.printf
-let pp0 = if gen_proof then pr0 else pn
+let rec iter_name i j base sep =
+ if i >= j then base^(string_of_int i)
+ else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j)
+let pr s = Printf.printf (s^^"\n")
(*s The actual printing *)
let _ =
- pr "(************************************************************************)";
- pr "(* v * The Coq Proof Assistant / The Coq Development Team *)";
- pr "(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)";
- pr "(* \\VV/ **************************************************************)";
- pr "(* // * This file is distributed under the terms of the *)";
- pr "(* * GNU Lesser General Public License Version 2.1 *)";
- pr "(************************************************************************)";
- pr "(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)";
- pr "(************************************************************************)";
- pr "";
- pr "(** * NMake *)";
- 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 "";
- pr "Require Import BigNumPrelude ZArith CyclicAxioms";
- pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic";
- pr " Wf_nat StreamMemo.";
- pr "";
- pr "Module Make (Import W0:CyclicType).";
- pr "";
+pr
+"(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \\VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
+(************************************************************************)
- pr " Definition w0 := W0.w.";
- for i = 1 to size do
- pr " Definition w%i := zn2z w%i." i (i-1)
- done;
- pr "";
+(** * NMake_gen *)
- pr " Definition w0_op := W0.w_op.";
- for i = 1 to 3 do
- pr " Definition w%i_op := mk_zn2z_op w%i_op." i (i-1)
- done;
- for i = 4 to size + 3 do
- pr " Definition w%i_op := mk_zn2z_op_karatsuba w%i_op." i (i-1)
- done;
- pr "";
+(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)
+
+(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)
+
+Require Import BigNumPrelude ZArith Ndigits CyclicAxioms
+ DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic
+ Wf_nat StreamMemo.
+
+Module Make (W0:CyclicType) <: NAbstract.
+
+ (** * The word types *)
+";
+
+pr " Local Notation w0 := W0.t.";
+for i = 1 to size do
+ pr " Definition w%i := zn2z w%i." i (i-1)
+done;
+pr "";
+
+pr " (** * The operation type classes for the word types *)
+";
+
+pr " Local Notation w0_op := W0.ops.";
+for i = 1 to min 3 size do
+ pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
+done;
+for i = 4 to size do
+ pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
+done;
+for i = size+1 to size+3 do
+ pr " Instance w%i_op : ZnZ.Ops (word w%i %i) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
+done;
+pr "";
pr " Section Make_op.";
- pr " Variable mk : forall w', znz_op w' -> znz_op (zn2z w').";
+ pr " Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w').";
pr "";
- pr " Fixpoint make_op_aux (n:nat) : znz_op (word w%i (S n)):=" size;
- pr " match n return znz_op (word w%i (S n)) with" size;
+ pr " Fixpoint make_op_aux (n:nat) : ZnZ.Ops (word w%i (S n)):=" size;
+ pr " match n return ZnZ.Ops (word w%i (S n)) with" size;
pr " | O => w%i_op" (size+1);
pr " | S n1 =>";
- pr " match n1 return znz_op (word w%i (S (S n1))) with" size;
+ pr " match n1 return ZnZ.Ops (word w%i (S (S n1))) with" size;
pr " | O => w%i_op" (size+2);
pr " | S n2 =>";
- pr " match n2 return znz_op (word w%i (S (S (S n2)))) with" size;
+ pr " match n2 return ZnZ.Ops (word w%i (S (S (S n2)))) with" size;
pr " | O => w%i_op" (size+3);
pr " | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))";
pr " end";
@@ -110,2565 +98,912 @@ let _ =
pr "";
pr " End Make_op.";
pr "";
- pr " Definition omake_op := make_op_aux mk_zn2z_op_karatsuba.";
+ pr " Definition omake_op := make_op_aux mk_zn2z_ops_karatsuba.";
pr "";
pr "";
pr " Definition make_op_list := dmemo_list _ omake_op.";
pr "";
- pr " Definition make_op n := dmemo_get _ omake_op n make_op_list.";
- pr "";
- pr " Lemma make_op_omake: forall n, make_op n = omake_op n.";
- pr " intros n; unfold make_op, make_op_list.";
- pr " refine (dmemo_get_correct _ _ _).";
- pr " Qed.";
+ pr " Instance make_op n : ZnZ.Ops (word w%i (S n))" size;
+ pr " := dmemo_get _ omake_op n make_op_list.";
pr "";
- pr " Inductive %s_ :=" t;
- 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;
- pr "";
- pr " Definition %s := %s_." t t;
- pr "";
- pr " Definition w_0 := w0_op.(znz_0).";
- pr "";
+pr " Ltac unfold_ops := unfold omake_op, make_op_aux, w%i_op, w%i_op." (size+3) (size+2);
- for i = 0 to size do
- pr " Definition one%i := w%i_op.(znz_1)." i i
- done;
- pr "";
+pr
+"
+ Lemma make_op_omake: forall n, make_op n = omake_op n.
+ Proof.
+ intros n; unfold make_op, make_op_list.
+ refine (dmemo_get_correct _ _ _).
+ Qed.
+ Theorem make_op_S: forall n,
+ make_op (S n) = mk_zn2z_ops_karatsuba (make_op n).
+ Proof.
+ intros n. do 2 rewrite make_op_omake.
+ revert n. fix IHn 1.
+ do 3 (destruct n; [unfold_ops; reflexivity|]).
+ simpl mk_zn2z_ops_karatsuba. simpl word in *.
+ rewrite <- (IHn n). auto.
+ Qed.
- pr " Definition zero := %s0 w_0." c;
- pr " Definition one := %s0 one0." c;
- pr "";
+ (** * The main type [t], isomorphic with [exists n, word w0 n] *)
+";
- pr " Definition to_Z x :=";
- pr " match x with";
+ pr " Inductive t' :=";
for i = 0 to size do
- pr " | %s%i wx => w%i_op.(znz_to_Z) wx" c i i
+ pr " | N%i : w%i -> t'" i i
done;
- pr " | %sn n wx => (make_op n).(znz_to_Z) wx" c;
- pr " end.";
+ pr " | Nn : forall n, word w%i (S n) -> t'." size;
pr "";
-
- pr " Open Scope Z_scope.";
- pr " Notation \"[ x ]\" := (to_Z x).";
- pr "";
-
- pr " Definition to_N x := Zabs_N (to_Z x).";
+ pr " Definition t := t'.";
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 " znz_op (word ww n) :=";
- 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 " end.";
- pp "";
- pp " (* Simplification by rewriting for nmake_op *)";
- 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.";
- pp "";
-
-
- pr " (* Eval and extend functions for each level *)";
- 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
- pr " Let extend%i := DoubleBase.extend (WW w_0)." i
- else
- pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i;
- done;
+ pr " Bind Scope abstract_scope with t t'.";
pr "";
-
- 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.";
- pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits.";
- pp " rewrite <- Hrec; auto.";
- pp " Qed.";
- pp "";
- 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.";
- pp " intros n; elim n; auto; clear n.";
- pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.";
- pp " rewrite <- Hrec; auto.";
- pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto.";
- pp " Qed.";
- pp "";
-
-
- 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.";
- pp " Qed.";
- pp "";
-
-
- pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,";
- pp " znz_to_Z (nmake_op ww ww_op (S n)) (WW xh xl) =";
- pp " znz_to_Z (nmake_op ww ww_op n) xh *";
- pp " base (znz_digits (nmake_op ww ww_op n)) +";
- pp " znz_to_Z (nmake_op ww ww_op n) xl.";
- pp " Proof.";
- pp " auto.";
- pp " Qed.";
- pp "";
-
- pp " Theorem make_op_S: forall n,";
- pp " make_op (S n) = mk_zn2z_op_karatsuba (make_op n).";
- pp " intro n.";
- pp " do 2 rewrite make_op_omake.";
- pp " pattern n; apply lt_wf_ind; clear n.";
- pp " intros n; case n; clear n.";
- pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2);
- pp " intros n; case n; clear n.";
- pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3);
- pp " intros n; case n; clear n.";
- pp " intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2);
- pp " intros n Hrec.";
- pp " change (omake_op (S (S (S (S n))))) with";
- pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op (S n))))).";
- pp " change (omake_op (S (S (S n)))) with";
- 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 "";
-
-
- 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 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 "";
- 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 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 "";
-
- 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)
- 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)
- done;
- pp "";
-
- pp " Let wn_spec: forall n, znz_spec (make_op n).";
- pp " intros n; elim n; clear n.";
- pp " exact w%i_spec." (size + 1);
- pp " intros n Hrec; rewrite make_op_S.";
- pp " exact (mk_znz2_karatsuba_spec Hrec).";
- pp " Qed.";
- pp "";
-
- for i = 0 to size do
- pr " Definition w%i_eq0 := w%i_op.(znz_eq0)." i i;
- pr " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True." i i c i;
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; unfold w%i_eq0, to_Z; generalize (spec_eq0 w%i_spec x);" i i;
- pp " case znz_eq0; auto.";
- pp " Qed.";
- pr "";
- done;
+ pr " (** * A generic toolbox for building and deconstructing [t] *)";
pr "";
-
- 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;
- 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 " Proof.";
- pp " intros n; exact (nmake_double n w%i w%i_op)." i i;
- pp " Qed.";
- pp "";
- done;
-
- 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 " Proof.";
- if j == 0 then
- if i == 0 then
- pp " auto."
- else
- begin
- pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1);
- pp " auto.";
- pp " unfold nmake_op; auto.";
- end
- else
- begin
- pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1);
- pp " auto.";
- pp " rewrite digits_nmake.";
- pp " rewrite digits_w%in%i." i (j - 1);
- pp " auto.";
- 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 " Proof.";
- if j == 0 then
- pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
- else
- begin
- pp " intros x; case x.";
- pp " auto.";
- pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (i + j);
- pp " rewrite digits_w%in%i." i (j - 1);
- pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1);
- pp " unfold eval%in, nmake_op%i." i i;
- pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1);
- end;
- 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;
- if j == 0 then
- begin
- pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j);
- pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1);
- pp " rewrite (spec_0 w%i_spec); auto." (i + j);
- end
- else
- begin
- pp " intros x; change (extend%i %i x) with (WW (znz_0 w%i_op) (extend%i %i x))." i j (i + j) i (j - 1);
- pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1);
- pp " rewrite (spec_0 w%i_spec)." (i + j);
- pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j);
- pp " intros HH; rewrite <- HH; auto.";
- end;
- pp " Qed.";
- pp "";
- end;
- done;
-
- pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1);
- pp " Proof.";
- pp " apply trans_equal with (xO (znz_digits w%i_op))." size;
- pp " auto.";
- pp " rewrite digits_nmake.";
- pp " rewrite digits_w%in%i." i (size - i);
- pp " auto.";
- 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 " Proof.";
- pp " intros x; case x.";
- pp " auto.";
- pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 1);
- pp " rewrite digits_w%in%i." i (size - i);
- pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i);
- pp " unfold eval%in, nmake_op%i." i i;
- pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i);
- 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 " intros x; case x.";
- pp " auto.";
- pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2);
- pp " rewrite digits_w%in%i." i (size + 1 - i);
- pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1);
- pp " unfold eval%in, nmake_op%i." i i;
- pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i);
- pp " Qed.";
- pp "";
- done;
-
- pp " Let digits_w%in: forall n," size;
- pp " znz_digits (make_op n) = znz_digits (nmake_op _ w%i_op (S n))." size;
- pp " intros n; elim n; clear n.";
- pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
- pp " rewrite nmake_op_S; apply sym_equal; auto.";
- pp " intros n Hrec.";
- pp " replace (znz_digits (make_op (S n))) with (xO (znz_digits (make_op n))).";
- pp " rewrite Hrec.";
- pp " rewrite nmake_op_S; apply sym_equal; auto.";
- pp " rewrite make_op_S; apply sym_equal; auto.";
- pp " Qed.";
- pp "";
-
- 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.";
- pp " unfold to_Z, eval%in, nmake_op%i." size size;
- pp " rewrite make_op_S; rewrite nmake_op_S; auto.";
- pp " intros xh xl.";
- pp " unfold to_Z in Hrec |- *.";
- pp " rewrite znz_to_Z_n.";
- pp " rewrite digits_w%in." size;
- pp " repeat rewrite Hrec.";
- pp " unfold eval%in, nmake_op%i." size size;
- pp " apply sym_equal; rewrite nmake_op_S; auto.";
- 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 " 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.";
- pp " change (make_op 0) with w%i_op." (size + 1);
- pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto." (size + 1) size;
- pp " intros n Hrec x.";
- pp " change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size;
- pp " unfold to_Z in Hrec |- *; rewrite znz_to_Z_n; auto.";
- pp " rewrite <- Hrec.";
- pp " replace (znz_to_Z (make_op n) W0) with 0; auto.";
- pp " case n; auto; intros; rewrite make_op_S; auto.";
- pp " Qed.";
- pp "";
-
- pr " Theorem spec_pos: forall x, 0 <= [x].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; clear x.";
- for i = 0 to size do
- pp " intros x; case (spec_to_Z w%i_spec x); auto." i;
- done;
- pp " intros n x; case (spec_to_Z (wn_spec n) x); auto.";
- pp " Qed.";
+ pr " Local Notation SizePlus n := %sn%s."
+ (iter_str size "(S ") (iter_str size ")");
+ pr " Local Notation Size := (SizePlus O).";
pr "";
- pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c;
- pp " intros n; elim n; auto.";
- pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.";
- pp " unfold to_Z.";
- pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
- pp " Qed.";
- pp "";
- pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
- pp " Proof.";
- pp " intros n x; unfold to_Z.";
- pp " rewrite znz_to_Z_n.";
- pp " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x)).";
- pp " apply (f_equal2 Zplus); auto.";
- pp " case n; auto.";
- pp " intros n1; rewrite make_op_S; auto.";
- pp " Qed.";
- 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;
- pp " Proof.";
- pp " induction m; auto.";
- pp " intros n x; simpl extend_tr.";
- pp " simpl plus; rewrite spec_extendn0_0; auto.";
- pp " Qed.";
- pp "";
- pp " Let spec_cast_l: forall n m x1,";
- pp " [%sn (Max.max n m)" c;
- pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =";
- pp " [%sn n x1]." c;
- pp " Proof.";
- pp " intros n m x1; case (diff_r n m); simpl castm.";
- pp " rewrite spec_extend_tr; auto.";
- pp " Qed.";
- pp "";
- pp " Let spec_cast_r: forall n m x1,";
- pp " [%sn (Max.max n m)" c;
- pp " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =";
- pp " [%sn m x1]." c;
- pp " Proof.";
- pp " intros n m x1; case (diff_l n m); simpl castm.";
- pp " rewrite spec_extend_tr; auto.";
- pp " Qed.";
- pp "";
-
-
- pr " Section LevelAndIter.";
- pr "";
- pr " Variable res: Type.";
- pr " Variable xxx: res.";
- pr " Variable P: Z -> Z -> res -> Prop.";
- pr " (* Abstraction function for each level *)";
- for i = 0 to size do
- pr " Variable f%i: w%i -> w%i -> res." i i i;
- pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i;
- pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i;
- pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i;
- if i == size then
- begin
- pp " Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i;
- pp " Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i;
- end
- else
- begin
- pp " Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i;
- pp " Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i;
- end;
- pr "";
- done;
- pr " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size;
- pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c;
- pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size;
- pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c;
- pr "";
- pr " (* Special zero functions *)";
- pr " Variable f0t: t_ -> res.";
- pp " Variable Pf0t: forall x, P 0 [x] (f0t x).";
- pr " Variable ft0: t_ -> res.";
- pp " Variable Pft0: forall x, P [x] 0 (ft0 x).";
+ pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1);
pr "";
-
- pr " (* We level the two arguments before applying *)";
- pr " (* the functions at each leval *)";
- pr " Definition same_level (x y: t_): res :=";
- pr0 " Eval lazy zeta beta iota delta [";
- for i = 0 to size do
- pr0 "extend%i " i;
- done;
- pr "";
- pr " DoubleBase.extend DoubleBase.extend_aux";
- pr " ] in";
- pr " match x, y with";
+ pr " Definition dom_t n := match n with";
for i = 0 to size do
- for j = 0 to i - 1 do
- pr " | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1);
- done;
- pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
- for j = i + 1 to size do
- 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 (extend%i %i wx)) wy" c i c size i (size - i - 1);
+ pr " | %i => w%i" i i;
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 (extend%i %i wy))" c c i size i (size - i - 1);
- done;
- pr " | %sn n wx, Nn m wy =>" c;
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " fnn mn";
- pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
- pr " (castm (diff_l n m) (extend_tr wy (fst d)))";
- pr " end.";
+ pr " | %sn => word w%i n" (if size=0 then "" else "SizePlus ") size;
+ pr " end.";
pr "";
- pp " Lemma spec_same_level: forall x y, P [x] [y] (same_level x y).";
- pp " Proof.";
- pp " intros x; case x; clear x; unfold 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; rewrite spec_extend%in%i; apply Pf%i." j i i;
- done;
- pp " intros y; apply Pf%i." i;
- for j = i + 1 to size do
- pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
- done;
- if i == size then
- pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
- 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
- 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 " rewrite <- (spec_cast_r n m y); apply Pfnn.";
- pp " Qed.";
- pp "";
-
- pr " (* We level the two arguments before applying *)";
- pr " (* the functions at each level (special zero case) *)";
- pr " Definition same_level0 (x y: t_): res :=";
- pr0 " Eval lazy zeta beta iota delta [";
- for i = 0 to size do
- pr0 "extend%i " i;
- done;
- pr "";
- pr " DoubleBase.extend DoubleBase.extend_aux";
- pr " ] in";
- pr " match x with";
- for i = 0 to size do
- pr " | %s%i wx =>" c i;
- if i == 0 then
- pr " if w0_eq0 wx then f0t y else";
- pr " match y with";
- for j = 0 to i - 1 do
- pr " | %s%i wy =>" c j;
- 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;
- pr " | %s%i wy => f%i wx wy" c i i;
- for j = i + 1 to size do
- 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 (extend%i %i wx)) wy" c size i (size - i - 1);
- pr" end";
- done;
- pr " | %sn n wx =>" c;
- pr " match y with";
- for i = 0 to size do
- pr " | %s%i wy =>" c i;
- 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 (extend%i %i wy))" size i (size - i - 1);
- done;
- pr " | %sn m wy =>" c;
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " fnn mn";
- pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
- pr " (castm (diff_l n m) (extend_tr wy (fst d)))";
- pr " end";
- pr " end.";
- pr "";
+pr
+" Instance dom_op n : ZnZ.Ops (dom_t n) | 10.
+ Proof.
+ do_size (destruct n; [simpl;auto with *|]).
+ unfold dom_t. auto with *.
+ Defined.
+";
- pp " Lemma spec_same_level0: forall x y, P [x] [y] (same_level0 x y).";
- pp " Proof.";
- pp " intros x; case x; clear x; unfold same_level0.";
- for i = 0 to size do
- pp " intros x.";
- if i == 0 then
- begin
- pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H.";
- pp " intros y; rewrite H; apply Pf0t.";
- pp " clear H.";
- end;
- pp " intros y; case y; clear y.";
- for j = 0 to i - 1 do
- pp " intros y.";
- if j == 0 then
- begin
- pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
- pp " rewrite H; apply Pft0.";
- pp " clear H.";
- end;
- pp " rewrite spec_extend%in%i; apply Pf%i." j i i;
- done;
- pp " intros y; apply Pf%i." i;
- for j = i + 1 to size do
- pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
- done;
- if i == size then
- pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
- 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.";
+ pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A) : t -> A :=";
for i = 0 to size do
- pp " intros y.";
- if i = 0 then
- begin
- pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
- pp " rewrite H; apply Pft0.";
- pp " clear H.";
- end;
- if i == size then
- pp " rewrite (spec_extend%in n); apply Pfnn." size
- else
- pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
+ pr " let f%i := f %i in" i i;
done;
- 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 :=";
- pr0 " Eval lazy zeta beta iota delta [";
+ pr " let fn n := f (SizePlus (S n)) in";
+ pr " fun x => match x with";
for i = 0 to size do
- pr0 "extend%i " i;
+ pr " | N%i wx => f%i wx" i i;
done;
- pr "";
- pr " DoubleBase.extend DoubleBase.extend_aux";
- pr " ] in";
- pr " match x, y with";
- for i = 0 to size do
- for j = 0 to i - 1 do
- pr " | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1);
- done;
- pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
- for j = i + 1 to size do
- 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 (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 (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;
+ pr " | Nn n wx => fn n wx";
pr " end.";
pr "";
- 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.";
- for i = 0 to size do
- pp " intros x y; case y; clear y.";
- for j = 0 to i - 1 do
- pp " intros y; rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
- done;
- pp " intros y; apply Pf%i." i;
- for j = i + 1 to size do
- pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
- done;
- if i == size then
- pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
- 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
- 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.";
- pp " Qed.";
- pp "";
-
-
- pr " (* We iter the smaller argument with the bigger (zero case) *)";
- pr " Definition iter0 (x y: t_): res :=";
- pr0 " Eval lazy zeta beta iota delta [";
- for i = 0 to size do
- pr0 "extend%i " i;
- done;
- pr "";
- pr " DoubleBase.extend DoubleBase.extend_aux";
- pr " ] in";
- pr " match x with";
- for i = 0 to size do
- pr " | %s%i wx =>" c i;
- if i == 0 then
- pr " if w0_eq0 wx then f0t y else";
- pr " match y with";
- for j = 0 to i - 1 do
- pr " | %s%i wy =>" c j;
- if j == 0 then
- pr " if w0_eq0 wy then ft0 x else";
- pr " fn%i %i wx wy" j (i - j - 1);
- done;
- pr " | %s%i wy => f%i wx wy" c i i;
- for j = i + 1 to size do
- 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 (extend%i %i wx) wy" c size i (size - i - 1);
- pr " end";
- done;
- pr " | %sn n wx =>" c;
- pr " match y with";
+ pr " Definition mk_t (n:nat) : dom_t n -> t :=";
+ pr " match n as n' return dom_t n' -> t with";
for i = 0 to size do
- pr " | %s%i wy =>" c i;
- 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 (extend%i %i wy)" size i (size - i - 1);
+ pr " | %i => N%i" i i;
done;
- pr " | %sn m wy => fnm n m wx wy" c;
- pr " end";
+ pr " | %s(S n) => Nn n" (if size=0 then "" else "SizePlus ");
pr " end.";
pr "";
- pp " Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y).";
- pp " Proof.";
- pp " intros x; case x; clear x; unfold iter0.";
- for i = 0 to size do
- pp " intros x.";
- if i == 0 then
- begin
- pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H.";
- pp " intros y; rewrite H; apply Pf0t.";
- pp " clear H.";
- end;
- pp " intros y; case y; clear y.";
- for j = 0 to i - 1 do
- pp " intros y.";
- if j == 0 then
- begin
- pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
- pp " rewrite H; apply Pft0.";
- pp " clear H.";
- end;
- pp " rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
- done;
- pp " intros y; apply Pf%i." i;
- for j = i + 1 to size do
- pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
- done;
- if i == size then
- pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
- 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
- pp " intros y.";
- if i = 0 then
- begin
- pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
- pp " rewrite H; apply Pft0.";
- pp " clear H.";
- end;
- if i == size then
- pp " rewrite spec_eval%in; apply Pfn%i." size size
- 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.";
- pp " Qed.";
- pp "";
-
-
- pr " End LevelAndIter.";
- pr "";
+pr
+" Definition level := iter_t (fun n _ => n).
+ Inductive View_t : t -> Prop :=
+ Mk_t : forall n (x : dom_t n), View_t (mk_t n x).
+
+ Lemma destr_t : forall x, View_t x.
+ Proof.
+ intros x. generalize (Mk_t (level x)). destruct x; simpl; auto.
+ Defined.
+
+ Lemma iter_mk_t : forall A (f:forall n, dom_t n -> A),
+ forall n x, iter_t f (mk_t n x) = f n x.
+ Proof.
+ do_size (destruct n; try reflexivity).
+ Qed.
+
+ (** * Projection to ZArith *)
+
+ Definition to_Z : t -> Z :=
+ Eval lazy beta iota delta [iter_t dom_t dom_op] in
+ iter_t (fun _ x => ZnZ.to_Z x).
+
+ Notation \"[ x ]\" := (to_Z x).
+
+ Theorem spec_mk_t : forall n (x:dom_t n), [mk_t n x] = ZnZ.to_Z x.
+ Proof.
+ intros. change to_Z with (iter_t (fun _ x => ZnZ.to_Z x)).
+ rewrite iter_mk_t; auto.
+ Qed.
+
+ (** * Regular make op, without memoization or karatsuba
+
+ This will normally never be used for actual computations,
+ but only for specification purpose when using
+ [word (dom_t n) m] intermediate values. *)
+
+ Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) :
+ ZnZ.Ops (word ww n) :=
+ match n return ZnZ.Ops (word ww n) with
+ O => ww_op
+ | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)
+ end.
+
+ Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
+
+ Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,
+ nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).
+ Proof.
+ auto.
+ Qed.
+
+ Theorem digits_nmake_S :forall n ww (w_op: ZnZ.Ops ww),
+ ZnZ.digits (nmake_op _ w_op (S n)) =
+ xO (ZnZ.digits (nmake_op _ w_op n)).
+ Proof.
+ auto.
+ Qed.
+
+ Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww),
+ ZnZ.digits (nmake_op _ w_op n) = Pos.shiftl_nat (ZnZ.digits w_op) n.
+ Proof.
+ induction n. auto.
+ intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto.
+ Qed.
+
+ Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),
+ ZnZ.to_Z (Ops:=nmake_op _ w_op n) =
+ @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n.
+ Proof.
+ intros n; elim n; auto; clear n.
+ intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.
+ rewrite <- Hrec; auto.
+ unfold DoubleBase.double_wB; rewrite <- digits_nmake; auto.
+ Qed.
+
+ Theorem nmake_WW: forall ww ww_op n xh xl,
+ (ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) =
+ ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh *
+ base (ZnZ.digits (nmake_op ww ww_op n)) +
+ ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl)%%Z.
+ Proof.
+ auto.
+ Qed.
+
+ (** * The specification proofs for the word operators *)
+";
+
+ if size <> 0 then
+ pr " Typeclasses Opaque %s." (iter_name 1 size "w" "");
+ pr "";
+
+ pr " Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
+ for i = 1 to min 3 size do
+ pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
+ done;
+ for i = 4 to size do
+ pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
+ done;
+ pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." (size+1) (size+1) size;
+
+
+pr "
+ Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).
+ Proof.
+ induction n.
+ rewrite make_op_omake; simpl; auto with *.
+ rewrite make_op_S. exact (mk_zn2z_specs_karatsuba IHn).
+ Qed.
+
+ Instance dom_spec n : ZnZ.Specs (dom_op n) | 10.
+ Proof.
+ do_size (destruct n; auto with *). apply wn_spec.
+ Qed.
+
+ Let make_op_WW : forall n x y,
+ (ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =
+ ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n))
+ + ZnZ.to_Z (Ops:=make_op n) y)%%Z.
+ Proof.
+ intros n x y; rewrite make_op_S; auto.
+ Qed.
+
+ (** * Zero *)
+
+ Definition zero0 : w0 := ZnZ.zero.
+
+ Definition zeron n : dom_t n :=
+ match n with
+ | O => zero0
+ | SizePlus (S n) => W0
+ | _ => W0
+ end.
+
+ Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z.
+ Proof.
+ do_size (destruct n; [exact ZnZ.spec_0|]).
+ destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0.
+ Qed.
+
+ (** * Digits *)
+
+ Lemma digits_make_op_0 : forall n,
+ ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op Size)) (S n).
+ Proof.
+ induction n.
+ auto.
+ replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n))).
+ rewrite IHn; auto.
+ rewrite make_op_S; auto.
+ Qed.
+
+ Lemma digits_make_op : forall n,
+ ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)).
+ Proof.
+ intros. rewrite digits_make_op_0.
+ replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto).
+ rewrite Pshiftl_nat_plus. auto.
+ Qed.
+
+ Lemma digits_dom_op : forall n,
+ ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) n.
+ Proof.
+ do_size (destruct n; try reflexivity).
+ exact (digits_make_op n).
+ Qed.
+
+ Lemma digits_dom_op_nmake : forall n m,
+ ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m).
+ Proof.
+ intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_nat_plus.
+ Qed.
+
+ (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)].
+
+ These two types are provably equal, but not convertible,
+ hence we need some work. We now avoid using generic casts
+ (i.e. rewrite via proof of equalities in types), since
+ proving things with them is a mess.
+ *)
+
+ Definition succ_t n : zn2z (dom_t n) -> dom_t (S n) :=
+ match n with
+ | SizePlus (S _) => fun x => x
+ | _ => fun x => x
+ end.
+
+ Lemma spec_succ_t : forall n x,
+ ZnZ.to_Z (succ_t n x) =
+ zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+ Proof.
+ do_size (destruct n ; [reflexivity|]).
+ intros. simpl. rewrite make_op_S. simpl. auto.
+ Qed.
+
+ Definition pred_t n : dom_t (S n) -> zn2z (dom_t n) :=
+ match n with
+ | SizePlus (S _) => fun x => x
+ | _ => fun x => x
+ end.
+
+ Lemma succ_pred_t : forall n x, succ_t n (pred_t n x) = x.
+ Proof.
+ do_size (destruct n ; [reflexivity|]). reflexivity.
+ Qed.
+
+ (** We can hence project from [zn2z (dom_t n)] to [t] : *)
+
+ Definition mk_t_S n (x : zn2z (dom_t n)) : t :=
+ mk_t (S n) (succ_t n x).
+
+ Lemma spec_mk_t_S : forall n x,
+ [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+ Proof.
+ intros. unfold mk_t_S. rewrite spec_mk_t. apply spec_succ_t.
+ Qed.
+
+ Lemma mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
+ Proof.
+ intros. unfold mk_t_S, level. rewrite iter_mk_t; auto.
+ Qed.
+
+ (** * Conversion from [word (dom_t n) m] to [dom_t (m+n)].
+
+ Things are more complex here. We start with a naive version
+ that breaks zn2z-trees and reconstruct them. Doing this is
+ quite unfortunate, but I don't know how to fully avoid that.
+ (cast someday ?). Then we build an optimized version where
+ all basic cases (n<=6 or m<=7) are nicely handled.
+ *)
+
+ Definition zn2z_map {A} {B} (f:A->B) (x:zn2z A) : zn2z B :=
+ match x with
+ | W0 => W0
+ | WW h l => WW (f h) (f l)
+ end.
+
+ Lemma zn2z_map_id : forall A f (x:zn2z A), (forall u, f u = u) ->
+ zn2z_map f x = x.
+ Proof.
+ destruct x; auto; intros.
+ simpl; f_equal; auto.
+ Qed.
+
+ (** The naive version *)
+
+ Fixpoint plus_t n m : word (dom_t n) m -> dom_t (m+n) :=
+ match m as m' return word (dom_t n) m' -> dom_t (m'+n) with
+ | O => fun x => x
+ | S m => fun x => succ_t _ (zn2z_map (plus_t n m) x)
+ end.
+
+ Theorem spec_plus_t : forall n m (x:word (dom_t n) m),
+ ZnZ.to_Z (plus_t n m x) = eval n m x.
+ Proof.
+ unfold eval.
+ induction m.
+ simpl; auto.
+ intros.
+ simpl plus_t; simpl plus. rewrite spec_succ_t.
+ destruct x.
+ simpl; auto.
+ fold word in w, w0.
+ simpl. rewrite 2 IHm. f_equal. f_equal. f_equal.
+ apply digits_dom_op_nmake.
+ Qed.
+
+ Definition mk_t_w n m (x:word (dom_t n) m) : t :=
+ mk_t (m+n) (plus_t n m x).
+
+ Theorem spec_mk_t_w : forall n m (x:word (dom_t n) m),
+ [mk_t_w n m x] = eval n m x.
+ Proof.
+ intros. unfold mk_t_w. rewrite spec_mk_t. apply spec_plus_t.
+ Qed.
+
+ (** The optimized version.
+
+ NB: the last particular case for m could depend on n,
+ but it's simplier to just expand everywhere up to m=7
+ (cf [mk_t_w'] later).
+ *)
+
+ Definition plus_t' n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+ match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+ | SizePlus (S n') as n => plus_t n
+ | _ as n =>
+ fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+ | SizePlus (S (S m')) as m => plus_t n m
+ | _ => fun x => x
+ end
+ end.
+
+ Lemma plus_t_equiv : forall n m x,
+ plus_t' n m x = plus_t n m x.
+ Proof.
+ (do_size try destruct n); try reflexivity;
+ (do_size try destruct m); try destruct m; try reflexivity;
+ simpl; symmetry; repeat (intros; apply zn2z_map_id; trivial).
+ Qed.
+
+ Lemma spec_plus_t' : forall n m x,
+ ZnZ.to_Z (plus_t' n m x) = eval n m x.
+ Proof.
+ intros; rewrite plus_t_equiv. apply spec_plus_t.
+ Qed.
+
+ (** Particular cases [Nk x] = eval i j x with specific k,i,j
+ can be solved by the following tactic *)
+
+ Ltac solve_eval :=
+ intros; rewrite <- spec_plus_t'; unfold to_Z; simpl dom_op; reflexivity.
+
+ (** The last particular case that remains useful *)
+
+ Lemma spec_eval_size : forall n x, [Nn n x] = eval Size (S n) x.
+ Proof.
+ induction n.
+ solve_eval.
+ destruct x as [ | xh xl ].
+ simpl. unfold eval. rewrite make_op_S. rewrite nmake_op_S. auto.
+ simpl word in xh, xl |- *.
+ unfold to_Z in *. rewrite make_op_WW.
+ unfold eval in *. rewrite nmake_WW.
+ f_equal; auto.
+ f_equal; auto.
+ f_equal.
+ rewrite <- digits_dom_op_nmake. rewrite plus_comm; auto.
+ Qed.
+
+ (** An optimized [mk_t_w].
+
+ We could say mk_t_w' := mk_t _ (plus_t' n m x)
+ (TODO: WHY NOT, BTW ??).
+ Instead we directly define functions for all intersting [n],
+ reverting to naive [mk_t_w] at places that should normally
+ never be used (see [mul] and [div_gt]).
+ *)
+";
+
+for i = 0 to size-1 do
+let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in
+pr
+" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
+ match m return word w%i (S m) -> t with
+ | %s as p => mk_t_w %i (S p)
+ | p => mk_t (%i+p)
+ end.
+" i i pattern i (i+1)
+done;
+
+pr
+" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
+ match n return (forall m, word (dom_t n) (S m) -> t) with";
+for i = 0 to size-1 do pr " | %i => mk_t_%iw" i i done;
+pr
+" | Size => Nn
+ | _ as n' => fun m => mk_t_w n' (S m)
+ end.
+";
+
+pr
+" Ltac solve_spec_mk_t_w' :=
+ rewrite <- spec_plus_t';
+ match goal with _ : word (dom_t ?n) ?m |- _ => apply (spec_mk_t (n+m)) end.
+
+ Theorem spec_mk_t_w' :
+ forall n m x, [mk_t_w' n m x] = eval n (S m) x.
+ Proof.
+ intros.
+ repeat (apply spec_mk_t_w || (destruct n;
+ [repeat (apply spec_mk_t_w || (destruct m; [solve_spec_mk_t_w'|]))|])).
+ apply spec_eval_size.
+ Qed.
+
+ (** * Extend : injecting [dom_t n] into [word (dom_t n) (S m)] *)
+
+ Definition extend n m (x:dom_t n) : word (dom_t n) (S m) :=
+ DoubleBase.extend_aux m (WW (zeron n) x).
+
+ Lemma spec_extend : forall n m x,
+ [mk_t n x] = eval n (S m) (extend n m x).
+ Proof.
+ intros. unfold eval, extend.
+ rewrite spec_mk_t.
+ assert (H : forall (x:dom_t n),
+ (ZnZ.to_Z (zeron n) * base (ZnZ.digits (dom_op n)) + ZnZ.to_Z x =
+ ZnZ.to_Z x)%%Z).
+ clear; intros; rewrite spec_zeron; auto.
+ rewrite <- (@DoubleBase.spec_extend _
+ (WW (zeron n)) (ZnZ.digits (dom_op n)) ZnZ.to_Z H m x).
+ simpl. rewrite digits_nmake, <- nmake_double. auto.
+ Qed.
+
+ (** A particular case of extend, used in [same_level]:
+ [extend_size] is [extend Size] *)
+
+ Definition extend_size := DoubleBase.extend (WW (W0:dom_t Size)).
+
+ Lemma spec_extend_size : forall n x, [mk_t Size x] = [Nn n (extend_size n x)].
+ Proof.
+ intros. rewrite spec_eval_size. apply (spec_extend Size n).
+ Qed.
+
+ (** Misc results about extensions *)
+
+ Let spec_extend_WW : forall n x,
+ [Nn (S n) (WW W0 x)] = [Nn n x].
+ Proof.
+ intros n x.
+ set (N:=SizePlus (S n)).
+ change ([Nn (S n) (extend N 0 x)]=[mk_t N x]).
+ rewrite (spec_extend N 0).
+ solve_eval.
+ Qed.
+
+ Let spec_extend_tr: forall m n w,
+ [Nn (m + n) (extend_tr w m)] = [Nn n w].
+ Proof.
+ induction m; auto.
+ intros n x; simpl extend_tr.
+ simpl plus; rewrite spec_extend_WW; auto.
+ Qed.
+
+ Let spec_cast_l: forall n m x1,
+ [Nn n x1] =
+ [Nn (Max.max n m) (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))].
+ Proof.
+ intros n m x1; case (diff_r n m); simpl castm.
+ rewrite spec_extend_tr; auto.
+ Qed.
+
+ Let spec_cast_r: forall n m x1,
+ [Nn m x1] =
+ [Nn (Max.max n m) (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))].
+ Proof.
+ intros n m x1; case (diff_l n m); simpl castm.
+ rewrite spec_extend_tr; auto.
+ Qed.
+
+ Ltac unfold_lets :=
+ match goal with
+ | h : _ |- _ => unfold h; clear h; unfold_lets
+ | _ => idtac
+ end.
+
+ (** * [same_level]
+
+ Generic binary operator construction, by extending the smaller
+ argument to the level of the other.
+ *)
+
+ Section SameLevel.
+
+ Variable res: Type.
+ Variable P : Z -> Z -> res -> Prop.
+ Variable f : forall n, dom_t n -> dom_t n -> res.
+ Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
+";
+
+for i = 0 to size do
+pr " Let f%i : w%i -> w%i -> res := f %i." i i i i
+done;
+pr
+" Let fn n := f (SizePlus (S n)).
+
+ Let Pf' :
+ forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
+ Proof.
+ intros. subst. rewrite 2 spec_mk_t. apply Pf.
+ Qed.
+";
+
+let ext i j s =
+ if j <= i then s else Printf.sprintf "(extend %i %i %s)" i (j-i-1) s
+in
+
+pr " Notation same_level_folded := (fun x y => match x, y with";
+for i = 0 to size do
+ for j = 0 to size do
+ pr " | N%i wx, N%i wy => f%i %s %s" i j (max i j) (ext i j "wx") (ext j i "wy")
+ done;
+ pr " | N%i wx, Nn m wy => fn m (extend_size m %s) wy" i (ext i size "wx")
+done;
+for i = 0 to size do
+ pr " | Nn n wx, N%i wy => fn n wx (extend_size n %s)" i (ext i size "wy")
+done;
+pr
+" | Nn n wx, Nn m wy =>
+ let mn := Max.max n m in
+ let d := diff n m in
+ fn mn
+ (castm (diff_r n m) (extend_tr wx (snd d)))
+ (castm (diff_l n m) (extend_tr wy (fst d)))
+ end).
+";
+
+pr
+" Definition same_level := Eval lazy beta iota delta
+ [ DoubleBase.extend DoubleBase.extend_aux extend zeron ]
+ in same_level_folded.
+
+ Lemma spec_same_level_0: forall x y, P [x] [y] (same_level x y).
+ Proof.
+ change same_level with same_level_folded. unfold_lets.
+ destruct x, y; apply Pf'; simpl mk_t; rewrite <- ?spec_extend_size;
+ match goal with
+ | |- context [ extend ?n ?m _ ] => apply (spec_extend n m)
+ | |- context [ castm _ _ ] => apply spec_cast_l || apply spec_cast_r
+ | _ => reflexivity
+ end.
+ Qed.
+
+ End SameLevel.
+
+ Arguments same_level [res] f x y.
+
+ Theorem spec_same_level_dep :
+ forall res
+ (P : nat -> Z -> Z -> res -> Prop)
+ (Pantimon : forall n m z z' r, n <= m -> P m z z' r -> P n z z' r)
+ (f : forall n, dom_t n -> dom_t n -> res)
+ (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
+ forall x y, P (level x) [x] [y] (same_level f x y).
+ Proof.
+ intros res P Pantimon f Pf.
+ set (f' := fun n x y => (n, f n x y)).
+ set (P' := fun z z' r => P (fst r) z z' (snd r)).
+ assert (FST : forall x y, level x <= fst (same_level f' x y))
+ by (destruct x, y; simpl; omega with * ).
+ assert (SND : forall x y, same_level f x y = snd (same_level f' x y))
+ by (destruct x, y; reflexivity).
+ intros. eapply Pantimon; [eapply FST|].
+ rewrite SND. eapply (@spec_same_level_0 _ P' f'); eauto.
+ Qed.
+
+ (** * [iter]
+
+ Generic binary operator construction, by splitting the larger
+ argument in blocks and applying the smaller argument to them.
+ *)
+
+ Section Iter.
+
+ Variable res: Type.
+ Variable P: Z -> Z -> res -> Prop.
+
+ Variable f : forall n, dom_t n -> dom_t n -> res.
+ Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
+
+ Variable fd : forall n m, dom_t n -> word (dom_t n) (S m) -> res.
+ Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res.
+ Variable Pfd : forall n m x y, P (ZnZ.to_Z x) (eval n (S m) y) (fd n m x y).
+ Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y).
+
+ Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
+ Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).
+
+ Let Pf' :
+ forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
+ Proof.
+ intros. subst. rewrite 2 spec_mk_t. apply Pf.
+ Qed.
+
+ Let Pfd' : forall n m x y u v, u = [mk_t n x] -> v = eval n (S m) y ->
+ P u v (fd n m x y).
+ Proof.
+ intros. subst. rewrite spec_mk_t. apply Pfd.
+ Qed.
+
+ Let Pfg' : forall n m x y u v, u = eval n (S m) x -> v = [mk_t n y] ->
+ P u v (fg n m x y).
+ Proof.
+ intros. subst. rewrite spec_mk_t. apply Pfg.
+ Qed.
+";
+
+for i = 0 to size do
+pr " Let f%i := f %i." i i
+done;
+
+for i = 0 to size do
+pr " Let f%in := fd %i." i i;
+pr " Let fn%i := fg %i." i i;
+done;
+
+pr " Notation iter_folded := (fun x y => match x, y with";
+for i = 0 to size do
+ for j = 0 to size do
+ pr " | N%i wx, N%i wy => f%s wx wy" i j
+ (if i = j then string_of_int i
+ else if i < j then string_of_int i ^ "n " ^ string_of_int (j-i-1)
+ else "n" ^ string_of_int j ^ " " ^ string_of_int (i-j-1))
+ done;
+ pr " | N%i wx, Nn m wy => f%in m %s wy" i size (ext i size "wx")
+done;
+for i = 0 to size do
+ pr " | Nn n wx, N%i wy => fn%i n wx %s" i size (ext i size "wy")
+done;
+pr
+" | Nn n wx, Nn m wy => fnm n m wx wy
+ end).
+";
+
+pr
+" Definition iter := Eval lazy beta iota delta
+ [extend DoubleBase.extend DoubleBase.extend_aux zeron]
+ in iter_folded.
+
+ Lemma spec_iter: forall x y, P [x] [y] (iter x y).
+ Proof.
+ change iter with iter_folded; unfold_lets.
+ destruct x; destruct y; apply Pf' || apply Pfd' || apply Pfg' || apply Pfnm;
+ simpl mk_t;
+ match goal with
+ | |- ?x = ?x => reflexivity
+ | |- [Nn _ _] = _ => apply spec_eval_size
+ | |- context [extend ?n ?m _] => apply (spec_extend n m)
+ | _ => idtac
+ end;
+ unfold to_Z; rewrite <- spec_plus_t'; simpl dom_op; reflexivity.
+ Qed.
+
+ End Iter.
+";
+
+pr
+" Definition switch
+ (P:nat->Type)%s
+ (fn:forall n, P n) n :=
+ match n return P n with"
+ (iter_str_gen size (fun i -> Printf.sprintf "(f%i:P %i)" i i));
+for i = 0 to size do pr " | %i => f%i" i i done;
+pr
+" | n => fn n
+ end.
+";
+
+pr
+" Lemma spec_switch : forall P (f:forall n, P n) n,
+ switch P %sf n = f n.
+ Proof.
+ repeat (destruct n; try reflexivity).
+ Qed.
+" (iter_str_gen size (fun i -> Printf.sprintf "(f %i) " i));
+
+pr
+" (** * [iter_sym]
+
+ A variant of [iter] for symmetric functions, or pseudo-symmetric
+ functions (when f y x can be deduced from f x y).
+ *)
+
+ Section IterSym.
+
+ Variable res: Type.
+ Variable P: Z -> Z -> res -> Prop.
+
+ Variable f : forall n, dom_t n -> dom_t n -> res.
+ Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y).
+
+ Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res.
+ Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y).
+
+ Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
+ Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).
+
+ Variable opp: res -> res.
+ Variable Popp : forall u v r, P u v r -> P v u (opp r).
+";
+
+for i = 0 to size do
+pr " Let f%i := f %i." i i
+done;
+
+for i = 0 to size do
+pr " Let fn%i := fg %i." i i;
+done;
+
+pr " Let f' := switch _ %s f." (iter_name 0 size "f" "");
+pr " Let fg' := switch _ %s fg." (iter_name 0 size "fn" "");
+
+pr
+" Local Notation iter_sym_folded :=
+ (iter res f' (fun n m x y => opp (fg' n m y x)) fg' fnm).
+
+ Definition iter_sym :=
+ Eval lazy beta zeta iota delta [iter f' fg' switch] in iter_sym_folded.
+
+ Lemma spec_iter_sym: forall x y, P [x] [y] (iter_sym x y).
+ Proof.
+ intros. change iter_sym with iter_sym_folded. apply spec_iter; clear x y.
+ unfold_lets.
+ intros. rewrite spec_switch. auto.
+ intros. apply Popp. unfold_lets. rewrite spec_switch; auto.
+ intros. unfold_lets. rewrite spec_switch; auto.
+ auto.
+ Qed.
+
+ End IterSym.
+
+ (** * Reduction
+
+ [reduce] can be used instead of [mk_t], it will choose the
+ lowest possible level. NB: We only search and remove leftmost
+ W0's via ZnZ.eq0, any non-W0 block ends the process, even
+ if its value is 0.
+ *)
+
+ (** First, a direct version ... *)
+
+ Fixpoint red_t n : dom_t n -> t :=
+ match n return dom_t n -> t with
+ | O => N0
+ | S n => fun x =>
+ let x' := pred_t n x in
+ reduce_n1 _ _ (N0 zero0) ZnZ.eq0 (red_t n) (mk_t_S n) x'
+ end.
+
+ Lemma spec_red_t : forall n x, [red_t n x] = [mk_t n x].
+ Proof.
+ induction n.
+ reflexivity.
+ intros.
+ simpl red_t. unfold reduce_n1.
+ rewrite <- (succ_pred_t n x) at 2.
+ remember (pred_t n x) as x'.
+ rewrite spec_mk_t, spec_succ_t.
+ destruct x' as [ | xh xl]. simpl. apply ZnZ.spec_0.
+ generalize (ZnZ.spec_eq0 xh); case ZnZ.eq0; intros H.
+ rewrite IHn, spec_mk_t. simpl. rewrite H; auto.
+ apply spec_mk_t_S.
+ Qed.
+
+ (** ... then a specialized one *)
+";
+
+for i = 0 to size do
+pr " Definition eq0%i := @ZnZ.eq0 _ w%i_op." i i;
+done;
+
+pr "
+ Definition reduce_0 := N0.";
+for i = 1 to size do
+ pr " Definition reduce_%i :=" i;
+ pr " Eval lazy beta iota delta [reduce_n1] in";
+ pr " reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i N%i." (i-1) (i-1) i
+done;
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Reduction *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- 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."
- (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 " Eval lazy beta iota delta [reduce_n1] in";
+ pr " reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i (Nn 0)." size size;
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 "";
-
- pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c;
- pp " Proof.";
- pp " intros x; unfold to_Z, reduce_0.";
- pp " auto.";
- pp " Qed.";
- pp "";
-
- for i = 1 to size + 1 do
- if i == size + 1 then
- pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c
- else
- pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i;
- pp " Proof.";
- 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 " case w%i_eq0; intros H1; auto." (i - 1);
- 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 "";
- done;
-
- pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c;
- pp " Proof.";
- pp " intros n; elim n; simpl reduce_n.";
- pp " intros x; rewrite <- spec_reduce_%i; auto." (size + 1);
- pp " intros n1 Hrec x; case x.";
- pp " unfold to_Z; rewrite make_op_S; auto.";
- pp " exact (spec_0 w0_spec).";
- pp " intros x1 y1; case x1; auto.";
- pp " rewrite Hrec.";
- pp " rewrite spec_extendn0_0; auto.";
- pp " Qed.";
- pp "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Successor *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_succ_c := w%i_op.(znz_succ_c)." i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_succ := w%i_op.(znz_succ)." i i
- done;
- pr "";
-
- pr " Definition succ x :=";
- pr " match x with";
- 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 " | 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 " | 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 " | C1 r => %sn (S n) (WW op.(znz_1) r)" c;
- pr " end";
- pr " end.";
- pr "";
-
- pr " Theorem spec_succ: forall n, [succ n] = [n] + 1.";
- pa " Admitted.";
- pp " Proof.";
- pp " intros n; case n; unfold succ, to_Z.";
- for i = 0 to size do
- pp " intros n1; generalize (spec_succ_c w%i_spec n1);" i;
- pp " unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto." i;
- 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;
- done;
- pp " intros k n1; generalize (spec_succ_c (wn_spec k) n1).";
- pp " unfold succ, to_Z; case znz_succ_c; auto.";
- 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.";
- pr "";
-
-
- pr " (***************************************************************)";
- pr " (* *)";
- 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 x y :=" i;
- pr " match w%i_add_c x y with" i;
- pr " | C0 r => %s%i r" c i;
- if i == size then
- pr " | C1 r => %sn 0 (WW one%i r)" c size
- else
- pr " | C1 r => %s%i (WW one%i r)" c (i + 1) i;
- pr " end.";
- pr "";
- done ;
- pr " Definition addn n (x y : word w%i (S n)) :=" size;
- pr " let op := make_op n in";
- pr " match op.(znz_add_c) x y with";
- pr " | C0 r => %sn n r" c;
- pr " | C1 r => %sn (S n) (WW op.(znz_1) r) end." c;
- pr "";
-
-
- for i = 0 to size do
- pp " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y]." i i c i c i;
- 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 " 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 "";
- 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 " 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.";
-
- pr " Definition add := Eval lazy beta delta [same_level] in";
- pr0 " (same_level t_ ";
- for i = 0 to size do
- pr0 "w%i_add " i;
- done;
- pr "addn).";
- pr "";
-
- pr " Theorem spec_add: forall x y, [add x y] = [x] + [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " unfold add.";
- pp " generalize (spec_same_level t_ (fun x y res => [res] = x + y)).";
- pp " unfold same_level; intros HH; apply HH; clear HH.";
- for i = 0 to size do
- pp " exact spec_w%i_add." i;
- done;
- pp " exact spec_wn_add.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Predecessor *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_pred_c := w%i_op.(znz_pred_c)." i i
- done;
- pr "";
-
- pr " Definition pred x :=";
- pr " match x with";
- 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 " | 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 " | C1 r => zero";
- pr " end";
- pr " end.";
- pr "";
-
- 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 " 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.";
- pp " case (spec_to_Z w%i_spec x1); intros HH1 HH2." i;
- pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5." i;
- 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 " 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.";
- pp " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2.";
- pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5.";
- 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 " 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 " 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 " 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 " (** * Subtraction *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_sub_c := w%i_op.(znz_sub_c)." i i
- done;
- pr "";
-
- 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;
- pr " | C1 r => zero";
- pr " end."
- done;
- pr "";
-
- pr " Definition subn n (x y : word w%i (S n)) :=" size;
- pr " let op := make_op n in";
- pr " match op.(znz_sub_c) x y with";
- pr " | C0 r => %sn n r" c;
- pr " | C1 r => N0 w_0";
- pr " end.";
- pr "";
-
- for i = 0 to size do
- 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 " intros x; auto."
- else
- pp " intros x; try rewrite spec_reduce_%i; auto." i;
- pp " unfold interp_carry; unfold zero, w_0, to_Z.";
- pp " rewrite (spec_0 w0_spec).";
- pp " case (spec_to_Z w%i_spec x); intros; auto with zarith." i;
- 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 " intros x; auto.";
- pp " unfold interp_carry, to_Z.";
- pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith.";
- pp " Qed.";
- pp "";
-
- pr " Definition sub := Eval lazy beta delta [same_level] in";
- pr0 " (same_level t_ ";
- for i = 0 to size do
- pr0 "w%i_sub " i;
- done;
- pr "subn).";
- pr "";
-
- pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " unfold sub.";
- pp " generalize (spec_same_level t_ (fun x y res => y <= x -> [res] = x - y)).";
- pp " unfold same_level; intros HH; apply HH; clear HH.";
- for i = 0 to size do
- pp " exact spec_w%i_sub." i;
- done;
- pp " exact spec_wn_sub.";
- pp " Qed.";
- pr "";
-
- for i = 0 to size do
- 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 " 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.";
- pp " Qed.";
- pp "";
- done;
-
- 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 " 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.";
- pp " Qed.";
- pp "";
-
- pr " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0.";
- pa " Admitted.";
- pp " Proof.";
- pp " unfold sub.";
- pp " generalize (spec_same_level t_ (fun x y res => x < y -> [res] = 0)).";
- pp " unfold same_level; intros HH; apply HH; clear HH.";
- for i = 0 to size do
- pp " exact spec_w%i_sub0." i;
- done;
- pp " exact spec_wn_sub0.";
- pp " Qed.";
- pr "";
-
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Comparison *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition compare_%i := w%i_op.(znz_compare)." i i;
- 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 " Definition comparenm n m wx wy :=";
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " let op := make_op mn in";
- pr " op.(znz_compare)";
- pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
- pr " (castm (diff_l n m) (extend_tr wy (fst d))).";
- pr "";
-
- 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 => CompOpp (comparen_%i (S n) y x))" i;
- pr " (fun n => comparen_%i (S n))" i;
- done;
- pr " comparenm).";
- 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 " 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;
- pp " end.";
- pp " Proof.";
- 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;
- pp " | Eq => eval%in n x = [%s%i y]" i c i;
- pp " | Lt => eval%in n x < [%s%i y]" i c i;
- pp " | Gt => eval%in n x > [%s%i y]" i c i;
- pp " end.";
- pp " intros n x y.";
- pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i;
- pp " apply spec_compare_mn_1.";
- pp " exact (spec_0 w%i_spec)." i;
- pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i);
- pp " exact (spec_to_Z w%i_spec)." i;
- pp " exact (spec_compare w%i_spec)." i;
- pp " exact (spec_compare w%i_spec)." i;
- pp " exact (spec_to_Z w%i_spec)." i;
- pp " Qed.";
- pp "";
- done;
-
- pp " Let spec_opp_compare: forall c (u v: Z),";
- pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->";
- pp " match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end.";
- pp " Proof.";
- pp " intros c u v; case c; unfold CompOpp; auto with zarith.";
- pp " Qed.";
- pp "";
-
-
- 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 " Eq => x = y";
- pp " | Lt => x < y";
- pp " | Gt => x > y";
- pp " end)";
- for i = 0 to size do
- pp " compare_%i" i;
- pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
- 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;
- 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;
- pp " intros n m x y; unfold comparenm.";
- pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y).";
- pp " unfold to_Z; apply (spec_compare (wn_spec (Max.max n m))).";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Multiplication *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_mul_c := w%i_op.(znz_mul_c)." i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_mul_add :=" i;
- pr " Eval lazy beta delta [w_mul_add] in";
- pr " @w_mul_add w%i %s w%i_succ w%i_add_c w%i_mul_c." i (pz i) i i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_0W := znz_0W w%i_op." i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_WW := znz_WW w%i_op." i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_mul_add_n1 :=" i;
- pr " @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add." i (pz i) i i i
- done;
- pr "";
-
- for i = 0 to size - 1 do
- pr " Let to_Z%i n :=" i;
- 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
- pr " | %i%s => fun x => %sn 0 x" j "%nat" c;
- pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
- end
- else
- pr " | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1)
- done;
- pr " | _ => fun _ => N0 w_0";
- pr " end.";
- pr "";
- done;
-
-
- for i = 0 to size - 1 do
- pp "Theorem to_Z%i_spec:" i;
- pp " forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = znz_to_Z (nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i;
- for j = 1 to size + 2 - i do
- pp " intros n; case n; clear n.";
- pp " unfold to_Z%i." i;
- pp " intros x H; rewrite spec_eval%in%i; auto." i j;
- done;
- pp " intros n x.";
- pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
- pp " Qed.";
- pp "";
- done;
-
-
- for i = 0 to size do
- pr " Definition w%i_mul n x y :=" i;
- pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i);
- if i == size then
- begin
- 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
- 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;
- pr "";
- done;
-
- pr " Definition mulnm n m x y :=";
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " let op := make_op mn in";
- pr " reduce_n (S mn) (op.(znz_mul_c)";
- pr " (castm (diff_r n m) (extend_tr x (snd d)))";
- pr " (castm (diff_l n m) (extend_tr y (fst d)))).";
- pr "";
-
- 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 n x y => w%i_mul n y x)" i;
- pr " w%i_mul" i;
- done;
- pr " mulnm";
- pr " (fun _ => N0 w_0)";
- pr " (fun _ => N0 w_0)";
- pr " ).";
- pr "";
- for i = 0 to size do
- pp " Let spec_w%i_mul_add: forall x y z," i;
- pp " let (q,r) := w%i_mul_add x y z in" i;
- pp " znz_to_Z w%i_op q * (base (znz_digits w%i_op)) + znz_to_Z w%i_op r =" i i i;
- pp " znz_to_Z w%i_op x * znz_to_Z w%i_op y + znz_to_Z w%i_op z :=" i i i ;
- pp " (spec_mul_add w%i_spec)." i;
- pp "";
- done;
-
- for i = 0 to size do
- pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i;
- pp " let (q,r) := w%i_mul_add_n1 n x y z in" i;
- pp " znz_to_Z w%i_op q * (base (znz_digits (nmake_op _ w%i_op n))) +" i i;
- pp " znz_to_Z (nmake_op _ w%i_op n) r =" i;
- pp " znz_to_Z (nmake_op _ w%i_op n) x * znz_to_Z w%i_op y +" i i;
- pp " znz_to_Z w%i_op z." i;
- pp " Proof.";
- pp " intros n x y z; unfold w%i_mul_add_n1." i;
- pp " rewrite nmake_double.";
- pp " rewrite digits_doubled.";
- pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i;
- pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i;
- pp " apply spec_double_mul_add_n1; auto.";
- if i == 0 then pp " exact (spec_0 w%i_spec)." i;
- pp " exact (spec_WW w%i_spec)." i;
- pp " exact (spec_0W w%i_spec)." i;
- pp " exact (spec_mul_add w%i_spec)." i;
- 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)) +";
- pp " znz_to_Z (nmake_op ww ww1 n) y.";
- 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 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
- 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;
- pp " Proof.";
- pp " intros n x y; unfold to_Z.";
- pp " rewrite <- (spec_mul_c (wn_spec n)).";
- 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 " forall n x y,";
- if i <> size then
- pp0 " Z_of_nat n <= %i -> " (size - i);
- pp " [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i;
- if i == size then
- pp " intros n x y; unfold w%i_mul." i
- else
- pp " intros n x y H; unfold w%i_mul." i;
- pp " generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i);
- pp " case w%i_mul_add_n1; intros x1 y1." i;
- pp " change (znz_to_Z (nmake_op _ w%i_op (S n)) x) with (eval%in (S n) x)." i i;
- pp " change (znz_to_Z w%i_op y) with ([%s%i y])." i c i;
- if i == 0 then
- pp " unfold w_0; rewrite (spec_0 w0_spec); rewrite Zplus_0_r."
- else
- pp " change (znz_to_Z w%i_op W0) with 0; rewrite Zplus_0_r." i;
- pp " intros H1; rewrite <- H1; clear H1.";
- 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
- 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
- else
- begin
- pp " rewrite to_Z%i_spec; auto with zarith." i;
- pp " rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i
- end;
- pp " rewrite nmake_op_WW; rewrite extend%in_spec; auto." i;
- 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 n x y => w%i_mul n y x)" i;
- pp " w%i_mul _ _ _" i;
- done;
- pp " mulnm _";
- pp " (fun _ => N0 w_0) _";
- pp " (fun _ => N0 w_0) _";
- pp " ).";
- for i = 0 to size do
- pp " intros x y; rewrite spec_reduce_%i." (i + 1);
- pp " unfold w%i_mul_c, to_Z." i;
- pp " generalize (spec_mul_c w%i_spec x y)." i;
- pp " intros HH; rewrite <- HH; clear HH; auto.";
- 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;
- 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;
- end;
- done;
- pp " intros n m x y; unfold mulnm.";
- pp " rewrite spec_reduce_n.";
- pp " rewrite <- (spec_cast_l n m x).";
- pp " rewrite <- (spec_cast_r n m y).";
- pp " rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto.";
- pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring.";
- pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Square *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_square_c := w%i_op.(znz_square_c)." i i
- done;
- pr "";
-
- pr " Definition square x :=";
- pr " match x with";
- pr " | %s0 wx => reduce_1 (w0_square_c wx)" c;
- for i = 1 to size - 1 do
- pr " | %s%i wx => %s%i (w%i_square_c wx)" c i c (i+1) i
- done;
- pr " | %s%i wx => %sn 0 (w%i_square_c wx)" c size c size;
- pr " | %sn n wx =>" c;
- pr " let op := make_op n in";
- pr " %sn (S n) (op.(znz_square_c) wx)" c;
- pr " end.";
- pr "";
-
- pr " Theorem spec_square: forall x, [square x] = [x] * [x].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; unfold square; clear x.";
- pp " intros x; rewrite spec_reduce_1; unfold to_Z.";
- pp " exact (spec_square_c w%i_spec x)." 0;
- for i = 1 to size do
- pp " intros x; unfold to_Z.";
- pp " exact (spec_square_c w%i_spec x)." i;
- done;
- pp " intros n x; unfold to_Z.";
- pp " rewrite make_op_S.";
- pp " exact (spec_square_c (wn_spec n) x).";
- pp "Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Square root *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_sqrt := w%i_op.(znz_sqrt)." i i
- done;
- pr "";
-
- pr " Definition sqrt x :=";
- pr " match x with";
- for i = 0 to size do
- pr " | %s%i wx => reduce_%i (w%i_sqrt wx)" c i i i;
- done;
- pr " | %sn n wx =>" c;
- pr " let op := make_op n in";
- pr " reduce_n n (op.(znz_sqrt) wx)";
- pr " end.";
- pr "";
-
- pr " Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; unfold sqrt; case x; clear x.";
- for i = 0 to size do
- pp " intros x; rewrite spec_reduce_%i; exact (spec_sqrt w%i_spec x)." i i;
- done;
- pp " intros n x; rewrite spec_reduce_n; exact (spec_sqrt (wn_spec n) x).";
- pp " Qed.";
- pr "";
-
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Division *)";
- 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 " 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_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 " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
- pp "";
-
- for i = 0 to size do
- pr " Definition w%i_divn1 n x y :=" i;
- pr " let (u, v) :=";
- pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i;
- pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i;
- pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i;
- pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i;
- if i == size then
- pr " (%sn _ u, %s%i v)." c c i
- else
- pr " (to_Z%i _ u, %s%i v)." i c i;
- done;
- pr "";
-
- 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 " [%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.";
- pp " rewrite spec_double_eval%in; unfold to_Z." i;
- pp " apply DoubleBase.spec_get_low.";
- pp " exact (spec_0 w%i_spec)." i;
- pp " exact (spec_to_Z w%i_spec)." i;
- pp " apply Zle_lt_trans with [%s%i y]; auto." c i;
- pp " rewrite <- spec_double_eval%in; auto." i;
- pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i;
- pp " Qed.";
- pp "";
- done;
-
- for i = 0 to size do
- pr " Let div_gt%i x y := let (u,v) := (w%i_div_gt x y) in (reduce_%i u, reduce_%i v)." i i i i;
- done;
- pr "";
-
-
- pr " Let div_gtnm n m wx wy :=";
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " let op := make_op mn in";
- pr " let (q, r):= op.(znz_div_gt)";
- pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
- pr " (castm (diff_l n m) (extend_tr wy (fst d))) in";
- pr " (reduce_n mn q, reduce_n mn r).";
- pr "";
-
- pr " Definition div_gt := Eval lazy beta delta [iter] in";
- 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;
- done;
- pr " div_gtnm).";
- pr "";
-
- pr " Theorem spec_div_gt: forall x y,";
- pr " [x] > [y] -> 0 < [y] ->";
- pr " let (q,r) := div_gt x y in";
- pr " [q] = [x] / [y] /\\ [r] = [x] mod [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " assert (FO:";
- 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 " let (q,r) := res in";
- pp " x = [q] * y + [r] /\\ 0 <= [r] < y)";
- 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;
- done;
- pp " div_gtnm _).";
- for i = 0 to size do
- pp " intros x y H1 H2; unfold div_gt%i, w%i_div_gt." i i;
- pp " generalize (spec_div_gt w%i_spec x y H1 H2); case znz_div_gt." i;
- pp " intros xx yy; repeat rewrite spec_reduce_%i; auto." i;
- if i == size then
- 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 " (DoubleBase.get_low %s (S n) y))." (pz i);
- pp0 "";
- for j = 0 to i do
- pp0 "unfold w%i; " (i-j);
- done;
- pp "case znz_div_gt.";
- pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i;
- pp " generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i;
- pp " unfold to_Z in H2; rewrite H5 in H4; auto with zarith.";
- if i == size then
- pp " intros n x y H2 H3."
- else
- pp " intros n x y H1 H2 H3.";
- pp " generalize";
- 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);
- done;
- pp "case double_divn1.";
- pp " intros xx yy H4.";
- if i == size then
- begin
- pp " repeat rewrite <- spec_double_eval%in in H4; auto." i;
- pp " rewrite spec_eval%in; auto." i;
- end
- else
- begin
- pp " rewrite to_Z%i_spec; auto with zarith." i;
- pp " repeat rewrite <- spec_double_eval%in in H4; auto." i;
- end;
- done;
- pp " intros n m x y H1 H2; unfold div_gtnm.";
- pp " generalize (spec_div_gt (wn_spec (Max.max n m))";
- pp " (castm (diff_r n m)";
- pp " (extend_tr x (snd (diff n m))))";
- pp " (castm (diff_l n m)";
- pp " (extend_tr y (fst (diff n m))))).";
- pp " case znz_div_gt.";
- pp " intros xx yy HH.";
- pp " repeat rewrite spec_reduce_n.";
- pp " rewrite <- (spec_cast_l n m x).";
- pp " rewrite <- (spec_cast_r n m y).";
- pp " unfold to_Z; apply HH.";
- pp " rewrite <- (spec_cast_l n m x) in H1; auto.";
- pp " rewrite <- (spec_cast_r n m y) in H1; auto.";
- pp " rewrite <- (spec_cast_r n m y) in H2; auto.";
- pp " intros x y H1 H2; generalize (FO x y H1 H2); case div_gt.";
- pp " intros q r (H3, H4); split.";
- pp " apply (Zdiv_unique [x] [y] [q] [r]); auto.";
- pp " rewrite Zmult_comm; auto.";
- pp " apply (Zmod_unique [x] [y] [q] [r]); auto.";
- pp " rewrite Zmult_comm; auto.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Modulo *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i
- done;
- pr "";
-
- for i = 0 to size do
- pr " Definition w%i_modn1 :=" i;
- pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i;
- pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i;
- pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i;
- done;
- pr "";
-
- pr " Let mod_gtnm n m wx wy :=";
- pr " let mn := Max.max n m in";
- pr " let d := diff n m in";
- pr " let op := make_op mn in";
- pr " reduce_n mn (op.(znz_mod_gt)";
- pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
- pr " (castm (diff_l n m) (extend_tr wy (fst d)))).";
- pr "";
-
- pr " Definition mod_gt := Eval lazy beta delta[iter] in";
- 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);
- pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i;
- done;
- 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 " 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_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 " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
- pp "";
-
- pr " Theorem spec_mod_gt:";
- pr " forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " refine (spec_iter _ (fun x y res => x > y -> 0 < y ->";
- pp " [res] = x mod y)";
- for i = 0 to size do
- pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i;
- pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i);
- pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i;
- done;
- pp " mod_gtnm _).";
- for i = 0 to size do
- pp " intros x y H1 H2; rewrite spec_reduce_%i." i;
- pp " exact (spec_mod_gt w%i_spec x y H1 H2)." i;
- if i == size then
- pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
- else
- pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
- pp " unfold w%i_mod_gt." i;
- pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i;
- pp " unfold to_Z; apply (spec_mod_gt w%i_spec); auto." i;
- pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i;
- 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
- 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;
- done;
- pp " intros n m x y H1 H2; unfold mod_gtnm.";
- pp " repeat rewrite spec_reduce_n.";
- pp " rewrite <- (spec_cast_l n m x).";
- pp " rewrite <- (spec_cast_r n m y).";
- pp " unfold to_Z; apply (spec_mod_gt (wn_spec (Max.max n m))).";
- pp " rewrite <- (spec_cast_l n m x) in H1; auto.";
- pp " rewrite <- (spec_cast_r n m y) in H1; auto.";
- pp " rewrite <- (spec_cast_r n m y) in H2; auto.";
- pp " Qed.";
- pr "";
-
- pr " (** digits: a measure for gcd *)";
- pr "";
-
- pr " Definition digits x :=";
- pr " match x with";
- for i = 0 to size do
- pr " | %s%i _ => w%i_op.(znz_digits)" c i i;
- done;
- pr " | %sn n _ => (make_op n).(znz_digits)" c;
- pr " end.";
- pr "";
-
- pr " Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x).";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; clear x.";
- for i = 0 to size do
- pp " intros x; unfold to_Z, digits;";
- pp " generalize (spec_to_Z w%i_spec x); unfold base; intros H; exact H." i;
- done;
- pp " intros n x; unfold to_Z, digits;";
- pp " generalize (spec_to_Z (wn_spec n) x); unfold base; intros H; exact H.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Conversion *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- 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 " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p))).";
- pr " Proof.";
- pr " intros p; unfold pheight.";
- pr " assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1).";
- pr " intros x.";
- pr " assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith.";
- pr " rewrite <- inj_S.";
- pr " rewrite <- (fun x => S_pred x 0); auto with zarith.";
- pr " rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto.";
- pr " apply lt_le_trans with 1%snat; auto with zarith." "%";
- pr " exact (le_Pmult_nat x 1).";
- pr " rewrite F1; clear F1.";
- pr " assert (F2:= (get_height_correct (znz_digits w0_op) (plength p))).";
- pr " apply Zlt_le_trans with (Zpos (Psucc p)).";
- pr " rewrite Zpos_succ_morphism; auto with zarith.";
- pr " apply Zle_trans with (1 := plength_pred_correct (Psucc p)).";
- pr " rewrite Ppred_succ.";
- pr " apply Zpower_le_monotone; auto with zarith.";
- pr " Qed.";
- pr "";
-
- pr " Definition of_pos x :=";
- pr " let h := pheight x in";
- pr " match h with";
- for i = 0 to size do
- pr " | %i%snat => reduce_%i (snd (w%i_op.(znz_of_pos) x))" i "%" i i;
- done;
- pr " | _ =>";
- pr " let n := minus h %i in" (size + 1);
- pr " reduce_n n (snd ((make_op n).(znz_of_pos) x))";
- pr " end.";
- pr "";
-
- pr " Theorem spec_of_pos: forall x,";
- pr " [of_pos x] = Zpos x.";
- pa " Admitted.";
- pp " Proof.";
- pp " assert (F := spec_more_than_1_digit w0_spec).";
- pp " intros x; unfold of_pos; case_eq (pheight x).";
- for i = 0 to size do
- if i <> 0 then
- pp " intros n; case n; clear n.";
- pp " intros H1; rewrite spec_reduce_%i; unfold to_Z." i;
- pp " apply (znz_of_pos_correct w%i_spec)." i;
- pp " apply Zlt_le_trans with (1 := pheight_correct x).";
- pp " rewrite H1; simpl Z_of_nat; change (2^%i) with (%s)." i (gen2 i);
- pp " unfold base.";
- pp " apply Zpower_le_monotone; split; auto with zarith.";
- if i <> 0 then
- begin
- pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.";
- pp " repeat rewrite <- Zpos_xO.";
- pp " refine (Zle_refl _).";
- end;
- done;
- pp " intros n.";
- pp " intros H1; rewrite spec_reduce_n; unfold to_Z.";
- pp " simpl minus; rewrite <- minus_n_O.";
- pp " apply (znz_of_pos_correct (wn_spec n)).";
- pp " apply Zlt_le_trans with (1 := pheight_correct x).";
- pp " unfold base.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " split; auto with zarith.";
- pp " rewrite H1.";
- pp " elim n; clear n H1.";
- pp " simpl Z_of_nat; change (2^%i) with (%s)." (size + 1) (gen2 (size + 1));
- pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.";
- pp " repeat rewrite <- Zpos_xO.";
- pp " refine (Zle_refl _).";
- pp " intros n Hrec.";
- pp " rewrite make_op_S.";
- pp " change (@znz_digits (word _ (S (S n))) (mk_zn2z_op_karatsuba (make_op n))) with";
- pp " (xO (znz_digits (make_op n))).";
- pp " rewrite (fun x y => (Zpos_xO (@znz_digits x y))).";
- pp " rewrite inj_S; unfold Zsucc.";
- pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith.";
- pp " rewrite Zpower_1_r.";
- pp " assert (tmp: forall x y z, x * (y * z) = y * (x * z));";
- pp " [intros; ring | rewrite tmp; clear tmp].";
- pp " apply Zmult_le_compat_l; auto with zarith.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (** * Shift *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- (* Head0 *)
- pr " Definition head0 w := match w with";
- for i = 0 to size do
- pr " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)" c i i i;
- done;
- pr " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)" c;
- pr " end.";
- pr "";
-
- pr " Theorem spec_head00: forall x, [x] = 0 ->[head0 x] = Zpos (digits x).";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; unfold head0; clear x.";
- for i = 0 to size do
- pp " intros x; rewrite spec_reduce_%i; exact (spec_head00 w%i_spec x)." i i;
- done;
- pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x).";
- pp " Qed.";
- 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 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 " 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.";
- done;
- pp " intros n x Hx; rewrite spec_reduce_n.";
- 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 " 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.";
- pp " Qed.";
- pr "";
-
-
- (* Tail0 *)
- pr " Definition tail0 w := match w with";
- for i = 0 to size do
- pr " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)" c i i i;
- done;
- pr " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)" c;
- pr " end.";
- pr "";
-
-
- pr " Theorem spec_tail00: forall x, [x] = 0 ->[tail0 x] = Zpos (digits x).";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; unfold tail0; clear x.";
- for i = 0 to size do
- pp " intros x; rewrite spec_reduce_%i; exact (spec_tail00 w%i_spec x)." i i;
- done;
- pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x).";
- pp " Qed.";
- pr "";
-
-
- pr " Theorem spec_tail0: forall x,";
- pr " 0 < [x] -> exists y, 0 <= y /\\ [x] = (2 * y + 1) * 2 ^ [tail0 x].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; clear x; unfold tail0.";
- for i = 0 to size do
- pp " intros x Hx; rewrite spec_reduce_%i; exact (spec_tail0 w%i_spec x Hx)." i i;
- done;
- pp " intros n x Hx; rewrite spec_reduce_n; exact (spec_tail0 (wn_spec n) x Hx).";
- pp " Qed.";
- pr "";
-
-
- (* Number of digits *)
- pr " Definition %sdigits x :=" c;
- pr " match x with";
- pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c;
- 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;
- pr " end.";
- pr "";
-
- pr " Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x).";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; clear x; unfold Ndigits, digits.";
- for i = 0 to size do
- pp " intros _; try rewrite spec_reduce_%i; exact (spec_zdigits w%i_spec)." i i;
- done;
- pp " intros n _; try rewrite spec_reduce_n; exact (spec_zdigits (wn_spec n)).";
- pp " Qed.";
- pr "";
-
-
- (* Shiftr *)
- for i = 0 to size do
- 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 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 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 (unsafe_shiftr%i n x))" i i;
- done;
- pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x)).";
- pr "";
-
-
- 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).";
- pp " intros; ring.";
- pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z).";
- pp " intros x y z HH HH1 HH2.";
- pp " split; auto with zarith.";
- pp " apply Zle_lt_trans with (2 := HH2); auto with zarith.";
- pp " apply Zdiv_le_upper_bound; auto with zarith.";
- pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.";
- pp " apply Zmult_le_compat_l; auto.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " rewrite Zpower_0_r; ring.";
- pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x).";
- pp " intros xx y HH HH1.";
- 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 " (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) ->";
- pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->";
- pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->";
- pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->";
- pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->";
- pp " znz_to_Z ww_op";
- pp " (znz_add_mul_div ww_op (znz_sub ww_op (znz_zdigits ww_op) yy1)";
- pp " (znz_0 ww_op) xx1) = znz_to_Z ww1_op xx / 2 ^ znz_to_Z ww2_op yy).";
- pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy.";
- pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2.";
- pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4.";
- pp " rewrite <- Hx.";
- 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 " yy1)";
- pp " ).";
- pp " rewrite (spec_0 Hw).";
- pp " rewrite Zmult_0_l; rewrite Zplus_0_l.";
- pp " rewrite (CyclicAxioms.spec_sub Hw).";
- pp " rewrite Zmod_small; auto with zarith.";
- pp " rewrite (spec_zdigits Hw).";
- pp " rewrite F0.";
- pp " rewrite Zmod_small; auto with zarith.";
- pp " unfold base; rewrite (spec_zdigits Hw) in Hl1 |- *;";
- pp " auto with zarith.";
- pp " assert (F5: forall n m, (n <= m)%snat ->" "%";
- pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m))).";
- pp " intros n m HH; elim HH; clear m HH; auto with zarith.";
- pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec).";
- pp " rewrite make_op_S.";
- pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end.";
- pp " rewrite Zpos_xO.";
- pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith.";
- pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size;
- pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0))).";
- pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
- 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 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 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;
- pp " rewrite (spec_zdigits w%i_spec)." j;
- pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)"));
- pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
- pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
- 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 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 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 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
- begin
- 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;
- pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size;
- end
- done;
- pp " intros n x y; case y; clear y;";
- 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;
- pp " rewrite (spec_zdigits w%i_spec)." i;
- pp " rewrite (spec_zdigits (wn_spec n)).";
- pp " apply Zle_trans with (2 := F6 n).";
- pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)"));
- pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
- pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
- pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i;
- if i == size then
- pp " change ([Nn n (extend%i n y)] = [N%i y])." size i
- else
- pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i;
- pp " rewrite <- (spec_extend%in n); auto." size;
- if i <> size then
- pp " try (rewrite <- spec_extend%in%i; auto)." i size;
- done;
- pp " generalize y; clear y; intros m y.";
- pp " rewrite spec_reduce_n; unfold to_Z; intros H1.";
- pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith.";
- pp " rewrite (spec_zdigits (wn_spec m)).";
- pp " rewrite (spec_zdigits (wn_spec (Max.max n m))).";
- pp " apply F5; auto with arith.";
- pp " exact (spec_cast_r n m y).";
- pp " exact (spec_cast_l n m x).";
- pp " Qed.";
- pr "";
-
- (* Unsafe_Shiftl *)
- for i = 0 to size do
- 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 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 (unsafe_shiftl%i n x))" i i;
- done;
- pr " (fun n p x => reduce_n n (unsafe_shiftln n p x)).";
- pr "";
- pr "";
-
-
- 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).";
- pp " intros; ring.";
- pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z).";
- pp " intros x y z HH HH1 HH2.";
- pp " split; auto with zarith.";
- pp " apply Zle_lt_trans with (2 := HH2); auto with zarith.";
- pp " apply Zdiv_le_upper_bound; auto with zarith.";
- pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.";
- pp " apply Zmult_le_compat_l; auto.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " rewrite Zpower_0_r; ring.";
- pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x).";
- pp " intros xx y HH HH1.";
- 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 " (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) ->";
- pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->";
- pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->";
- pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->";
- pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->";
- pp " znz_to_Z ww_op";
- pp " (znz_add_mul_div ww_op yy1";
- pp " xx1 (znz_0 ww_op)) = znz_to_Z ww1_op xx * 2 ^ znz_to_Z ww2_op yy).";
- pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy.";
- pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2.";
- pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4.";
- pp " rewrite <- Hx.";
- pp " rewrite <- Hy.";
- pp " generalize (spec_add_mul_div Hw xx1 (znz_0 ww_op) yy1).";
- pp " rewrite (spec_0 Hw).";
- pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op)).";
- pp " case (Zle_lt_or_eq _ _ HH1); intros HH5.";
- pp " apply Zlt_le_weak.";
- pp " case (CyclicAxioms.spec_head0 Hw1 xx).";
- pp " rewrite <- Hx; auto.";
- pp " intros _ Hu; unfold base in Hu.";
- pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))";
- pp " (znz_to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1.";
- pp " absurd (2 ^ (Zpos (znz_digits ww1_op)) <= 2 ^ (znz_to_Z ww1_op (znz_head0 ww1_op xx))).";
- pp " apply Zlt_not_le.";
- pp " case (spec_to_Z Hw1 xx); intros HHx3 HHx4.";
- pp " rewrite <- (Zmult_1_r (2 ^ znz_to_Z ww1_op (znz_head0 ww1_op xx))).";
- pp " apply Zle_lt_trans with (2 := Hu).";
- pp " apply Zmult_le_compat_l; auto with zarith.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
- pp " rewrite Zdiv_0_l; auto with zarith.";
- pp " rewrite Zplus_0_r.";
- pp " case (Zle_lt_or_eq _ _ HH1); intros HH5.";
- 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 " apply Zle_trans with (2 := Hl1); auto.";
- pp " rewrite (spec_zdigits Hw1); auto with zarith.";
- pp " split; auto with zarith .";
- pp " apply Zlt_le_trans with (base (znz_digits ww1_op)).";
- pp " rewrite Hx.";
- pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto.";
- pp " rewrite <- Hx; auto.";
- pp " intros _ Hu; rewrite Zmult_comm in Hu.";
- pp " apply Zle_lt_trans with (2 := Hu).";
- pp " apply Zmult_le_compat_l; auto with zarith.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " unfold base; apply Zpower_le_monotone; auto with zarith.";
- pp " split; auto with zarith.";
- pp " rewrite <- (spec_zdigits Hw); auto with zarith.";
- pp " rewrite <- (spec_zdigits Hw1); auto with zarith.";
- pp " rewrite <- HH5.";
- pp " rewrite Zmult_0_l.";
- pp " rewrite Zmod_small; auto with zarith.";
- pp " intros HH; apply HH.";
- pp " rewrite Hy; apply Zle_trans with (1 := Hl).";
- pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
- pp " rewrite <- (spec_zdigits Hw); auto with zarith.";
- pp " rewrite <- (spec_zdigits Hw1); auto with zarith.";
- pp " assert (F5: forall n m, (n <= m)%snat ->" "%";
- pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m))).";
- pp " intros n m HH; elim HH; clear m HH; auto with zarith.";
- pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec).";
- pp " rewrite make_op_S.";
- pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end.";
- pp " rewrite Zpos_xO.";
- pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith.";
- pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size;
- pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0))).";
- pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
- 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 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 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;
- pp " rewrite (spec_zdigits w%i_spec)." j;
- pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)"));
- pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
- pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
- 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 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 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 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
- begin
- 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;
- pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size;
- end
- done;
- pp " intros n x y; case y; clear y;";
- 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;
- pp " rewrite (spec_zdigits w%i_spec)." i;
- pp " rewrite (spec_zdigits (wn_spec n)).";
- pp " apply Zle_trans with (2 := F6 n).";
- pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)"));
- pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
- pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
- pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i;
- if i == size then
- pp " change ([Nn n (extend%i n y)] = [N%i y])." size i
- else
- pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i;
- pp " rewrite <- (spec_extend%in n); auto." size;
- if i <> size then
- pp " try (rewrite <- spec_extend%in%i; auto)." i size;
- done;
- pp " generalize y; clear y; intros m y.";
- pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
- pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith.";
- pp " rewrite (spec_zdigits (wn_spec m)).";
- pp " rewrite (spec_zdigits (wn_spec (Max.max n m))).";
- pp " apply F5; auto with arith.";
- pp " exact (spec_cast_r n m y).";
- pp " exact (spec_cast_l n m x).";
- pp " Qed.";
- pr "";
-
- (* Double size *)
- pr " Definition double_size w := match w with";
- for i = 0 to size-1 do
- pr " | %s%i x => %s%i (WW (znz_0 w%i_op) x)" c i c (i + 1) i;
- done;
- pr " | %s%i x => %sn 0 (WW (znz_0 w%i_op) x)" c size c size;
- pr " | %sn n x => %sn (S n) (WW (znz_0 (make_op n)) x)" c c;
- pr " end.";
- pr "";
-
- pr " Theorem spec_double_size_digits:";
- pr " forall x, digits (double_size x) = xO (digits x).";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; unfold double_size, digits; clear x; auto.";
- pp " intros n x; rewrite make_op_S; auto.";
- pp " Qed.";
- pr "";
-
-
- pr " Theorem spec_double_size: forall x, [double_size x] = [x].";
- pa " Admitted.";
- 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 " 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;";
- pp " generalize (znz_to_Z_n n); simpl word.";
- pp " intros HH; rewrite HH; clear HH.";
- pp " generalize (spec_0 (wn_spec n)); simpl word.";
- pp " intros HH; rewrite HH; clear HH; auto with zarith.";
- pp " Qed.";
- pr "";
-
-
- pr " Theorem spec_double_size_head0:";
- pr " forall x, 2 * [head0 x] <= [head0 (double_size x)].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x.";
- pp " assert (F1:= spec_pos (head0 x)).";
- pp " assert (F2: 0 < Zpos (digits x)).";
- pp " red; auto.";
- pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH.";
- pp " generalize HH; rewrite <- (spec_double_size x); intros HH1.";
- pp " case (spec_head0 x HH); intros _ HH2.";
- pp " case (spec_head0 _ HH1).";
- pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x).";
- pp " intros HH3 _.";
- pp " case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4.";
- pp " absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto.";
- pp " apply Zle_not_lt.";
- pp " apply Zmult_le_compat_r; auto with zarith.";
- pp " apply Zpower_le_monotone; auto; auto with zarith.";
- pp " generalize (spec_pos (head0 (double_size x))); auto with zarith.";
- pp " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).";
- pp " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5.";
- pp " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith.";
- pp " rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith.";
- pp " assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp].";
- pp " apply Zle_trans with (2 := Zlt_le_weak _ _ HH2).";
- 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 " 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.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " rewrite (Zmult_comm 2).";
- pp " rewrite Zpower_mult; auto with zarith.";
- pp " rewrite Zpower_2.";
- pp " apply Zlt_le_trans with (2 := HH3).";
- pp " rewrite <- Zmult_assoc.";
- pp " replace (Zpos (xO (digits x)) - 1) with";
- pp " ((Zpos (digits x) - 1) + (Zpos (digits x))).";
- pp " rewrite Zpower_exp; auto with zarith.";
- pp " apply Zmult_lt_compat2; auto with zarith.";
- pp " split; auto with zarith.";
- pp " apply Zmult_lt_0_compat; auto with zarith.";
- pp " rewrite Zpos_xO; ring.";
- pp " apply Zlt_le_weak; auto.";
- pp " repeat rewrite spec_head00; auto.";
- pp " rewrite spec_double_size_digits.";
- pp " rewrite Zpos_xO; auto with zarith.";
- pp " rewrite spec_double_size; auto.";
- pp " Qed.";
- pr "";
-
- pr " Theorem spec_double_size_head0_pos:";
- pr " forall x, 0 < [head0 (double_size x)].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x.";
- pp " assert (F: 0 < Zpos (digits x)).";
- pp " red; auto.";
- pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0.";
- pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1.";
- pp " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.";
- pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3.";
- pp " generalize F3; rewrite <- (spec_double_size x); intros F4.";
- pp " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).";
- pp " apply Zle_not_lt.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " split; auto with zarith.";
- pp " rewrite Zpos_xO; auto with zarith.";
- pp " case (spec_head0 x F3).";
- pp " rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH.";
- pp " apply Zle_lt_trans with (2 := HH).";
- pp " case (spec_head0 _ F4).";
- pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x).";
- pp " rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto.";
- pp " generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith.";
- pp " Qed.";
- pr "";
-
- (* even *)
- pr " Definition is_even x :=";
- pr " match x with";
- for i = 0 to size do
- pr " | %s%i wx => w%i_op.(znz_is_even) wx" c i i
- done;
- pr " | %sn n wx => (make_op n).(znz_is_even) wx" c;
- pr " end.";
- pr "";
-
-
- pr " Theorem spec_is_even: forall x,";
- pr " if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x; unfold is_even, to_Z; clear x.";
- for i = 0 to size do
- pp " intros x; exact (spec_is_even w%i_spec x)." i;
- done;
- pp " intros n x; exact (spec_is_even (wn_spec n) x).";
- pp " Qed.";
- pr "";
-
- pr "End Make.";
- pr "";
-
+ pr " Eval lazy beta iota delta [reduce_n] in";
+ pr " reduce_n _ _ (N0 zero0) reduce_%i Nn n." (size + 1);
+ pr "";
+
+pr " Definition reduce n : dom_t n -> t :=";
+pr " match n with";
+for i = 0 to size do
+pr " | %i => reduce_%i" i i;
+done;
+pr " | %s(S n) => reduce_n n" (if size=0 then "" else "SizePlus ");
+pr " end.";
+pr "";
+
+pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ",");
+
+pr "
+ Ltac solve_red :=
+ let H := fresh in let G := fresh in
+ match goal with
+ | |- ?P (S ?n) => assert (H:P n) by solve_red
+ | _ => idtac
+ end;
+ intros n G x; destruct (le_lt_eq_dec _ _ G) as [LT|EQ];
+ solve [
+ apply (H _ (lt_n_Sm_le _ _ LT)) |
+ inversion LT |
+ subst; change (reduce 0 x = red_t 0 x); reflexivity |
+ specialize (H (pred n)); subst; destruct x;
+ [|unfold_red; rewrite H; auto]; reflexivity
+ ].
+
+ Lemma reduce_equiv : forall n x, n <= Size -> reduce n x = red_t n x.
+ Proof.
+ set (P N := forall n, n <= N -> forall x, reduce n x = red_t n x).
+ intros n x H. revert n H x. change (P Size). solve_red.
+ Qed.
+
+ Lemma spec_reduce_n : forall n x, [reduce_n n x] = [Nn n x].
+ Proof.
+ assert (H : forall x, reduce_%i x = red_t (SizePlus 1) x).
+ destruct x; [|unfold reduce_%i; rewrite (reduce_equiv Size)]; auto.
+ induction n.
+ intros. rewrite H. apply spec_red_t.
+ destruct x as [|xh xl].
+ simpl. rewrite make_op_S. exact ZnZ.spec_0.
+ fold word in *.
+ destruct xh; auto.
+ simpl reduce_n.
+ rewrite IHn.
+ rewrite spec_extend_WW; auto.
+ Qed.
+" (size+1) (size+1);
+
+pr
+" Lemma spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
+ Proof.
+ do_size (destruct n;
+ [intros; rewrite reduce_equiv;[apply spec_red_t|auto with arith]|]).
+ apply spec_reduce_n.
+ Qed.
+
+End Make.
+";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index cdd41647..5bde1008 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,9 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: Nbasic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-Require Import ZArith.
+Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import Max.
Require Import DoubleType.
@@ -18,44 +16,64 @@ Require Import DoubleBase.
Require Import CyclicAxioms.
Require Import DoubleCyclic.
+Arguments mk_zn2z_ops [t] ops.
+Arguments mk_zn2z_ops_karatsuba [t] ops.
+Arguments mk_zn2z_specs [t ops] specs.
+Arguments mk_zn2z_specs_karatsuba [t ops] specs.
+Arguments ZnZ.digits [t] Ops.
+Arguments ZnZ.zdigits [t] Ops.
+
+Lemma Pshiftl_nat_Zpower : forall n p,
+ Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
+Proof.
+ intros.
+ rewrite Z.mul_comm.
+ induction n. simpl; auto.
+ transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
+ rewrite <- IHn. auto.
+ rewrite Z.mul_assoc.
+ rewrite Nat2Z.inj_succ.
+ rewrite <- Z.pow_succ_r; auto with zarith.
+Qed.
+
(* To compute the necessary height *)
Fixpoint plength (p: positive) : positive :=
match p with
xH => xH
- | xO p1 => Psucc (plength p1)
- | xI p1 => Psucc (plength p1)
+ | xO p1 => Pos.succ (plength p1)
+ | xI p1 => Pos.succ (plength p1)
end.
Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
-assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
-intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
+assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z).
+intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z.
rewrite Zpower_exp; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
intros p; elim p; simpl plength; auto.
-intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
+intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI.
assert (tmp: (forall p, 2 * p = p + p)%Z);
try repeat rewrite tmp; auto with zarith.
-intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
+intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1).
assert (tmp: (forall p, 2 * p = p + p)%Z);
try repeat rewrite tmp; auto with zarith.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
Qed.
-Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
-intros p; case (Psucc_pred p); intros H1.
+Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z.
+intros p; case (Pos.succ_pred_or p); intros H1.
subst; simpl plength.
-rewrite Zpower_1_r; auto with zarith.
+rewrite Z.pow_1_r; auto with zarith.
pattern p at 1; rewrite <- H1.
-rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
-generalize (plength_correct (Ppred p)); auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith.
+generalize (plength_correct (Pos.pred p)); auto with zarith.
Qed.
Definition Pdiv p q :=
- match Zdiv (Zpos p) (Zpos q) with
+ match Z.div (Zpos p) (Zpos q) with
Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
Z0 => q1
- | _ => (Psucc q1)
+ | _ => (Pos.succ q1)
end
| _ => xH
end.
@@ -67,20 +85,20 @@ unfold Pdiv.
assert (H1: Zpos q > 0); auto with zarith.
assert (H1b: Zpos p >= 0); auto with zarith.
generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b).
-generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv.
- intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl.
+generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Z.div.
+ intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl.
case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
intros q1 H2.
replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2;
- case Zmod.
+ case Z.modulo.
intros HH _; rewrite HH; auto with zarith.
- intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
- unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith.
+ intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ.
+ unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith.
intros r1 _ (HH,_); case HH; auto.
intros q1 HH; rewrite HH.
-unfold Zge; simpl Zcompare; intros HH1; case HH1; auto.
+unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto.
Qed.
Definition is_one p := match p with xH => true | _ => false end.
@@ -91,7 +109,7 @@ Qed.
Definition get_height digits p :=
let r := Pdiv p digits in
- if is_one r then xH else Psucc (plength (Ppred r)).
+ if is_one r then xH else Pos.succ (plength (Pos.pred r)).
Theorem get_height_correct:
forall digits N,
@@ -101,13 +119,13 @@ unfold get_height.
assert (H1 := Pdiv_le N digits).
case_eq (is_one (Pdiv N digits)); intros H2.
rewrite (is_one_one _ H2) in H1.
-rewrite Zmult_1_r in H1.
-change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto.
+rewrite Z.mul_1_r in H1.
+change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto.
clear H2.
-apply Zle_trans with (1 := H1).
-apply Zmult_le_compat_l; auto with zarith.
-rewrite Zpos_succ_morphism; unfold Zsucc.
-rewrite Zplus_comm; rewrite Zminus_plus.
+apply Z.le_trans with (1 := H1).
+apply Z.mul_le_mono_nonneg_l; auto with zarith.
+rewrite Pos2Z.inj_succ; unfold Z.succ.
+rewrite Z.add_comm; rewrite Z.add_simpl_l.
apply plength_pred_correct.
Qed.
@@ -134,18 +152,18 @@ Open Scope nat_scope.
Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
match n return (n + S m = S (n + m))%nat with
- | 0 => refl_equal (S m)
+ | 0 => eq_refl (S m)
| S n1 =>
let v := S (S n1 + m) in
- eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
+ eq_ind_r (fun n => S n = v) (eq_refl v) (plusnS n1 m)
end.
Fixpoint plusn0 n : n + 0 = n :=
match n return (n + 0 = n) with
- | 0 => refl_equal 0
+ | 0 => eq_refl 0
| S n1 =>
let v := S n1 in
- eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
+ eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1)
end.
Fixpoint diff (m n: nat) {struct m}: nat * nat :=
@@ -159,8 +177,8 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
match m return fst (diff m n) + n = max m n with
| 0 =>
match n return (n = max 0 n) with
- | 0 => refl_equal _
- | S n0 => refl_equal _
+ | 0 => eq_refl _
+ | S n0 => eq_refl _
end
| S m1 =>
match n return (fst (diff (S m1) n) + n = max (S m1) n)
@@ -170,7 +188,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
let v := fst (diff m1 n1) + n1 in
let v1 := fst (diff m1 n1) + S n1 in
eq_ind v (fun n => v1 = S n)
- (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
+ (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _))
_ (diff_l _ _)
end
end.
@@ -179,17 +197,17 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
match m return (snd (diff m n) + m = max m n) with
| 0 =>
match n return (snd (diff 0 n) + 0 = max 0 n) with
- | 0 => refl_equal _
+ | 0 => eq_refl _
| S _ => plusn0 _
end
| S m =>
match n return (snd (diff (S m) n) + S m = max (S m) n) with
- | 0 => refl_equal (snd (diff (S m) 0) + S m)
+ | 0 => eq_refl (snd (diff (S m) 0) + S m)
| S n1 =>
let v := S (max m n1) in
eq_ind_r (fun n => n = v)
(eq_ind_r (fun n => S n = v)
- (refl_equal v) (diff_r _ _)) (plusnS _ _)
+ (eq_refl v) (diff_r _ _)) (plusnS _ _)
end
end.
@@ -198,7 +216,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
(word w (S n)) :=
match H in (_ = y) return (word w (S y)) with
- | refl_equal => x
+ | eq_refl => x
end.
Variable m: nat.
@@ -212,8 +230,8 @@ Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
End ExtendMax.
-Implicit Arguments extend_tr[w m].
-Implicit Arguments castm[w m n].
+Arguments extend_tr [w m] v n.
+Arguments castm [w m n] H x.
@@ -287,11 +305,7 @@ Section CompareRec.
Variable w_to_Z: w -> Z.
Variable w_to_Z_0: w_to_Z w_0 = 0.
Variable spec_compare0_m: forall x,
- match compare0_m x with
- Eq => w_to_Z w_0 = wm_to_Z x
- | Lt => w_to_Z w_0 < wm_to_Z x
- | Gt => w_to_Z w_0 > wm_to_Z x
- end.
+ compare0_m x = (w_to_Z w_0 ?= wm_to_Z x).
Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.
Let double_to_Z := double_to_Z wm_base wm_to_Z.
@@ -300,7 +314,7 @@ Section CompareRec.
Lemma base_xO: forall n, base (xO n) = (base n)^2.
Proof.
intros n1; unfold base.
- rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
+ rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith.
Qed.
Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
@@ -308,29 +322,25 @@ Section CompareRec.
Lemma spec_compare0_mn: forall n x,
- match compare0_mn n x with
- Eq => 0 = double_to_Z n x
- | Lt => 0 < double_to_Z n x
- | Gt => 0 > double_to_Z n x
- end.
- Proof.
+ compare0_mn n x = (0 ?= double_to_Z n x).
+ Proof.
intros n; elim n; clear n; auto.
- intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto.
+ intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto.
intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
+ fold word in *.
intros xh xl.
- generalize (Hrec xh); case compare0_mn; auto.
- generalize (Hrec xl); case compare0_mn; auto.
- simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto.
- simpl double_to_Z; intros H1 H2; rewrite <- H2; auto.
+ rewrite 2 Hrec.
+ simpl double_to_Z.
+ set (wB := DoubleBase.double_wB wm_base n).
+ case Z.compare_spec; intros Cmp.
+ rewrite <- Cmp. reflexivity.
+ symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *)
+ assert (0 < wB).
+ unfold wB, DoubleBase.double_wB, base; auto with zarith.
+ change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith.
+ apply Z.mul_pos_pos; auto with zarith.
case (double_to_Z_pos n xl); auto with zarith.
- intros H1; simpl double_to_Z.
- set (u := DoubleBase.double_wB wm_base n).
- case (double_to_Z_pos n xl); intros H2 H3.
- assert (0 < u); auto with zarith.
- unfold u, DoubleBase.double_wB, base; auto with zarith.
- change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith.
- apply Zmult_lt_0_compat; auto with zarith.
- case (double_to_Z_pos n xh); auto with zarith.
+ case (double_to_Z_pos n xh); intros; exfalso; omega.
Qed.
Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
@@ -348,17 +358,9 @@ Section CompareRec.
end.
Variable spec_compare: forall x y,
- match compare x y with
- Eq => w_to_Z x = w_to_Z y
- | Lt => w_to_Z x < w_to_Z y
- | Gt => w_to_Z x > w_to_Z y
- end.
+ compare x y = Z.compare (w_to_Z x) (w_to_Z y).
Variable spec_compare_m: forall x y,
- match compare_m x y with
- Eq => wm_to_Z x = w_to_Z y
- | Lt => wm_to_Z x < w_to_Z y
- | Gt => wm_to_Z x > w_to_Z y
- end.
+ compare_m x y = Z.compare (wm_to_Z x) (w_to_Z y).
Variable wm_base_lt: forall x,
0 <= w_to_Z x < base (wm_base).
@@ -367,39 +369,36 @@ Section CompareRec.
Proof.
intros n x; elim n; simpl; auto; clear n.
intros n (H0, H); split; auto.
- apply Zlt_le_trans with (1:= H).
+ apply Z.lt_le_trans with (1:= H).
unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite base_xO.
- set (u := base (double_digits wm_base n)).
+ rewrite Pshiftl_nat_S, base_xO.
+ set (u := base (Pos.shiftl_nat wm_base n)).
assert (0 < u).
unfold u, base; auto with zarith.
replace (u^2) with (u * u); simpl; auto with zarith.
- apply Zle_trans with (1 * u); auto with zarith.
- unfold Zpower_pos; simpl; ring.
+ apply Z.le_trans with (1 * u); auto with zarith.
+ unfold Z.pow_pos; simpl; ring.
Qed.
Lemma spec_compare_mn_1: forall n x y,
- match compare_mn_1 n x y with
- Eq => double_to_Z n x = w_to_Z y
- | Lt => double_to_Z n x < w_to_Z y
- | Gt => double_to_Z n x > w_to_Z y
- end.
+ compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y).
Proof.
intros n; elim n; simpl; auto; clear n.
intros n Hrec x; case x; clear x; auto.
- intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto.
- intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b.
- rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto.
- apply Hrec.
- apply Zlt_gt.
+ intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity.
+ intros xh xl y; simpl;
+ rewrite spec_compare0_mn, Hrec. case Z.compare_spec.
+ intros H1b.
+ rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto.
+ symmetry. apply Z.lt_gt.
case (double_wB_lt n y); intros _ H0.
- apply Zlt_le_trans with (1:= H0).
+ apply Z.lt_le_trans with (1:= H0).
fold double_wB.
case (double_to_Z_pos n xl); intros H1 H2.
- apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith.
- apply Zle_trans with (1 * double_wB n); auto with zarith.
- case (double_to_Z_pos n xh); auto with zarith.
+ apply Z.le_trans with (double_to_Z n xh * double_wB n); auto with zarith.
+ apply Z.le_trans with (1 * double_wB n); auto with zarith.
+ case (double_to_Z_pos n xh); intros; exfalso; omega.
Qed.
End CompareRec.
@@ -433,22 +432,6 @@ Section AddS.
End AddS.
-
- Lemma spec_opp: forall u x y,
- match u with
- | Eq => y = x
- | Lt => y < x
- | Gt => y > x
- end ->
- match CompOpp u with
- | Eq => x = y
- | Lt => x < y
- | Gt => x > y
- end.
- Proof.
- intros u x y; case u; simpl; auto with zarith.
- Qed.
-
Fixpoint length_pos x :=
match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.
@@ -457,8 +440,8 @@ End AddS.
Proof.
intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
intros y; case y; clear y; intros y1 H || intros H; simpl length_pos;
- try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
- try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
+ try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1));
+ try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1));
try (inversion H; fail);
try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith);
assert (0 < Zpos y1); auto with zarith; red; auto.
@@ -474,34 +457,112 @@ End AddS.
Variable w: Type.
- Theorem digits_zop: forall w (x: znz_op w),
- znz_digits (mk_zn2z_op x) = xO (znz_digits x).
+ Theorem digits_zop: forall t (ops : ZnZ.Ops t),
+ ZnZ.digits (mk_zn2z_ops ops) = xO (ZnZ.digits ops).
+ Proof.
intros ww x; auto.
Qed.
- Theorem digits_kzop: forall w (x: znz_op w),
- znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x).
+ Theorem digits_kzop: forall t (ops : ZnZ.Ops t),
+ ZnZ.digits (mk_zn2z_ops_karatsuba ops) = xO (ZnZ.digits ops).
+ Proof.
intros ww x; auto.
Qed.
- Theorem make_zop: forall w (x: znz_op w),
- znz_to_Z (mk_zn2z_op x) =
+ Theorem make_zop: forall t (ops : ZnZ.Ops t),
+ @ZnZ.to_Z _ (mk_zn2z_ops ops) =
fun z => match z with
- W0 => 0
- | WW xh xl => znz_to_Z x xh * base (znz_digits x)
- + znz_to_Z x xl
+ | W0 => 0
+ | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops)
+ + ZnZ.to_Z xl
end.
+ Proof.
intros ww x; auto.
Qed.
- Theorem make_kzop: forall w (x: znz_op w),
- znz_to_Z (mk_zn2z_op_karatsuba x) =
+ Theorem make_kzop: forall t (ops: ZnZ.Ops t),
+ @ZnZ.to_Z _ (mk_zn2z_ops_karatsuba ops) =
fun z => match z with
- W0 => 0
- | WW xh xl => znz_to_Z x xh * base (znz_digits x)
- + znz_to_Z x xl
+ | W0 => 0
+ | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops)
+ + ZnZ.to_Z xl
end.
+ Proof.
intros ww x; auto.
Qed.
End SimplOp.
+
+(** Abstract vision of a datatype of arbitrary-large numbers.
+ Concrete operations can be derived from these generic
+ fonctions, in particular from [iter_t] and [same_level].
+*)
+
+Module Type NAbstract.
+
+(** The domains: a sequence of [Z/nZ] structures *)
+
+Parameter dom_t : nat -> Type.
+Declare Instance dom_op n : ZnZ.Ops (dom_t n).
+Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
+
+Axiom digits_dom_op : forall n,
+ ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op 0)) n.
+
+(** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t]
+ and destructor [destr_t] and iterator [iter_t] *)
+
+Parameter t : Type.
+
+Parameter mk_t : forall (n:nat), dom_t n -> t.
+
+Inductive View_t : t -> Prop :=
+ Mk_t : forall n (x : dom_t n), View_t (mk_t n x).
+
+Axiom destr_t : forall x, View_t x. (* i.e. every x is a (mk_t n xw) *)
+
+Parameter iter_t : forall {A:Type}(f : forall n, dom_t n -> A), t -> A.
+
+Axiom iter_mk_t : forall A (f:forall n, dom_t n -> A),
+ forall n x, iter_t f (mk_t n x) = f n x.
+
+(** Conversion to [ZArith] *)
+
+Parameter to_Z : t -> Z.
+Local Notation "[ x ]" := (to_Z x).
+
+Axiom spec_mk_t : forall n x, [mk_t n x] = ZnZ.to_Z x.
+
+(** [reduce] is like [mk_t], but try to minimise the level of the number *)
+
+Parameter reduce : forall (n:nat), dom_t n -> t.
+Axiom spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
+
+(** Number of level in the tree representation of a number.
+ NB: This function isn't a morphism for setoid [eq]. *)
+
+Definition level := iter_t (fun n _ => n).
+
+(** [same_level] and its rich specification, indexed by [level] *)
+
+Parameter same_level : forall {A:Type}
+ (f : forall n, dom_t n -> dom_t n -> A), t -> t -> A.
+
+Axiom spec_same_level_dep :
+ forall res
+ (P : nat -> Z -> Z -> res -> Prop)
+ (Pantimon : forall n m z z' r, (n <= m)%nat -> P m z z' r -> P n z z' r)
+ (f : forall n, dom_t n -> dom_t n -> res)
+ (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)),
+ forall x y, P (level x) [x] [y] (same_level f x y).
+
+(** [mk_t_S] : building a number of the next level *)
+
+Parameter mk_t_S : forall (n:nat), zn2z (dom_t n) -> t.
+
+Axiom spec_mk_t_S : forall n (x:zn2z (dom_t n)),
+ [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x.
+
+Axiom mk_t_S_level : forall n x, level (mk_t_S n x) = S n.
+
+End NAbstract.