aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v72
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml74
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSig.v7
3 files changed, 77 insertions, 76 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index b5a4db91c..925b0535a 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -389,21 +389,21 @@ Module Make (Import W0:CyclicType) <: NType.
(** * Shift *)
- Definition safe_shiftr n x :=
+ Definition shiftr n x :=
match compare n (Ndigits x) with
- | Lt => shiftr n x
+ | Lt => unsafe_shiftr n x
| _ => N0 w_0
end.
- Theorem spec_safe_shiftr: forall n x,
- [safe_shiftr n x] = [x] / 2 ^ [n].
+ Theorem spec_shiftr: forall n x,
+ [shiftr n x] = [x] / 2 ^ [n].
Proof.
- intros n x; unfold safe_shiftr;
+ 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_shiftr; auto with zarith.
+ 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.
@@ -412,22 +412,22 @@ Module Make (Import W0:CyclicType) <: NType.
apply Zpower_le_monotone; auto with zarith.
Qed.
- Definition safe_shiftl_aux_body cont n x :=
+ Definition shiftl_aux_body cont n x :=
match compare n (head0 x) with
Gt => cont n (double_size x)
- | _ => shiftl n x
+ | _ => unsafe_shiftl n x
end.
- Theorem spec_safe_shift_aux_body: forall n p x cont,
+ Theorem spec_shiftl_aux_body: forall n p x cont,
2^ Zpos p <= [head0 x] ->
(forall x, 2 ^ (Zpos p + 1) <= [head0 x]->
[cont n x] = [x] * 2 ^ [n]) ->
- [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n].
+ [shiftl_aux_body cont n x] = [x] * 2 ^ [n].
Proof.
- intros n p x cont H1 H2; unfold safe_shiftl_aux_body.
+ intros n p x cont H1 H2; unfold shiftl_aux_body.
generalize (spec_compare_aux n (head0 x)); case compare; intros H.
- apply spec_shiftl; auto with zarith.
- apply spec_shiftl; auto with zarith.
+ 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.
@@ -435,23 +435,23 @@ Module Make (Import W0:CyclicType) <: NType.
rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith.
Qed.
- Fixpoint safe_shiftl_aux p cont n x {struct p} :=
- safe_shiftl_aux_body
+ Fixpoint shiftl_aux p cont n x {struct p} :=
+ shiftl_aux_body
(fun n x => match p with
| xH => cont n x
- | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x
- | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x
+ | xO p => shiftl_aux p (shiftl_aux p cont) n x
+ | xI p => shiftl_aux p (shiftl_aux p cont) n x
end) n x.
- Theorem spec_safe_shift_aux: forall p q n x cont,
+ Theorem spec_shiftl_aux: forall p q n x cont,
2 ^ (Zpos q) <= [head0 x] ->
(forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->
[cont n x] = [x] * 2 ^ [n]) ->
- [safe_shiftl_aux p cont n x] = [x] * 2 ^ [n].
+ [shiftl_aux p cont n x] = [x] * 2 ^ [n].
Proof.
- intros p; elim p; unfold safe_shiftl_aux; fold safe_shiftl_aux; clear p.
+ intros p; elim p; unfold shiftl_aux; fold shiftl_aux; clear p.
intros p Hrec q n x cont H1 H2.
- apply spec_safe_shift_aux_body with (q); auto.
+ 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.
@@ -462,7 +462,7 @@ Module Make (Import W0:CyclicType) <: NType.
auto.
repeat rewrite Zpos_plus_distr; ring.
intros p Hrec q n x cont H1 H2.
- apply spec_safe_shift_aux_body with (q); auto.
+ 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.
@@ -473,34 +473,34 @@ Module Make (Import W0:CyclicType) <: NType.
auto.
repeat rewrite Zpos_plus_distr; ring.
intros q n x cont H1 H2.
- apply spec_safe_shift_aux_body with (q); auto.
+ apply spec_shiftl_aux_body with (q); auto.
rewrite Zplus_comm; auto.
Qed.
- Definition safe_shiftl n x :=
- safe_shiftl_aux_body
- (safe_shiftl_aux_body
- (safe_shiftl_aux (digits n) shiftl)) n x.
+ Definition shiftl n x :=
+ shiftl_aux_body
+ (shiftl_aux_body
+ (shiftl_aux (digits n) unsafe_shiftl)) n x.
- Theorem spec_safe_shift: forall n x,
- [safe_shiftl n x] = [x] * 2 ^ [n].
+ Theorem spec_shiftl: forall n x,
+ [shiftl n x] = [x] * 2 ^ [n].
Proof.
- intros n x; unfold safe_shiftl, safe_shiftl_aux_body.
+ intros n x; unfold shiftl, shiftl_aux_body.
generalize (spec_compare_aux n (head0 x)); case compare; intros H.
- apply spec_shiftl; auto with zarith.
- apply spec_shiftl; auto with zarith.
+ apply spec_unsafe_shiftl; auto with zarith.
+ apply spec_unsafe_shiftl; auto with zarith.
rewrite <- (spec_double_size x).
generalize (spec_compare_aux n (head0 (double_size x))); case compare; intros H1.
- apply spec_shiftl; auto with zarith.
- apply spec_shiftl; auto with zarith.
+ apply spec_unsafe_shiftl; auto with zarith.
+ apply spec_unsafe_shiftl; auto with zarith.
rewrite <- (spec_double_size (double_size x)).
- apply spec_safe_shift_aux with 1%positive.
+ apply spec_shiftl_aux with 1%positive.
apply Zle_trans with (2 := spec_double_size_head0 (double_size x)).
replace (2 ^ 1) with (2 * 1).
apply Zmult_le_compat_l; auto with zarith.
generalize (spec_double_size_head0_pos x); auto with zarith.
rewrite Zpower_1_r; ring.
- intros x1 H2; apply spec_shiftl.
+ intros x1 H2; apply spec_unsafe_shiftl.
apply Zle_trans with (2 := H2).
apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith.
case (spec_digits n); auto with zarith.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index e045c068c..b8552a39b 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -71,9 +71,9 @@ let _ =
pr "";
pr "Require Import BigNumPrelude ZArith CyclicAxioms";
pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic";
- pr " Wf_nat StreamMemo NSig.";
+ pr " Wf_nat StreamMemo.";
pr "";
- pr "Module Make (Import W0:CyclicType). (*<: NType (now just almost) *)";
+ pr "Module Make (Import W0:CyclicType).";
pr "";
pr " Definition w0 := W0.w.";
@@ -470,7 +470,6 @@ let _ =
pp " unfold to_Z.";
pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extendn_0: extr.";
pp "";
pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
pp " Proof.";
@@ -481,7 +480,6 @@ let _ =
pp " case n; auto.";
pp " intros n1; rewrite make_op_S; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extendn_0: extr.";
pp "";
pp " Let spec_extend_tr: forall m n (w: word _ (S n)),";
pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c;
@@ -490,7 +488,6 @@ let _ =
pp " intros n x; simpl extend_tr.";
pp " simpl plus; rewrite spec_extendn0_0; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extend_tr: extr.";
pp "";
pp " Let spec_cast_l: forall n m x1,";
pp " [%sn (Max.max n m)" c;
@@ -500,7 +497,6 @@ let _ =
pp " intros n m x1; case (diff_r n m); simpl castm.";
pp " rewrite spec_extend_tr; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_cast_l: extr.";
pp "";
pp " Let spec_cast_r: forall n m x1,";
pp " [%sn (Max.max n m)" c;
@@ -510,7 +506,6 @@ let _ =
pp " intros n m x1; case (diff_l n m); simpl castm.";
pp " rewrite spec_extend_tr; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_cast_r: extr.";
pp "";
@@ -757,6 +752,7 @@ let _ =
pp " Ltac zg_tac := try";
pp " (red; simpl Zcompare; auto;";
pp " let t := fresh \"H\" in (intros t; discriminate t)).";
+ pp "";
pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
pp " Proof.";
pp " intros x; case x; clear x; unfold iter.";
@@ -1055,7 +1051,6 @@ let _ =
pp " apply f_equal2 with (f := Zmult); auto;";
pp " exact (spec_1 w%i_spec)." i;
pp " Qed.";
- pp " Hint Rewrite spec_w%i_add: addr." i;
pp "";
done;
pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c;
@@ -1068,7 +1063,6 @@ let _ =
pp " apply f_equal2 with (f := Zmult); auto;";
pp " exact (spec_1 (wn_spec k)).";
pp " Qed.";
- pp " Hint Rewrite spec_wn_add: addr.";
pr " Definition add := Eval lazy beta delta [same_level] in";
pr0 " (same_level t_ ";
@@ -2200,22 +2194,22 @@ let _ =
(* Shiftr *)
for i = 0 to size do
- pr " Definition shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i;
+ pr " Definition unsafe_shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i;
done;
- pr " Definition shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x.";
+ pr " Definition unsafe_shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x.";
pr "";
- pr " Definition shiftr := Eval lazy beta delta [same_level] in";
- pr " same_level _ (fun n x => %s0 (shiftr0 n x))" c;
+ pr " Definition unsafe_shiftr := Eval lazy beta delta [same_level] in";
+ pr " same_level _ (fun n x => %s0 (unsafe_shiftr0 n x))" c;
for i = 1 to size do
- pr " (fun n x => reduce_%i (shiftr%i n x))" i i;
+ pr " (fun n x => reduce_%i (unsafe_shiftr%i n x))" i i;
done;
- pr " (fun n p x => reduce_n n (shiftrn n p x)).";
+ pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x)).";
pr "";
- pr " Theorem spec_shiftr: forall n x,";
- pr " [n] <= [Ndigits x] -> [shiftr n x] = [x] / 2 ^ [n].";
+ pr " Theorem spec_unsafe_shiftr: forall n x,";
+ pr " [n] <= [Ndigits x] -> [unsafe_shiftr n x] = [x] / 2 ^ [n].";
pa " Admitted.";
pp " Proof.";
pp " assert (F0: forall x y, x - (x - y) = y).";
@@ -2278,11 +2272,11 @@ let _ =
pp " rewrite Zpos_xO.";
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
pp " apply F5; auto with arith.";
- pp " intros x; case x; clear x; unfold shiftr, same_level.";
+ pp " intros x; case x; clear x; unfold unsafe_shiftr, same_level.";
for i = 0 to size do
pp " intros x y; case y; clear y.";
for j = 0 to i - 1 do
- pp " intros y; unfold shiftr%i, Ndigits." i;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." i;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
pp " rewrite (spec_zdigits w%i_spec)." i;
@@ -2294,25 +2288,25 @@ let _ =
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
done;
- pp " intros y; unfold shiftr%i, Ndigits." i;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." i;
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
for j = i + 1 to size do
- pp " intros y; unfold shiftr%i, Ndigits." j;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." j;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
done;
if i == size then
begin
- pp " intros m y; unfold shiftrn, Ndigits.";
+ pp " intros m y; unfold unsafe_shiftrn, Ndigits.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
end
else
begin
- pp " intros m y; unfold shiftrn, Ndigits.";
+ pp " intros m y; unfold unsafe_shiftrn, Ndigits.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
@@ -2320,7 +2314,7 @@ let _ =
end
done;
pp " intros n x y; case y; clear y;";
- pp " intros y; unfold shiftrn, Ndigits; try rewrite spec_reduce_n.";
+ pp " intros y; unfold unsafe_shiftrn, Ndigits; try rewrite spec_reduce_n.";
for i = 0 to size do
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
@@ -2350,23 +2344,23 @@ let _ =
pp " Qed.";
pr "";
- (* Shiftl *)
+ (* Unsafe_Shiftl *)
for i = 0 to size do
- pr " Definition shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i
+ pr " Definition unsafe_shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i
done;
- pr " Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0).";
- pr " Definition shiftl := Eval lazy beta delta [same_level] in";
- pr " same_level _ (fun n x => %s0 (shiftl0 n x))" c;
+ pr " Definition unsafe_shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0).";
+ pr " Definition unsafe_shiftl := Eval lazy beta delta [same_level] in";
+ pr " same_level _ (fun n x => %s0 (unsafe_shiftl0 n x))" c;
for i = 1 to size do
- pr " (fun n x => reduce_%i (shiftl%i n x))" i i;
+ pr " (fun n x => reduce_%i (unsafe_shiftl%i n x))" i i;
done;
- pr " (fun n p x => reduce_n n (shiftln n p x)).";
+ pr " (fun n p x => reduce_n n (unsafe_shiftln n p x)).";
pr "";
pr "";
- pr " Theorem spec_shiftl: forall n x,";
- pr " [n] <= [head0 x] -> [shiftl n x] = [x] * 2 ^ [n].";
+ pr " Theorem spec_unsafe_shiftl: forall n x,";
+ pr " [n] <= [head0 x] -> [unsafe_shiftl n x] = [x] * 2 ^ [n].";
pa " Admitted.";
pp " Proof.";
pp " assert (F0: forall x y, x - (x - y) = y).";
@@ -2463,11 +2457,11 @@ let _ =
pp " rewrite Zpos_xO.";
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
pp " apply F5; auto with arith.";
- pp " intros x; case x; clear x; unfold shiftl, same_level.";
+ pp " intros x; case x; clear x; unfold unsafe_shiftl, same_level.";
for i = 0 to size do
pp " intros x y; case y; clear y.";
for j = 0 to i - 1 do
- pp " intros y; unfold shiftl%i, head0." i;
+ pp " intros y; unfold unsafe_shiftl%i, head0." i;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
pp " rewrite (spec_zdigits w%i_spec)." i;
@@ -2478,25 +2472,25 @@ let _ =
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j;
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
done;
- pp " intros y; unfold shiftl%i, head0." i;
+ pp " intros y; unfold unsafe_shiftl%i, head0." i;
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
for j = i + 1 to size do
- pp " intros y; unfold shiftl%i, head0." j;
+ pp " intros y; unfold unsafe_shiftl%i, head0." j;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
done;
if i == size then
begin
- pp " intros m y; unfold shiftln, head0.";
+ pp " intros m y; unfold unsafe_shiftln, head0.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
end
else
begin
- pp " intros m y; unfold shiftln, head0.";
+ pp " intros m y; unfold unsafe_shiftln, head0.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
@@ -2504,7 +2498,7 @@ let _ =
end
done;
pp " intros n x y; case y; clear y;";
- pp " intros y; unfold shiftln, head0; try rewrite spec_reduce_n.";
+ pp " intros y; unfold unsafe_shiftln, head0; try rewrite spec_reduce_n.";
for i = 0 to size do
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 116927766..85639aa6a 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -55,6 +55,9 @@ Module Type NType.
Parameter div : t -> t -> t.
Parameter modulo : t -> t -> t.
Parameter gcd : t -> t -> t.
+ Parameter shiftr : t -> t -> t.
+ Parameter shiftl : t -> t -> t.
+ Parameter is_even : t -> bool.
Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -76,6 +79,10 @@ Module Type NType.
Parameter spec_div: forall x y, [div x y] = [x] / [y].
Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
+ Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p].
+ Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p].
+ Parameter spec_is_even: forall x,
+ if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.
End NType.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 09:22:37 +0000