Skip to content

Commit

Permalink
Merge pull request #208 from coq-community/stdlib_repo
Browse files Browse the repository at this point in the history
Adapt to coq/coq#19530
  • Loading branch information
Lysxia authored Sep 17, 2024
2 parents 7dc1ada + 823afcd commit e53316b
Showing 96 changed files with 251 additions and 249 deletions.
2 changes: 1 addition & 1 deletion algebra/CMonoids.v
Original file line number Diff line number Diff line change
@@ -36,7 +36,7 @@

(** printing [0] %\ensuremath{\mathbf0}% #0# *)

Require Export Coq.Arith.Euclid.
From Coq Require Export Euclid.
Require Export CoRN.model.Zmod.Cmod.
Require Export CoRN.algebra.CSemiGroups.
Require Export CoRN.tactics.csetoid_rewrite.
3 changes: 2 additions & 1 deletion algebra/CRing_as_Ring.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@

Require Export CoRN.algebra.CRings Coq.setoid_ring.Ring.
Require Export CoRN.algebra.CRings.
From Coq Require Export Ring.
Definition CRing_Ring(R:CRing):(ring_theory (@cm_unit R) (@cr_one R) (@csg_op R) (@cr_mult R) (fun x y => x [-] y) (@cg_inv R) (@cs_eq R)).
Proof.
split;algebra.
2 changes: 1 addition & 1 deletion algebra/CSums.v
Original file line number Diff line number Diff line change
@@ -41,7 +41,7 @@
(** printing Sumx %\ensuremath{\sum'}% #∑'&*)

Require Export CoRN.algebra.CAbGroups.
Require Export Coq.Arith.Peano_dec.
From Coq Require Export Peano_dec.
From Coq Require Import Lia.

(**
2 changes: 1 addition & 1 deletion algebra/Expon.v
Original file line number Diff line number Diff line change
@@ -36,7 +36,7 @@

(** printing [^^] %\ensuremath{\hat{\ }}% #^# *)

Require Export Coq.Arith.Arith.
From Coq Require Export Arith.
Require Export CoRN.algebra.COrdCauchy.
From Coq Require Import Lia.

4 changes: 2 additions & 2 deletions complex/NRootCC.v
Original file line number Diff line number Diff line change
@@ -40,8 +40,8 @@
(** printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)

Require Export CoRN.complex.CComplex.
Require Export Coq.Arith.Wf_nat.
Require Export Coq.setoid_ring.ArithRing.
From Coq Require Export Wf_nat.
From Coq Require Export ArithRing.
Import CRing_Homomorphisms.coercions.

(**
22 changes: 11 additions & 11 deletions coq_reals/Rreals_iso.v
Original file line number Diff line number Diff line change
@@ -17,22 +17,22 @@
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)

Require Import Coq.QArith.QArith.
Require Import Coq.QArith.Qreals.
Require Import Coq.QArith.QArith_base.
From Coq Require Import QArith.
From Coq Require Import Qreals.
From Coq Require Import QArith_base.
Require Import CoRN.tactics.CornTac.
Require Import Coq.Reals.RIneq.
Require Import Coq.Reals.Rcomplete.
Require Import Coq.Reals.Rlimit.
Require Import Coq.Reals.Rbasic_fun.
From Coq Require Import RIneq.
From Coq Require Import Rcomplete.
From Coq Require Import Rlimit.
From Coq Require Import Rbasic_fun.
Require Import CoRN.coq_reals.Rreals.
Require Import CoRN.reals.iso_CReals.
Require Import CoRN.reals.CauchySeq.
Require Import Coq.Reals.Rtrigo_def.
From Coq Require Import Rtrigo_def.
Require Import CoRN.transc.PowerSeries.
Require Import Coq.Logic.ConstructiveEpsilon.
Require Import Coq.Reals.Rlogic.
Require Export Coq.Reals.Reals.
From Coq Require Import ConstructiveEpsilon.
From Coq Require Import Rlogic.
From Coq Require Export Reals.
Require Import CoRN.transc.Pi.
Require Import CoRN.transc.MoreArcTan.
Require Import CoRN.logic.PropDecid.
4 changes: 2 additions & 2 deletions fta/KeyLemma.v
Original file line number Diff line number Diff line change
@@ -34,8 +34,8 @@
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)

Require Export Coq.ZArith.ZArith.
Require Export Coq.Arith.Compare.
From Coq Require Export ZArith.
From Coq Require Export Compare.
Require Export CoRN.reals.NRootIR.
From Coq Require Import Lia.

2 changes: 1 addition & 1 deletion ftc/WeakIVTQ.v
Original file line number Diff line number Diff line change
@@ -7,7 +7,7 @@ Definition Q2R (q: Q) : IR := (inj_Q IR q).
Coercion Q2R : Q >-> st_car.


Require Import Coq.setoid_ring.Ring.
From Coq Require Import Ring.
Require Import CoRN.tactics.CornTac.
Require Import CoRN.algebra.CRing_as_Ring.

8 changes: 4 additions & 4 deletions logic/CLogic.v
Original file line number Diff line number Diff line change
@@ -44,11 +44,11 @@
(** printing or %\ensuremath{\mathrel\vee}% *)
(** printing and %\ensuremath{\mathrel\wedge}% *)

Require Export Coq.Arith.Compare_dec.
From Coq Require Export Compare_dec.
Require Export CoRN.logic.CornBasics.
Require Export Coq.ZArith.ZArith.
Require Export Coq.setoid_ring.ZArithRing.
Require Export Coq.Arith.Wf_nat.
From Coq Require Export ZArith.
From Coq Require Export ZArithRing.
From Coq Require Export Wf_nat.
From Coq Require Import Lia.


4 changes: 2 additions & 2 deletions logic/CornBasics.v
Original file line number Diff line number Diff line change
@@ -48,8 +48,8 @@
From Coq Require Export ZArith.
From Coq Require Import Lia.
Require Export CoRN.stdlib_omissions.List.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Setoids.Setoid.
From Coq Require Import Eqdep_dec.
From Coq Require Import Setoid.

Tactic Notation "apply" ":" constr(x) := pose proof x as HHH; first [
refine HHH |
6 changes: 3 additions & 3 deletions metric2/Compact.v
Original file line number Diff line number Diff line change
@@ -21,11 +21,11 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
Require Import CoRN.model.totalorder.QposMinMax.
Require Import CoRN.metric2.Limit.
Require Export CoRN.metric2.FinEnum.
Require Import Coq.ZArith.Zpow_facts.
From Coq Require Import Zpow_facts.
Require Export CoRN.metric2.Complete.
Require Import CoRN.logic.Classic.
Require Import Coq.QArith.Qpower.
Require Import Coq.QArith.Qround.
From Coq Require Import Qpower.
From Coq Require Import Qround.

Set Implicit Arguments.

2 changes: 1 addition & 1 deletion metric2/Hausdorff.v
Original file line number Diff line number Diff line change
@@ -23,7 +23,7 @@ Require Import CoRN.logic.Classic.
Require Export CoRN.metric2.Metric.
Require Import CoRN.metric2.Classification.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
From Coq Require Import ZArith.
Require Import CoRN.model.totalorder.QMinMax.
Require Import CoRN.model.totalorder.QposMinMax.

4 changes: 2 additions & 2 deletions metric2/Limit.v
Original file line number Diff line number Diff line change
@@ -21,8 +21,8 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.

Require Import CoRN.algebra.RSetoid.
Require Import CoRN.model.totalorder.QposMinMax.
Require Import Coq.QArith.QArith.
Require Import Coq.Bool.Bool.
From Coq Require Import QArith.
From Coq Require Import Bool.
Require Export CoRN.metric2.Complete.
Require Export MathClasses.theory.CoqStreams.
Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals.
4 changes: 2 additions & 2 deletions metric2/Metric.v
Original file line number Diff line number Diff line change
@@ -20,8 +20,8 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
*)

Require Export Coq.QArith.QArith.
Require Import CoRN.algebra.RSetoid.
From Coq Require Export QArith.
Require Import CoRN.algebra.RSetoid.
Require Import MathClasses.interfaces.canonical_names.
Require Import MathClasses.interfaces.abstract_algebra.

2 changes: 1 addition & 1 deletion model/Zmod/ZBasics.v
Original file line number Diff line number Diff line change
@@ -35,7 +35,7 @@
*)
(* ZBasics.v, by Vince Barany *)

Require Export Coq.ZArith.ZArith.
From Coq Require Export ZArith.
Require Export CoRN.logic.CLogic.
From Coq Require Import Lia.

16 changes: 8 additions & 8 deletions model/Zmod/ZDivides.v
Original file line number Diff line number Diff line change
@@ -503,10 +503,10 @@ Proof.
case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
auto with zarith.
intros p q.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
intros Hlt Hp HR; rewrite HR; auto with zarith.
intros p q.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
case R.
auto with zarith.
intro r'; intros H0 H1 H2.
@@ -518,10 +518,10 @@ Proof.
case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
auto with zarith.
intros p q.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith.
intros p q.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
case R; intros; try discriminate; try tauto.
Qed.

@@ -536,12 +536,12 @@ Proof.
case b; unfold Z.opp in |- *.
auto.
intro B.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
intro Hr; rewrite Hr; auto.
intro B.
generalize (Z_mod_lt (Zpos A) (Zpos B)).
unfold Z.modulo, Z.div_eucl in |- *.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
case r.
intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
intros R Hlt HR.
@@ -558,7 +558,7 @@ Proof.
intro B.
generalize (Z_mod_lt (Zpos A) (Zpos B)).
unfold Z.modulo, Z.div_eucl in |- *.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
case r.
intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
intros R Hlt HR.
@@ -572,7 +572,7 @@ Proof.
intro B.
generalize (Z_mod_lt (Zpos A) (Zpos B)).
unfold Z.modulo, Z.div_eucl in |- *.
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
case r.
intros _ HR; fold (- q)%Z in |- *; auto.
intros; discriminate.
4 changes: 2 additions & 2 deletions model/metric2/L1metric.v
Original file line number Diff line number Diff line change
@@ -26,9 +26,9 @@ Require Export CoRN.model.structures.StepQsec.
Require Export CoRN.metric2.UniformContinuity.
Require Import CoRN.metric2.Prelength.
Require Import CoRN.model.structures.OpenUnit.
Require Import Coq.QArith.QArith.
From Coq Require Import QArith.
Require Import CoRN.model.totalorder.QMinMax.
Require Import Coq.QArith.Qabs.
From Coq Require Import Qabs.
Require Import CoRN.model.ordfields.Qordfield.
Require Import CoRN.model.metric2.Qmetric.
Require Import CoRN.algebra.COrdFields2.
4 changes: 2 additions & 2 deletions model/metric2/LinfMetric.v
Original file line number Diff line number Diff line change
@@ -27,9 +27,9 @@ Require Import CoRN.metric2.Prelength.
Require Import CoRN.model.metric2.L1metric.
Require Export CoRN.model.metric2.LinfMetricMonad.
Require Import CoRN.model.structures.OpenUnit.
Require Import Coq.QArith.QArith.
From Coq Require Import QArith.
Require Import CoRN.model.totalorder.QMinMax.
Require Import Coq.QArith.Qabs.
From Coq Require Import Qabs.
Require Import CoRN.model.ordfields.Qordfield.
Require Import CoRN.model.metric2.Qmetric.
Require Import CoRN.algebra.COrdFields2.
4 changes: 2 additions & 2 deletions model/metric2/LinfMetricMonad.v
Original file line number Diff line number Diff line change
@@ -29,9 +29,9 @@ Require Export CoRN.metric2.StepFunctionSetoid.
Require Import CoRN.metric2.StepFunctionMonad.
Require Import CoRN.metric2.UniformContinuity.
Require Import CoRN.model.structures.OpenUnit.
Require Import Coq.QArith.QArith.
From Coq Require Import QArith.
Require Import CoRN.model.totalorder.QMinMax.
Require Import Coq.QArith.Qabs.
From Coq Require Import Qabs.
Require Import CoRN.model.ordfields.Qordfield.
Require Import CoRN.model.metric2.Qmetric.
Require Import CoRN.metric2.Prelength.
4 changes: 2 additions & 2 deletions model/metric2/Qmetric.v
Original file line number Diff line number Diff line change
@@ -24,7 +24,7 @@ Require Import CoRN.metric2.Prelength.
Require Import CoRN.metric2.Classification.
Require Import CoRN.model.totalorder.QMinMax.
Require Import CoRN.model.totalorder.QposMinMax.
Require Import Coq.QArith.Qabs.
From Coq Require Import Qabs.
Require Import CoRN.metric2.UniformContinuity.
Require Import MathClasses.implementations.stdlib_rationals.

@@ -444,7 +444,7 @@ Proof with auto.
apply ball_sym...
Qed.

Require Import Coq.QArith.Qround.
From Coq Require Import Qround.

Lemma Qfloor_ball q:
Qball (1#2) ((Qfloor q # 1) + (1#2)) q.
2 changes: 1 addition & 1 deletion model/setoids/Zfinsetoid.v
Original file line number Diff line number Diff line change
@@ -33,7 +33,7 @@
* with this work; if not, write to the Free Software Foundation, Inc.,
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
Require Export Coq.ZArith.ZArith.
From Coq Require Export ZArith.
Require Import CoRN.algebra.CSetoids.

(**
7 changes: 2 additions & 5 deletions model/setoids/decsetoid.v
Original file line number Diff line number Diff line change
@@ -4,11 +4,8 @@

Set Implicit Arguments.

Require Import
CoRN.algebra.CSetoids
Coq.Classes.SetoidDec
Coq.Classes.Morphisms
Coq.Classes.SetoidClass.
Require Import CoRN.algebra.CSetoids.
From Coq Require Import SetoidDec Morphisms SetoidClass.


Class Apartness `{SetoidClass.Setoid} (ap: Crelation A): Type :=
5 changes: 3 additions & 2 deletions model/structures/NNUpperR.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
(* This module is designed to *not* be Import'ed, only Require'd. *)

Require Import
Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program.
From Coq Require Import Qabs.
Require Import CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec.
From Coq Require Import Qminmax Ring Program.

Require CoRN.model.structures.QnonNeg.
Import QnonNeg.notations QnonNeg.coercions.
4 changes: 2 additions & 2 deletions model/structures/Nsec.v
Original file line number Diff line number Diff line change
@@ -36,8 +36,8 @@

(** printing {#N} $\ensuremath{\mathrel\#_{\mathbb N}}$ *)

Require Export Coq.Arith.Peano_dec.
Require Export Coq.Relations.Relations.
From Coq Require Export Peano_dec.
From Coq Require Export Relations.
Require Import CoRN.logic.CLogic.
From Coq Require Import Lia.

2 changes: 1 addition & 1 deletion model/structures/OpenUnit.v
Original file line number Diff line number Diff line change
@@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
*)
Require Export Coq.QArith.QArith.
From Coq Require Export QArith.
Require Import CoRN.model.ordfields.Qordfield.
Require Import CoRN.algebra.COrdFields.
Require Import CoRN.tactics.Qauto.
7 changes: 3 additions & 4 deletions model/structures/Qinf.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
Require Import
CoRN.model.totalorder.QposMinMax
Coq.Setoids.Setoid Coq.Arith.Arith
CoRN.model.rings.Qring CoRN.model.structures.QposInf
Require Import CoRN.model.totalorder.QposMinMax.
From Coq Require Import Setoid Arith.
Require Import CoRN.model.rings.Qring CoRN.model.structures.QposInf
CoRN.stdlib_omissions.Q
MathClasses.interfaces.abstract_algebra
MathClasses.implementations.stdlib_rationals
6 changes: 4 additions & 2 deletions model/structures/QnonNeg.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
(* This module is designed to *not* be Import'ed, only Require'd. *)

Require Import CoRN.model.totalorder.QposMinMax
Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax.
Require Import CoRN.model.totalorder.QposMinMax.
From Coq Require Import Program.
Require Import CoRN.model.structures.QposInf.
From Coq Require Import Qminmax.


(* The data type and simple relations/constants: *)
2 changes: 1 addition & 1 deletion model/structures/QposInf.v
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
*)

Require Export Coq.QArith.QArith.
From Coq Require Export QArith.
Require Import CoRN.model.totalorder.QposMinMax.

(** printing QposInf $\mathbb{Q}^{+}_{\infty}$ #Q<SUP>+</SUP><SUB>&infin;</SUB># *)
Loading

0 comments on commit e53316b

Please sign in to comment.