Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

do not depend on Ndigits #90

Merged
merged 1 commit into from
Apr 16, 2024
Merged

do not depend on Ndigits #90

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion BigN/NMake.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
representation. The representation-dependent (and macro-generated) part
is now in [NMake_gen]. *)

Require Import Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType
Require Import Bool BigNumPrelude ZArith Lia Nnat CyclicAxioms DoubleType
Nbasic Wf_nat StreamMemo NSig NMake_gen.

Module Make (W0:CyclicType) <: NType.
Expand Down
2 changes: 1 addition & 1 deletion BigN/Nbasic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)

Require Import ZArith Lia Ndigits.
Require Import ZArith Lia.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Expand Down
12 changes: 10 additions & 2 deletions BigN/gen/NMake_gen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ pr

(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)

Require Import BigNumPrelude ZArith Lia Ndigits CyclicAxioms
Require Import BigNumPrelude ZArith Lia CyclicAxioms
DoubleType DoubleMul DoubleDivn1 DoubleBase DoubleCyclic Nbasic
Wf_nat StreamMemo.

Expand Down Expand Up @@ -253,7 +253,7 @@ pr
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.
intros ww ww_op. simpl Pos.shiftl_nat. rewrite <- IHn; auto.
Qed.

Theorem nmake_double: forall n (ww:univ_of_cycles) (w_op: ZnZ.Ops ww),
Expand Down Expand Up @@ -347,6 +347,14 @@ pr "
rewrite make_op_S; auto.
Qed.

Local Lemma Pshiftl_nat_plus : forall n m p,
Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
Proof.
intros n m; induction m; simpl; intros.
- reflexivity.
- now f_equal.
Qed.

Lemma digits_make_op : forall n,
ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)).
Proof.
Expand Down
2 changes: 1 addition & 1 deletion CyclicDouble/DoubleBase.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

Set Implicit Arguments.

Require Import ZArith Ndigits.
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.

Expand Down
4 changes: 2 additions & 2 deletions CyclicDouble/DoubleDivn1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

Set Implicit Arguments.

Require Import ZArith Ndigits Lia.
Require Import ZArith Lia.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Expand Down Expand Up @@ -309,7 +309,7 @@ Section GENDIVN1.
[|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits).
Proof.
induction n;intros.
unfold high,double_to_Z. rewrite Pshiftl_nat_0.
unfold high,double_to_Z. simpl Pos.shiftl_nat.
replace (Zpos w_digits - Zpos w_digits) with 0;try ring.
simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith.
assert (U2 := spec_double_digits n).
Expand Down
Loading