do not depend on Ndigits

coq-community · Apr 15, 2024 · 24834fb · 24834fb
1 parent e6085d6
commit 24834fb
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 7 deletions.
diff --git a/BigN/NMake.v b/BigN/NMake.v
@@ -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.

diff --git a/BigN/Nbasic.v b/BigN/Nbasic.v
@@ -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.

diff --git a/BigN/gen/NMake_gen.ml b/BigN/gen/NMake_gen.ml
@@ -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.
 
@@ -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),
@@ -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.

diff --git a/CyclicDouble/DoubleBase.v b/CyclicDouble/DoubleBase.v
@@ -10,7 +10,7 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Ndigits.
+Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 

diff --git a/CyclicDouble/DoubleDivn1.v b/CyclicDouble/DoubleDivn1.v
@@ -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.
@@ -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).