aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v5
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v29
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v6
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v21
-rw-r--r--theories/Numbers/NatInt/NZParity.v2
-rw-r--r--theories/Numbers/NatInt/NZSqrt.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NDefOps.v1
-rw-r--r--theories/Numbers/Natural/Abstract/NStrongRec.v3
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v42
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml9
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v4
12 files changed, 59 insertions, 67 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 39e086c31..17c69d226 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -93,7 +93,7 @@ Module ZnZ.
lor : t -> t -> t;
land : t -> t -> t;
lxor : t -> t -> t }.
-
+
Section Specs.
Context {t : Type}{ops : Ops t}.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 809169a4d..a6bc44682 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -809,7 +809,7 @@ refine
refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1
w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits
w_sqrt2 pred add_mul_div head0 compare
- _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
+ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
exact ZnZ.spec_zdigits.
exact ZnZ.spec_more_than_1_digit.
exact ZnZ.spec_is_even.
@@ -846,7 +846,7 @@ refine
intros (Hn,Hn').
assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
{ simpl; symmetry.
- rewrite Z.add_comm, Z.mod_add; auto with zarith.
+ rewrite Z.add_comm, Z.mod_add; auto with zarith nocore.
apply Z.mod_small; eauto with ZnZ zarith. }
rewrite E.
unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
@@ -923,6 +923,7 @@ refine
End Z_2nZ.
+
Section MulAdd.
Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 8525b0e13..dddae7db5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -211,8 +211,7 @@ Section DoubleDiv32.
Variable w_div21 : w -> w -> w -> w*w.
Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w).
- Definition w_div32 a1 a2 a3 b1 b2 :=
- Eval lazy beta iota delta [ww_add_c_cont ww_add] in
+ Definition w_div32_body a1 a2 a3 b1 b2 :=
match w_compare a1 b1 with
| Lt =>
let (q,r) := w_div21 a1 a2 b1 in
@@ -233,6 +232,10 @@ Section DoubleDiv32.
| Gt => (w_0, W0) (* cas absurde *)
end.
+ Definition w_div32 a1 a2 a3 b1 b2 :=
+ Eval lazy beta iota delta [ww_add_c_cont ww_add w_div32_body] in
+ w_div32_body a1 a2 a3 b1 b2.
+
(* Proof *)
Variable w_digits : positive.
@@ -312,26 +315,8 @@ Section DoubleDiv32.
assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits).
Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2.
rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r.
- change (w_div32 a1 a2 a3 b1 b2) with
- match w_compare a1 b1 with
- | Lt =>
- let (q,r) := w_div21 a1 a2 b1 in
- match ww_sub_c (w_WW r a3) (w_mul_c q b2) with
- | C0 r1 => (q,r1)
- | C1 r1 =>
- let q := w_pred q in
- ww_add_c_cont w_WW w_add_c w_add_carry_c
- (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2)))
- (fun r2 => (q,r2))
- r1 (WW b1 b2)
- end
- | Eq =>
- ww_add_c_cont w_WW w_add_c w_add_carry_c
- (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2)))
- (fun r => (w_Bm1,r))
- (WW (w_sub a2 b2) a3) (WW b1 b2)
- | Gt => (w_0, W0) (* cas absurde *)
- end.
+ change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2).
+ unfold w_div32_body.
rewrite spec_compare. case Z.compare_spec; intro Hcmp.
simpl in Hlt.
rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index df5d42bbc..789436334 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -692,7 +692,7 @@ intros x; case x; simpl ww_is_even.
intros x y H; unfold ww_sqrt2.
repeat match goal with |- context[split ?x] =>
generalize (spec_split x); case (split x)
- end; simpl fst; simpl snd.
+ end; simpl @fst; simpl @snd.
intros w0 w1 Hw0 w2 w3 Hw1.
assert (U: wB/4 <= [|w2|]).
case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1.
@@ -1193,7 +1193,7 @@ Qed.
rewrite <- wwB_4_wB_4; auto.
generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith.
case (w_sqrt2 w0 w1); intros w2 c.
- simpl ww_to_Z; simpl fst.
+ simpl ww_to_Z; simpl @fst.
case c; unfold interp_carry; autorewrite with rm10.
intros w3 (H6, H7); rewrite H6.
assert (V1 := spec_to_Z w3);auto with zarith.
@@ -1256,7 +1256,7 @@ Qed.
generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith.
case (w_sqrt2 w0 w1); intros w2 c.
case (spec_to_Z w2); intros HH1 HH2.
- simpl ww_to_Z; simpl fst.
+ simpl ww_to_Z; simpl @fst.
assert (Hv3: [[ww_pred ww_zdigits]]
= Zpos (xO w_digits) - 1).
rewrite spec_ww_pred; rewrite spec_ww_zdigits.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 03fc58c55..634ff7d63 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -623,7 +623,7 @@ Section Basics.
rewrite i2l_length; omega.
generalize (firstn_length (size-n) (i2l x)).
rewrite i2l_length.
- intros H0 H1; rewrite H1 in H0.
+ intros H0 H1. rewrite H1 in H0.
rewrite min_l in H0 by omega.
simpl length in H0.
omega.
@@ -882,16 +882,16 @@ Section Basics.
destruct p; simpl snd.
specialize IHn with p.
- destruct (p2ibis n p). simpl snd in *.
-rewrite nshiftr_S_tail.
+ destruct (p2ibis n p). simpl @snd in *.
+ rewrite nshiftr_S_tail.
destruct (le_lt_dec size n).
rewrite nshiftr_above_size; auto.
assert (H:=nshiftr_0_firstl _ _ l IHn).
replace (shiftr (twice_plus_one i)) with i; auto.
- destruct i; simpl in *; rewrite H; auto.
+ destruct i; simpl in *. rewrite H; auto.
specialize IHn with p.
- destruct (p2ibis n p); simpl snd in *.
+ destruct (p2ibis n p); simpl @snd in *.
rewrite nshiftr_S_tail.
destruct (le_lt_dec size n).
rewrite nshiftr_above_size; auto.
@@ -945,7 +945,7 @@ rewrite nshiftr_S_tail.
intros.
simpl p2ibis; destruct p; [ | | red; auto];
specialize IHn with p;
- destruct (p2ibis n p); simpl snd in *; simpl phi_inv_positive;
+ destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive;
rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice;
replace (S (size - S n))%nat with (size - n)%nat by omega;
apply IHn; omega.
@@ -1629,7 +1629,7 @@ Section Int31_Specs.
Lemma spec_pos_mod : forall w p,
[|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
Proof.
- unfold ZnZ.pos_mod, int31_ops, compare31.
+ unfold int31_ops, ZnZ.pos_mod, compare31.
change [|31|] with 31%Z.
assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p).
intros.
@@ -1959,7 +1959,7 @@ Section Int31_Specs.
Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|].
intros Hj; generalize (spec_div i j Hj).
- case div31; intros q r; simpl fst.
+ case div31; intros q r; simpl @fst.
intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
rewrite H1; ring.
Qed.
@@ -2094,7 +2094,7 @@ Section Int31_Specs.
generalize (spec_div21 ih il j Hj Hj1).
case div3121; intros q r (Hq, Hr).
apply Zdiv_unique with (phi r); auto with zarith.
- simpl fst; apply eq_trans with (1 := Hq); ring.
+ simpl @fst; apply eq_trans with (1 := Hq); ring.
Qed.
Lemma sqrt312_step_correct rec ih il j:
@@ -2215,6 +2215,9 @@ Section Int31_Specs.
apply Nat2Z.is_nonneg.
Qed.
+ (* Avoid expanding [iter312_sqrt] before variables in the context. *)
+ Strategy 1 [iter312_sqrt].
+
Lemma spec_sqrt2 : forall x y,
wB/ 4 <= [|x|] ->
let (s,r) := sqrt312 x y in
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 0e9323789..1e6593b10 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -95,7 +95,7 @@ Proof.
intros.
generalize (Even_or_Odd n) (Even_Odd_False n).
rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
+ destruct (odd n), (even n) ; simpl; intuition.
Qed.
Lemma negb_even : forall n, negb (even n) = odd n.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 8146fd014..6b6c85310 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.
Proof.
assert (Proper (eq==>eq==>Logic.eq) compare).
intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
- intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx.
+ intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
Qed.
(** The spec of [sqrt_up] indeed determines it *)
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 621a2ed9c..adbbc5ea0 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -133,7 +133,6 @@ Proof.
intros m n; unfold ltb at 1.
f_equiv.
rewrite recursion_succ; f_equiv'.
-reflexivity.
Qed.
(* Above, we rewrite applications of function. Is it possible to rewrite
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 67cab5507..f98e8da9a 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,7 +13,7 @@ and proves its properties *)
Require Export NSub.
-Ltac f_equiv' := repeat (f_equiv; try intros ? ? ?; auto).
+Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto).
Module NStrongRecProp (Import N : NAxiomsRecSig').
Include NSubProp N.
@@ -82,7 +82,6 @@ Proof.
intros. unfold strong_rec0.
f_equiv.
rewrite recursion_succ; f_equiv'.
-reflexivity.
Qed.
Lemma strong_rec_0 : forall a,
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 93ae858d8..bfbcb9465 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -242,8 +242,8 @@ Module Make (W0:CyclicType) <: NType.
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 zero := ZnZ.zero (Ops:=op) in
+ let compare := ZnZ.compare (Ops:=op) in
let compare0 := compare zero in
fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
@@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType.
Local Notation compare_folded :=
(iter_sym _
- (fun n => @ZnZ.compare _ (dom_op n))
+ (fun n => ZnZ.compare (Ops:=dom_op n))
comparen_m
comparenm
CompOpp).
@@ -358,13 +358,13 @@ Module Make (W0:CyclicType) <: NType.
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 zero := ZnZ.zero in
+ let succ := ZnZ.succ (Ops:=op) in
+ let add_c := ZnZ.add_c (Ops:=op) in
+ let mul_c := ZnZ.mul_c (Ops:=op) in
let ww := @ZnZ.WW _ op in
let ow := @ZnZ.OW _ op in
- let eq0 := @ZnZ.eq0 _ op in
+ let eq0 := ZnZ.eq0 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 =>
@@ -464,13 +464,13 @@ Module Make (W0:CyclicType) <: NType.
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 zero := ZnZ.zero in
+ let ww := ZnZ.WW in
+ let head0 := ZnZ.head0 in
+ let add_mul_div := ZnZ.add_mul_div in
+ let div21 := ZnZ.div21 in
+ let compare := ZnZ.compare in
+ let sub := ZnZ.sub 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).
@@ -633,12 +633,12 @@ Module Make (W0:CyclicType) <: NType.
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 zero := ZnZ.zero in
+ let head0 := ZnZ.head0 in
+ let add_mul_div := ZnZ.add_mul_div in
+ let div21 := ZnZ.div21 in
+ let compare := ZnZ.compare in
+ let sub := ZnZ.sub 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).
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b28ce15b9..8df4b7c64 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -324,8 +324,13 @@ pr "
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.
+ do_size (destruct n;
+ [match goal with
+ |- @eq Z (_ (zeron ?n)) _ =>
+ apply (ZnZ.spec_0 (Specs:=dom_spec n))
+ end|]).
+ destruct n; auto. simpl. rewrite make_op_S. fold word.
+ apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))).
Qed.
(** * Digits *)
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 167be6d70..d9f4b0429 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -627,7 +627,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
assert (Hz := spec_irred_zero nx dy).
assert (Hz':= spec_irred_zero ny dx).
destruct irred as (n1,d1); destruct irred as (n2,d2).
- simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
+ simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
rewrite spec_norm_denum.
qsimpl.
@@ -665,7 +665,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
assert (Hgc := strong_spec_irred nx dy).
assert (Hgc' := strong_spec_irred ny dx).
destruct irred as (n1,d1); destruct irred as (n2,d2).
- simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
+ simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
unfold norm_denum; qsimpl.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 12:52:01 +0000