Small changes (#169)

* Make Require commands more explicit (with From)

* Add From to Requires

* Fix a deprecation error

The suggested replacement of N.div_le_mono with N.Div0.le_mono caused an error
in versions < 8.17

Author: Casteran

theories/additions/AM.v

@@ -4,16 +4,19 @@
 (** Work in progress 
 
 *)
-
-Require Import Monoid_def Monoid_instances List PArith Relations.
-Require Import Strategies Lia.
-Generalizable All Variables.
+From Coq Require Import List PArith Relations Lia.
 Import Morphisms.
+
+From additions Require Import Monoid_def Monoid_instances Strategies.
 Import Monoid_def.
-Require Import Recdef Wf_nat.
-Require Import More_on_positive.
-Require  Import Pow.
-Require Import Euclidean_Chains.
+
+From Coq Require Import Recdef Wf_nat.
+From additions Require Import More_on_positive Pow  Euclidean_Chains
+  Dichotomy BinaryStrat.
+Generalizable All Variables.
+
+
+
 
 (** basic instructions *)
 (* begin snippet AMDef *)
@@ -137,7 +140,7 @@ Compute chain_apply C31_7 Natplus 1%nat.
 
 (* end snippet AMSemb *)
 
-Require Import NArith.
+From Coq Require Import NArith.
 
 Compute chain_apply C31_7 NMult 2%N.
 
@@ -522,8 +525,6 @@ Section CompositionProofs.
 
 (** *  Euclidean chain generation *)
 
-Require Import Dichotomy BinaryStrat.
-
 Definition  OK (s: signature) 
   := fun c: code => correctness_statement s c.
 

theories/additions/Addition_Chains.v

@@ -4,12 +4,11 @@ Pierre Casteran, LaBRI, University of Bordeaux
 
 *)
 
-Require Export Monoid_instances Pow Lia List.
-Require Import Relations RelationClasses.
-
+From additions Require Export Monoid_instances Pow.
+From Coq Require Import Relations RelationClasses Lia List.
 From Param Require Import Param.
 
-Require Import More_on_positive.
+From additions Require Import More_on_positive.
 Generalizable Variables A op one Aeq.
 Infix "==" := Monoid_def.equiv (at level 70) : type_scope.
 Open Scope nat_scope.

theories/additions/BinaryStrat.v

@@ -6,8 +6,9 @@
 *)
 
 
-Require Import Arith NArith Pow Compatibility More_on_positive Lia.
-Require Export Strategies.
+From Coq Require Import Arith NArith Lia.
+From additions Require Import  Pow Compatibility More_on_positive.
+From additions Require Export Strategies.
 
 Open Scope positive_scope.
 

theories/additions/Compatibility.v

@@ -7,9 +7,9 @@ equivalence theorems with functions defined in our module [Pow].
 
  *)
 
-Require Import Monoid_def Lia Monoid_instances
-     ArithRing  Pow.
-
+From additions Require Import Monoid_def Monoid_instances
+       Pow.
+From Coq Require Import Lia ArithRing.
 
 (** ** really logarithmic versions of N.pow, Pos.pow and Z.pow 
  

theories/additions/Demo.v

@@ -4,9 +4,7 @@ Module Alt.
 
 End Alt.
 
-Require Import Arith Lia.
-
-Require Import Even.
+From Coq Require Import Arith Lia Even.
 
 Lemma alt_double_ok n : Nat.double n = Alt.double n.
 Proof.

theories/additions/Demo_power.v

@@ -1,6 +1,4 @@
-Require Import Monoid_def 
-               Monoid_instances
-               Pow.
+From additions Require Import Monoid_def Monoid_instances Pow.
 (* begin snippet DemoPower *)
 Open Scope M_scope.
 

theories/additions/Dichotomy.v

@@ -9,8 +9,9 @@
 *)
 
 
-Require Import Arith NArith Pow Compatibility More_on_positive.
-Require Export Strategies.
+From Coq Require Import Arith NArith.
+From additions Require Export Strategies Pow Compatibility 
+  More_on_positive.
 
 Open Scope positive_scope.
 
@@ -170,8 +171,7 @@ Proof.
 intros p H; unfold dicho; generalize (dicho_aux_lt p H).
 intro H0; assert (2 <= N.pos p / (N.pos (dicho_aux p)) )%N.
 - replace 2%N with (2%N * Npos (dicho_aux p) / Npos (dicho_aux p))%N.
-  + apply N.div_le_mono.
-    * discriminate.
+  + apply (* N.Div0.div_le_mono. *) N.div_le_mono; try discriminate. 
     * replace 2%N with (Npos 2%positive); cbn;auto.
   + rewrite N.div_mul; [auto | discriminate].
 - case_eq (N.pos p / N.pos (dicho_aux p))%N.

theories/additions/Euclidean_Chains.v

@@ -14,13 +14,12 @@ small computation may be parameterized by the context in which it will be
 
 
 
-Require Import Inverse_Image  Inclusion  Wf_nat.
-Require Import Addition_Chains  NArith  Arith PArith  Compatibility.  
-Require Import More_on_positive.
-Import Monoid_def  Pow.
-Require Import Recdef Wf_nat.
-Require Import  More_on_positive .
-Require Import Wf_transparent Lexicographic_Product  Dichotomy BinaryStrat.
+From Coq Require Import Inverse_Image  Inclusion  Wf_nat 
+  NArith  Arith PArith Recdef Wf_nat Lexicographic_Product Lia.
+From additions Require Import Addition_Chains    Compatibility 
+  More_on_positive Wf_transparent   Dichotomy BinaryStrat.
+From Coq Require Import Lia.
+
 Generalizable All Variables.
 Import Morphisms.
 Import Monoid_def.
@@ -1538,7 +1537,7 @@ Arguments big_chain _%type_scope.
 Remark RM : (1 < 56789)%N. 
 Proof. reflexivity. Qed.
 
-Definition M := Nmod_Monoid _ RM.
+Definition M := Nmod_Monoid  _ RM.
 
 Definition exp56789 x := chain_apply big_chain (M:=M) x.
 

theories/additions/Fib2.v

@@ -1,6 +1,8 @@
 
 
-Require Import NArith Ring Monoid_instances Euclidean_Chains Pow
+From Coq Require Import NArith Ring.
+
+From additions Require Import Monoid_instances Euclidean_Chains Pow
         Strategies Dichotomy BinaryStrat.
 Import Addition_Chains. 
 Open Scope N_scope.
@@ -135,7 +137,8 @@ Time Compute fib_eucl half 153.
 Finished transaction in 0.002 secs (0.002u,0.s) (successful)
 *)
 
-Require Import AM.
+From additions Require Import AM.
+
 Definition fib_with_chain c :=
   match chain_apply c  Mul2 (1,0) with
     Some ((a,b), nil) => Some (a+b) | _ => None end.

theories/additions/FirstSteps.v

@@ -1,7 +1,6 @@
 (** Polymorphic versions of exponentiation functions *)
 
-Require Import Arith ZArith.
-Require Import String.
+From Coq Require Import Arith ZArith String.
 
 (** 
   Polymorphic exponentiation functions