Small changes

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 

theories/additions/Monoid_def.v

@@ -1,6 +1,4 @@
-Require Import RelationClasses.
-Require Import Relations Morphisms.
-Require Import String.
+From Coq Require Import RelationClasses Relations Morphisms String.
 
 Set Implicit Arguments.
 

theories/additions/More_on_positive.v

@@ -1,8 +1,8 @@
 
-Require Import Arith NArith Pow Compatibility Lia.
+From Coq Require Import Arith NArith  Lia Recdef.
+From additions Require Import Pow Compatibility Wf_transparent. 
 Open Scope positive_scope.
 Import Monoid_def.
-Require Import Recdef  Wf_transparent. 
 
 (** * Basic lemmas about positive and N *)
 

theories/additions/Trace_exercise.v

@@ -1,7 +1,8 @@
 (* Trace of a chain *)
 (** Solution to an exercise *)
 
-
+From Coq Require Import List.
+Import ListNotations.
 Require Import Addition_Chains PArith.
 
 

theories/additions/Wf_transparent.v

@@ -2,7 +2,7 @@
 *)
 
 
-Require Export Relation_Definitions.
+From Coq Require Export Relation_Definitions.
 
 Lemma wf_incl_transparent  :
 forall (A : Type) (R1 R2 : A -> A -> Prop),

theories/additions/fib.v

@@ -1,8 +1,7 @@
 (** author Yves Bertot, Inria  *)
 
 
-Require Import Extraction.
-Require Import ZArith Lia.
+From Coq Require Import Extraction ZArith Lia.
 
 From mathcomp Require Import all_ssreflect all_algebra.
 

theories/gaia/GHessenberg.v

@@ -6,8 +6,8 @@ From hydras Require Import DecPreOrder ON_Generic.
 From hydras Require Import T1 E0 Hessenberg.
 
 From gaia Require Export ssete9.
+From gaia_hydras Require Import T1Bridge. 
 
-Require Import T1Bridge. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 

theories/gaia/GLarge_Sets.v

@@ -7,7 +7,7 @@
 From mathcomp Require Import all_ssreflect zify.
 From hydras Require Import T1.
 From hydras Require Import Canon Paths Large_Sets.
-Require Import T1Bridge GCanon GPaths.
+From gaia_hydras Require Import T1Bridge GCanon GPaths.
 
 From gaia Require Import ssete9.
 Import CantorOrdinal. 

theories/gaia/GPaths.v

@@ -5,7 +5,7 @@
 
 From mathcomp Require Import all_ssreflect zify.
 From hydras Require Import Canon Paths.
-Require Import T1Bridge GCanon.
+From gaia_hydras Require Import T1Bridge GCanon.
 
 
 From hydras Require Import T1.

theories/gaia/GaiaToHydra.v

@@ -1,7 +1,7 @@
 (* begin snippet T1BridgeUse:: no-out *)
 
 From mathcomp Require Import all_ssreflect zify.
-Require Import T1Bridge . 
+From gaia_hydras Require Import T1Bridge . 
 From hydras Require Import T1. 
 
 From gaia Require Import ssete9.

theories/gaia/HydraGaia_Examples.v

@@ -5,7 +5,8 @@ From hydras Require Import DecPreOrder ON_Generic.
 From hydras Require Import T1 E0 Hessenberg.
 From gaia Require Export ssete9.
 
-Require Import T1Bridge GCanon GHessenberg GLarge_Sets. 
+From gaia_hydras Require Import T1Bridge GCanon GHessenberg 
+  GLarge_Sets. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/gaia/T1Choice.v

@@ -12,7 +12,7 @@ From mathcomp Require Import all_ssreflect zify.
 From Coq Require Import Logic.Eqdep_dec.
 From hydras Require Import DecPreOrder ON_Generic  T1 E0.
 From gaia Require Export ssete9.
-Require Import T1Bridge.
+From gaia_hydras Require Import T1Bridge.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/gaia/nfwfgaia.v

@@ -9,7 +9,7 @@
 
 
 From mathcomp
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+  Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import fintype bigop.
 
 Set Implicit Arguments.

theories/gaia/onType.v

@@ -205,7 +205,7 @@ Compute tricho om67 om12.
 
 (** To do :  Notation for epsilon0 *)
 
-Require Import T1Bridge.
+From gaia_hydras Require Import T1Bridge.
 
 Section ONEpsilon0Def. 
 

theories/goedel/PRrepresentable.v

@@ -29,7 +29,7 @@ From hydras Require Export MoreLibHyps NewNotations.
 Import NNnotations. 
 #[local] Arguments apply _ _ _ : clear implicits.
 Import LispAbbreviations. 
-Require Import Utf8.
+From Coq Require Import Utf8.
 
 Coercion natToTerm : nat >-> Term.
 

theories/goedel/goedel2.v

@@ -7,21 +7,15 @@ From hydras.Ackermann Require Import folReplace.
 From hydras.Ackermann Require Import folLogic3.
 From hydras.Ackermann Require Import subProp.
 From hydras.Ackermann Require Import ListExt.
-(*
-Require Import NNtheory.
-*)
+
 From Goedel Require Import fixPoint.
 From hydras.Ackermann Require Import NN2PA.
 From Goedel Require Import codeSysPrf.
 From hydras.Ackermann Require Import PAtheory.
 From hydras.Ackermann Require Import code.
-(*
-Require Import PRrepresentable.
-Require Import expressible.
-*)
 From hydras.Ackermann Require Import checkPrf.
 From hydras.Ackermann Require Import codeNatToTerm.
-Require Import rosserPA.
+From Goedel Require Import rosserPA.
 
 Section Goedel's_2nd_Incompleteness.
 

theories/ordinals/Ackermann/Deduction.v

@@ -6,9 +6,8 @@
 
 From Coq Require Import Ensembles List.
 
-Require Import folProof.
-Require Import folProp.
+From hydras.Ackermann Require Import folProof folProp.
 Import FolNotations.
 
 Section Deduction_Theorem.
 

theories/ordinals/Ackermann/LNN.v

@@ -8,9 +8,10 @@ Original version by Russel O'Connor
 
 From Coq Require Import Arith Ensembles List.
 
-Require Export Languages folProof  folProp  folLogic3.
+From hydras.Ackermann Require Export Languages folProof  
+  folProp  folLogic3.
 From LibHyps Require Import LibHyps. 
-Require Import MoreLibHyps NewNotations.
+From hydras Require Import MoreLibHyps NewNotations.
 
 (** * Instantiations of a few generic constructs 
 

theories/ordinals/Ackermann/LNN2LNT.v

@@ -10,8 +10,9 @@
 (* begin hide *)
 From Coq Require Import Ensembles List Arith.
 
-Require Import misc ListExt folProp folProof Languages  subAll  subProp.
-Require Import folLogic3  folReplace LNN LNT  codeNatToTerm  NewNotations.
+From hydras.Ackermann 
+ Require Import misc ListExt folProp folProof Languages  subAll  
+ subProp  folLogic3  folReplace LNN LNT  codeNatToTerm  NewNotations.
 
 Import FolNotations  NNnotations.
 

theories/ordinals/Ackermann/LNT.v

@@ -7,7 +7,8 @@ Original version by Russel O'Connor
 
 From Coq Require Import Arith Ensembles List.
 
-Require Import Languages  folProof  folProp  folLogic3.
+From hydras.Ackermann 
+ Require Import Languages  folProof  folProp  folLogic3.
 
 (** * Instantiations of a few generic constructs 
 

theories/ordinals/Ackermann/Languages.v

@@ -5,7 +5,7 @@
 (** TO do : reorganize Alectryon snippets *)
 
 From Coq Require Import Arith List.
-Require Import fol primRec code.
+From hydras.Ackermann Require Import fol primRec code.
 
 (**  * Language of Number Theory: [LNT] *)