Created
May 7, 2015 20:34
-
-
Save JasonGross/14decf638535a2447286 to your computer and use it in GitHub Desktop.
Patch for trunk branch of https://gforge.inria.fr/git/coq-contribs/math-classes.git
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| commit ec8f935df189b4857b064768d86591bb035b8783 | |
| Author: Jason Gross <jgross@mit.edu> | |
| Date: Thu May 7 16:27:10 2015 -0400 | |
| Absolutize all [Import]s | |
| Previously, on case-insensitive file systems, Coq thought that [Require | |
| Import List] meant [Require Import MathClasses.implementations.List] | |
| (which is invalid), not [Require Import Coq.Lists.List]. This fixes | |
| that. | |
| This commit was fully automatic, achieved by running | |
| ``` | |
| make | |
| git ls-files "*.v" | xargs python /path/to/coq-tools/absolutize-imports.py -R . MathClasses | |
| ``` | |
| where `/path/to/coq-tools` is the path to a local clone of my [coq-tools | |
| repository](https://github.com/JasonGross/coq-tools). | |
| diff --git a/categories/JMcat.v b/categories/JMcat.v | |
| index 401fc32..3151f22 100644 | |
| --- a/categories/JMcat.v | |
| +++ b/categories/JMcat.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - JMrelation. | |
| + MathClasses.misc.JMrelation. | |
| Require Import | |
| - abstract_algebra interfaces.functors theory.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories. | |
| Record Object := object | |
| { obj:> Type | |
| diff --git a/categories/algebras.v b/categories/algebras.v | |
| index 1c5046a..d381c49 100644 | |
| --- a/categories/algebras.v | |
| +++ b/categories/algebras.v | |
| @@ -1,8 +1,8 @@ | |
| (* Show that algebras with homomorphisms between them form a category. *) | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms theory.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories. | |
| Require | |
| - categories.setoids categories.product. | |
| + MathClasses.categories.setoids MathClasses.categories.product. | |
| Record Object (sign: Signature) : Type := object | |
| { algebra_carriers:> sorts sign → Type | |
| diff --git a/categories/categories.v b/categories/categories.v | |
| index df0503f..7886fa1 100644 | |
| --- a/categories/categories.v | |
| +++ b/categories/categories.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.functors theory.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories. | |
| Record Object := object | |
| { obj:> Type | |
| diff --git a/categories/dual.v b/categories/dual.v | |
| index eec6808..60f0c3e 100644 | |
| --- a/categories/dual.v | |
| +++ b/categories/dual.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Relation_Definitions abstract_algebra theory.categories interfaces.functors. | |
| + Coq.Relations.Relation_Definitions MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.interfaces.functors. | |
| Section contents. | |
| diff --git a/categories/empty.v b/categories/empty.v | |
| index 5a5d40b..2a3c02e 100644 | |
| --- a/categories/empty.v | |
| +++ b/categories/empty.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.functors. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors. | |
| Definition Empty_map {A: Empty_set → Type} : ∀ x : Empty_set, A x := λ x, match x with end. | |
| Local Notation E := Empty_map. | |
| diff --git a/categories/functors.v b/categories/functors.v | |
| index 4aa1392..8c86dbe 100644 | |
| --- a/categories/functors.v | |
| +++ b/categories/functors.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.functors theory.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories. | |
| Section natural_transformations_id_comp. | |
| Context | |
| diff --git a/categories/orders.v b/categories/orders.v | |
| index 0b03b0e..41fc560 100644 | |
| --- a/categories/orders.v | |
| +++ b/categories/orders.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - abstract_algebra theory.categories orders.maps interfaces.orders orders.orders | |
| - interfaces.functors. | |
| -Require categories.setoids. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.orders.maps MathClasses.interfaces.orders MathClasses.orders.orders | |
| + MathClasses.interfaces.functors. | |
| +Require MathClasses.categories.setoids. | |
| Inductive Object := object { T:> Type; e: Equiv T; le: Le T; setoid_proof: Setoid T; po_proof: PartialOrder le }. | |
| Existing Instance e. | |
| diff --git a/categories/product.v b/categories/product.v | |
| index 65e9c81..811822b 100644 | |
| --- a/categories/product.v | |
| +++ b/categories/product.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - abstract_algebra ChoiceFacts interfaces.functors | |
| - theory.categories categories.categories. | |
| + MathClasses.interfaces.abstract_algebra Coq.Logic.ChoiceFacts MathClasses.interfaces.functors | |
| + MathClasses.theory.categories MathClasses.categories.categories. | |
| (* Axiom dependent_functional_choice: DependentFunctionalChoice. *) | |
| diff --git a/categories/setoids.v b/categories/setoids.v | |
| index b63daaf..ab5f364 100644 | |
| --- a/categories/setoids.v | |
| +++ b/categories/setoids.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra theory.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.categories. | |
| Inductive Object := object { T:> Type; e: Equiv T; setoid_proof: Setoid T }. | |
| Arguments object _ {e setoid_proof}. | |
| diff --git a/categories/unit.v b/categories/unit.v | |
| index 28f8546..36a2c16 100644 | |
| --- a/categories/unit.v | |
| +++ b/categories/unit.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - RelationClasses Equivalence | |
| - categories.categories abstract_algebra categories.functors. | |
| + Coq.Classes.RelationClasses Coq.Classes.Equivalence | |
| + MathClasses.categories.categories MathClasses.interfaces.abstract_algebra MathClasses.categories.functors. | |
| Instance: Arrows unit := λ _ _, unit. | |
| Instance: CatId unit := λ _, tt. | |
| diff --git a/categories/varieties.v b/categories/varieties.v | |
| index 7e9ce19..c1d0c0b 100644 | |
| --- a/categories/varieties.v | |
| +++ b/categories/varieties.v | |
| @@ -5,7 +5,7 @@ factor out the commonality. | |
| *) | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms. | |
| Record Object (et: EquationalTheory) : Type := object | |
| { variety_carriers:> sorts et → Type | |
| diff --git a/functors/constant.v b/functors/constant.v | |
| index 52b307a..d4766ce 100644 | |
| --- a/functors/constant.v | |
| +++ b/functors/constant.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - theory.categories abstract_algebra interfaces.functors. | |
| + MathClasses.theory.categories MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors. | |
| Section constant_functor. | |
| Context `{Category A} `{Category B}. | |
| diff --git a/implementations/NType_naturals.v b/implementations/NType_naturals.v | |
| index 75a903f..10ee4a1 100644 | |
| --- a/implementations/NType_naturals.v | |
| +++ b/implementations/NType_naturals.v | |
| @@ -1,9 +1,9 @@ | |
| Require | |
| - stdlib_binary_integers theory.integers orders.semirings. | |
| + MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings. | |
| Require Import | |
| - Setoid NSig NSigNAxioms NArith ZArith Program Morphisms | |
| - abstract_algebra interfaces.naturals interfaces.integers | |
| - interfaces.orders interfaces.additional_operations. | |
| + Coq.Setoids.Setoid Coq.Numbers.Natural.SpecViaZ.NSig Coq.Numbers.Natural.SpecViaZ.NSigNAxioms Coq.NArith.NArith Coq.ZArith.ZArith Coq.Program.Program Coq.Classes.Morphisms | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers | |
| + MathClasses.interfaces.orders MathClasses.interfaces.additional_operations. | |
| Module NType_Integers (Import anyN: NType). | |
| diff --git a/implementations/QType_rationals.v b/implementations/QType_rationals.v | |
| index 175f6c8..7949a57 100644 | |
| --- a/implementations/QType_rationals.v | |
| +++ b/implementations/QType_rationals.v | |
| @@ -1,10 +1,10 @@ | |
| Require | |
| - theory.fields stdlib_rationals theory.int_pow. | |
| + MathClasses.theory.fields MathClasses.implementations.stdlib_rationals MathClasses.theory.int_pow. | |
| Require Import | |
| - QArith QSig | |
| - abstract_algebra interfaces.orders | |
| - interfaces.integers interfaces.rationals interfaces.additional_operations | |
| - theory.rings theory.rationals. | |
| + Coq.QArith.QArith Coq.Numbers.Rational.SpecViaQ.QSig | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders | |
| + MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations | |
| + MathClasses.theory.rings MathClasses.theory.rationals. | |
| Module QType_Rationals (Import anyQ: QType). | |
| diff --git a/implementations/ZType_integers.v b/implementations/ZType_integers.v | |
| index 7052cfe..3024e21 100644 | |
| --- a/implementations/ZType_integers.v | |
| +++ b/implementations/ZType_integers.v | |
| @@ -1,9 +1,9 @@ | |
| Require | |
| - stdlib_binary_integers theory.integers orders.semirings. | |
| + MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings. | |
| Require Import | |
| - ZSig ZSigZAxioms NArith ZArith | |
| - nonneg_integers_naturals interfaces.orders | |
| - abstract_algebra interfaces.integers interfaces.additional_operations. | |
| + Coq.Numbers.Integer.SpecViaZ.ZSig Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith | |
| + MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations. | |
| Module ZType_Integers (Import anyZ: ZType). | |
| diff --git a/implementations/bool.v b/implementations/bool.v | |
| index 330e9c0..5c19899 100644 | |
| --- a/implementations/bool.v | |
| +++ b/implementations/bool.v | |
| @@ -1,4 +1,4 @@ | |
| -Require Import abstract_algebra. | |
| +Require Import MathClasses.interfaces.abstract_algebra. | |
| Instance bool_eq: Equiv bool := eq. | |
| Instance bool_bottom: Bottom bool := false. | |
| diff --git a/implementations/dyadics.v b/implementations/dyadics.v | |
| index b3c3325..c5adfe8 100644 | |
| --- a/implementations/dyadics.v | |
| +++ b/implementations/dyadics.v | |
| @@ -4,12 +4,12 @@ | |
| embedded into any [Rationals] implementation [Q]. | |
| *) | |
| Require Import | |
| - Ring abstract_algebra | |
| - interfaces.integers interfaces.naturals interfaces.rationals | |
| - interfaces.additional_operations interfaces.orders | |
| - orders.minmax orders.integers orders.rationals | |
| - nonneg_integers_naturals stdlib_rationals | |
| - theory.rationals theory.shiftl theory.int_pow theory.nat_pow theory.abs. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra | |
| + MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders | |
| + MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals | |
| + MathClasses.implementations.nonneg_integers_naturals MathClasses.implementations.stdlib_rationals | |
| + MathClasses.theory.rationals MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.theory.abs. | |
| Record Dyadic Z := dyadic { mant: Z; expo: Z }. | |
| Arguments dyadic {Z} _ _. | |
| diff --git a/implementations/fast_integers.v b/implementations/fast_integers.v | |
| index e269045..3308c31 100644 | |
| --- a/implementations/fast_integers.v | |
| +++ b/implementations/fast_integers.v | |
| @@ -1,9 +1,9 @@ | |
| Require Import | |
| - BigZ | |
| - interfaces.abstract_algebra interfaces.integers | |
| - interfaces.additional_operations fast_naturals. | |
| + Coq.Numbers.Integer.BigZ.BigZ | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers | |
| + MathClasses.interfaces.additional_operations MathClasses.implementations.fast_naturals. | |
| Require Export | |
| - ZType_integers. | |
| + MathClasses.implementations.ZType_integers. | |
| Module BigZ_Integers := ZType_Integers BigZ. | |
| diff --git a/implementations/fast_naturals.v b/implementations/fast_naturals.v | |
| index c26cd29..77e1102 100644 | |
| --- a/implementations/fast_naturals.v | |
| +++ b/implementations/fast_naturals.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - BigN interfaces.naturals. | |
| + Coq.Numbers.Natural.BigN.BigN MathClasses.interfaces.naturals. | |
| Require Export | |
| - NType_naturals. | |
| + MathClasses.implementations.NType_naturals. | |
| Module BigN_Integers := NType_Integers BigN. | |
| diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v | |
| index 1884d7f..30492da 100644 | |
| --- a/implementations/fast_rationals.v | |
| +++ b/implementations/fast_rationals.v | |
| @@ -1,12 +1,12 @@ | |
| Require | |
| - theory.shiftl theory.int_pow. | |
| + MathClasses.theory.shiftl MathClasses.theory.int_pow. | |
| Require Import | |
| - QArith BigQ | |
| - abstract_algebra | |
| - interfaces.integers interfaces.rationals interfaces.additional_operations | |
| - fast_naturals fast_integers field_of_fractions stdlib_rationals. | |
| + Coq.QArith.QArith Coq.Numbers.Rational.BigQ.BigQ | |
| + MathClasses.interfaces.abstract_algebra | |
| + MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations | |
| + MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals. | |
| Require Export | |
| - QType_rationals. | |
| + MathClasses.implementations.QType_rationals. | |
| Module Import BigQ_Rationals := QType_Rationals BigQ. | |
| diff --git a/implementations/field_of_fractions.v b/implementations/field_of_fractions.v | |
| index 647861c..8ec46e6 100644 | |
| --- a/implementations/field_of_fractions.v | |
| +++ b/implementations/field_of_fractions.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - Ring abstract_algebra | |
| - theory.rings theory.dec_fields. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra | |
| + MathClasses.theory.rings MathClasses.theory.dec_fields. | |
| Inductive Frac R `{Rap : Equiv R} `{Rzero : Zero R} : Type := frac { num: R; den: R; den_ne_0: den ≠0 }. | |
| (* We used to have [den] and [den_nonzero] bundled, which did work relatively nicely with Program, but the | |
| diff --git a/implementations/intfrac_rationals.v b/implementations/intfrac_rationals.v | |
| index f8ca716..0de4ed1 100644 | |
| --- a/implementations/intfrac_rationals.v | |
| +++ b/implementations/intfrac_rationals.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - interfaces.rationals interfaces.integers | |
| - abstract_algebra theory.rationals. | |
| + MathClasses.interfaces.rationals MathClasses.interfaces.integers | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.rationals. | |
| Require Export | |
| - field_of_fractions. | |
| + MathClasses.implementations.field_of_fractions. | |
| Section intfrac_rationals. | |
| Context `{Integers Z}. | |
| diff --git a/implementations/list.v b/implementations/list.v | |
| index b910182..2e13b3a 100644 | |
| --- a/implementations/list.v | |
| +++ b/implementations/list.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - List SetoidList abstract_algebra interfaces.monads theory.monads. | |
| + Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads. | |
| (* The below belongs in the stdlib *) | |
| Section equivlistA_misc. | |
| diff --git a/implementations/list_finite_set.v b/implementations/list_finite_set.v | |
| index c27b705..6f7ce24 100644 | |
| --- a/implementations/list_finite_set.v | |
| +++ b/implementations/list_finite_set.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - List SetoidList implementations.list | |
| - abstract_algebra interfaces.finite_sets interfaces.orders | |
| - theory.lattices orders.lattices. | |
| + Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders | |
| + MathClasses.theory.lattices MathClasses.orders.lattices. | |
| (* | |
| We define finite sets as unordered lists. This implementation is slow, | |
| diff --git a/implementations/modular_ring.v b/implementations/modular_ring.v | |
| index d9cc211..283b807 100644 | |
| --- a/implementations/modular_ring.v | |
| +++ b/implementations/modular_ring.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.integers | |
| - theory.integers theory.ring_ideals. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers | |
| + MathClasses.theory.integers MathClasses.theory.ring_ideals. | |
| Definition is_multiple `{Equiv Z} `{Mult Z} (b x : Z) := ∃ k, x = b * k. | |
| Notation Mod b := (Factor _ (is_multiple b)). | |
| diff --git a/implementations/mset_finite_set.v b/implementations/mset_finite_set.v | |
| index e193fe0..60a954a 100644 | |
| --- a/implementations/mset_finite_set.v | |
| +++ b/implementations/mset_finite_set.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - MSetInterface MSetFacts MSetProperties | |
| - implementations.list implementations.list_finite_set theory.finite_sets | |
| - interfaces.finite_sets interfaces.orders abstract_algebra. | |
| + Coq.MSets.MSetInterface Coq.MSets.MSetFacts Coq.MSets.MSetProperties | |
| + MathClasses.implementations.list MathClasses.implementations.list_finite_set MathClasses.theory.finite_sets | |
| + MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra. | |
| Module MSet_FSet (E : DecidableType) (Import set : WSetsOn E). | |
| diff --git a/implementations/natpair_integers.v b/implementations/natpair_integers.v | |
| index 430d111..5f09169 100644 | |
| --- a/implementations/natpair_integers.v | |
| +++ b/implementations/natpair_integers.v | |
| @@ -5,12 +5,12 @@ | |
| of these integers. *) | |
| Require | |
| - theory.naturals. | |
| + MathClasses.theory.naturals. | |
| Require Import | |
| - Ring abstract_algebra theory.categories | |
| - interfaces.naturals interfaces.integers jections. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.categories | |
| + MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.jections. | |
| Require Export | |
| - implementations.semiring_pairs. | |
| + MathClasses.implementations.semiring_pairs. | |
| Section contents. | |
| Context `{Naturals N}. | |
| diff --git a/implementations/ne_list.v b/implementations/ne_list.v | |
| index 4a8f13e..1b6f1ee 100644 | |
| --- a/implementations/ne_list.v | |
| +++ b/implementations/ne_list.v | |
| @@ -1,7 +1,7 @@ | |
| (** This module should be [Require]d but not [Import]ed (except for the notations submodule). *) | |
| Require Import | |
| - Unicode.Utf8 Coq.Lists.List Setoid Morphisms Permutation. | |
| + Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation. | |
| Instance: ∀ A, Proper (@Permutation A ==> eq) (@length A). | |
| Proof Permutation_length. | |
| diff --git a/implementations/nonneg_integers_naturals.v b/implementations/nonneg_integers_naturals.v | |
| index cb35abb..761fb61 100644 | |
| --- a/implementations/nonneg_integers_naturals.v | |
| +++ b/implementations/nonneg_integers_naturals.v | |
| @@ -1,10 +1,10 @@ | |
| Require | |
| - peano_naturals. | |
| + MathClasses.implementations.peano_naturals. | |
| Require Import | |
| - Ring abstract_algebra interfaces.integers interfaces.naturals interfaces.orders | |
| - interfaces.additional_operations int_abs. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.orders | |
| + MathClasses.interfaces.additional_operations MathClasses.theory.int_abs. | |
| Require Export | |
| - implementations.nonneg_semiring_elements. | |
| + MathClasses.implementations.nonneg_semiring_elements. | |
| Section nonneg_integers_naturals. | |
| Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}. | |
| diff --git a/implementations/nonneg_semiring_elements.v b/implementations/nonneg_semiring_elements.v | |
| index dfd4b60..7fd6430 100644 | |
| --- a/implementations/nonneg_semiring_elements.v | |
| +++ b/implementations/nonneg_semiring_elements.v | |
| @@ -1,8 +1,8 @@ | |
| Require | |
| - theory.rings. | |
| + MathClasses.theory.rings. | |
| Require Import | |
| - Ring | |
| - abstract_algebra interfaces.orders orders.semirings. | |
| + Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.semirings. | |
| Local Existing Instance pseudo_srorder_semiring. | |
| diff --git a/implementations/nonzero_field_elements.v b/implementations/nonzero_field_elements.v | |
| index 44f94ac..bb7d8c5 100644 | |
| --- a/implementations/nonzero_field_elements.v | |
| +++ b/implementations/nonzero_field_elements.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Ring abstract_algebra theory.fields. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.fields. | |
| (* The non zero elements of a field form a CommutativeMonoid. *) | |
| Section contents. | |
| diff --git a/implementations/option.v b/implementations/option.v | |
| index 77b1956..4c819ca 100644 | |
| --- a/implementations/option.v | |
| +++ b/implementations/option.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.monads jections theory.monads. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads. | |
| Inductive option_equiv A `{Equiv A} : Equiv (option A) := | |
| | option_equiv_Some : Proper ((=) ==> (=)) Some | |
| diff --git a/implementations/peano_naturals.v b/implementations/peano_naturals.v | |
| index 2e46c1f..f184d51 100644 | |
| --- a/implementations/peano_naturals.v | |
| +++ b/implementations/peano_naturals.v | |
| @@ -1,9 +1,9 @@ | |
| Require | |
| - ua_homomorphisms. | |
| + MathClasses.theory.ua_homomorphisms. | |
| Require Import | |
| - Morphisms Ring Arith_base | |
| - abstract_algebra interfaces.naturals theory.categories | |
| - interfaces.additional_operations interfaces.orders orders.semirings. | |
| + Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings. | |
| Instance nat_equiv: Equiv nat := eq. | |
| Instance nat_plus: Plus nat := Peano.plus. | |
| diff --git a/implementations/polynomials.v b/implementations/polynomials.v | |
| index a812f06..5e163c9 100644 | |
| --- a/implementations/polynomials.v | |
| +++ b/implementations/polynomials.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - List | |
| - abstract_algebra. | |
| + Coq.Lists.List | |
| + MathClasses.interfaces.abstract_algebra. | |
| Section contents. | |
| Context R `{Ring R}. | |
| diff --git a/implementations/positive_semiring_elements.v b/implementations/positive_semiring_elements.v | |
| index 58be82a..9f43a18 100644 | |
| --- a/implementations/positive_semiring_elements.v | |
| +++ b/implementations/positive_semiring_elements.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring | |
| - abstract_algebra additional_operations | |
| - interfaces.orders interfaces.integers | |
| - orders.semirings theory.shiftl theory.int_pow. | |
| + Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations | |
| + MathClasses.interfaces.orders MathClasses.interfaces.integers | |
| + MathClasses.orders.semirings MathClasses.theory.shiftl MathClasses.theory.int_pow. | |
| Local Existing Instance pseudo_srorder_semiring. | |
| diff --git a/implementations/semiring_pairs.v b/implementations/semiring_pairs.v | |
| index 22ed364..43e7907 100644 | |
| --- a/implementations/semiring_pairs.v | |
| +++ b/implementations/semiring_pairs.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.orders orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings. | |
| Inductive SRpair (SR : Type) := C { pos : SR ; neg : SR }. | |
| Arguments C {SR} _ _. | |
| diff --git a/implementations/stdlib_binary_integers.v b/implementations/stdlib_binary_integers.v | |
| index 6fc290a..81f83d2 100644 | |
| --- a/implementations/stdlib_binary_integers.v | |
| +++ b/implementations/stdlib_binary_integers.v | |
| @@ -1,11 +1,11 @@ | |
| Require | |
| - interfaces.naturals theory.naturals peano_naturals theory.integers. | |
| + MathClasses.interfaces.naturals MathClasses.theory.naturals MathClasses.implementations.peano_naturals MathClasses.theory.integers. | |
| Require Import | |
| - BinInt Ring Arith NArith ZArith ZBinary | |
| - abstract_algebra interfaces.integers | |
| - natpair_integers stdlib_binary_naturals | |
| - interfaces.additional_operations interfaces.orders | |
| - nonneg_integers_naturals. | |
| + Coq.ZArith.BinInt Coq.setoid_ring.Ring Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Numbers.Integer.Binary.ZBinary | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers | |
| + MathClasses.implementations.natpair_integers MathClasses.implementations.stdlib_binary_naturals | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders | |
| + MathClasses.implementations.nonneg_integers_naturals. | |
| (* canonical names: *) | |
| Instance Z_equiv: Equiv Z := eq. | |
| diff --git a/implementations/stdlib_binary_naturals.v b/implementations/stdlib_binary_naturals.v | |
| index 7ef5c92..2a44de3 100644 | |
| --- a/implementations/stdlib_binary_naturals.v | |
| +++ b/implementations/stdlib_binary_naturals.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - NArith peano_naturals theory.naturals | |
| - abstract_algebra interfaces.naturals interfaces.orders | |
| - interfaces.additional_operations. | |
| + Coq.NArith.NArith MathClasses.implementations.peano_naturals MathClasses.theory.naturals | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders | |
| + MathClasses.interfaces.additional_operations. | |
| (* canonical names for relations/operations/constants: *) | |
| Instance N_equiv : Equiv N := eq. | |
| diff --git a/implementations/stdlib_rationals.v b/implementations/stdlib_rationals.v | |
| index c049829..2b4c0a8 100644 | |
| --- a/implementations/stdlib_rationals.v | |
| +++ b/implementations/stdlib_rationals.v | |
| @@ -1,10 +1,10 @@ | |
| Require | |
| - stdlib_binary_integers Field QArith.Qfield theory.rationals. | |
| + MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals. | |
| Require Import | |
| - Ring QArith_base Qabs Qpower | |
| - abstract_algebra interfaces.rationals | |
| - interfaces.orders interfaces.additional_operations | |
| - field_of_fractions orders.integers. | |
| + Coq.setoid_ring.Ring Coq.QArith.QArith_base Coq.QArith.Qabs Coq.QArith.Qpower | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals | |
| + MathClasses.interfaces.orders MathClasses.interfaces.additional_operations | |
| + MathClasses.implementations.field_of_fractions MathClasses.orders.integers. | |
| (* canonical names for relations/operations/constants: *) | |
| Instance Q_eq: Equiv Q := Qeq. | |
| diff --git a/interfaces/abstract_algebra.v b/interfaces/abstract_algebra.v | |
| index fce57d9..c297cd5 100644 | |
| --- a/interfaces/abstract_algebra.v | |
| +++ b/interfaces/abstract_algebra.v | |
| @@ -1,5 +1,5 @@ | |
| Require Export | |
| - canonical_names util decision propholds workarounds setoid_tactics. | |
| + MathClasses.interfaces.canonical_names MathClasses.misc.util MathClasses.misc.decision MathClasses.misc.propholds MathClasses.misc.workarounds MathClasses.misc.setoid_tactics. | |
| (* | |
| For various structures we omit declaration of substructures. For example, if we | |
| diff --git a/interfaces/additional_operations.v b/interfaces/additional_operations.v | |
| index 225bd2d..9a47bd3 100644 | |
| --- a/interfaces/additional_operations.v | |
| +++ b/interfaces/additional_operations.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Morphisms abstract_algebra. | |
| + Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra. | |
| Class Pow A B := pow : A → B → A. | |
| Infix "^" := pow : mc_scope. | |
| diff --git a/interfaces/canonical_names.v b/interfaces/canonical_names.v | |
| index 8946626..97f8097 100644 | |
| --- a/interfaces/canonical_names.v | |
| +++ b/interfaces/canonical_names.v | |
| @@ -2,8 +2,8 @@ Global Generalizable All Variables. | |
| Global Set Automatic Introduction. | |
| Global Set Automatic Coercions Import. | |
| -Require Import Streams. | |
| -Require Export Morphisms Setoid Program Unicode.Utf8 Utf8_core stdlib_hints. | |
| +Require Import Coq.Lists.Streams. | |
| +Require Export Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Program.Program Coq.Unicode.Utf8 Coq.Unicode.Utf8_core MathClasses.misc.stdlib_hints. | |
| Definition id {A : Type} (a : A) := a. | |
| diff --git a/interfaces/finite_sets.v b/interfaces/finite_sets.v | |
| index 4df238c..2cda57e 100644 | |
| --- a/interfaces/finite_sets.v | |
| +++ b/interfaces/finite_sets.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders. | |
| (* | |
| We define finite sets as the initial join semi lattice over a decidable type. | |
| diff --git a/interfaces/functors.v b/interfaces/functors.v | |
| index 1039b4c..4d490b5 100644 | |
| --- a/interfaces/functors.v | |
| +++ b/interfaces/functors.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - abstract_algebra. | |
| + MathClasses.interfaces.abstract_algebra. | |
| Require | |
| - theory.setoids. | |
| + MathClasses.theory.setoids. | |
| Section functor_class. | |
| Context `{Category C} `{Category D} (M: C → D). | |
| diff --git a/interfaces/integers.v b/interfaces/integers.v | |
| index 4660380..87ff778 100644 | |
| --- a/interfaces/integers.v | |
| +++ b/interfaces/integers.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - abstract_algebra interfaces.naturals theory.categories | |
| - categories.varieties. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories | |
| + MathClasses.categories.varieties. | |
| Require | |
| - varieties.rings. | |
| + MathClasses.varieties.rings. | |
| Section initial_maps. | |
| Variable A : Type. | |
| diff --git a/interfaces/monads.v b/interfaces/monads.v | |
| index ec337ad..f6b637a 100644 | |
| --- a/interfaces/monads.v | |
| +++ b/interfaces/monads.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - abstract_algebra canonical_names. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names. | |
| Require Export | |
| - interfaces.functors. | |
| + MathClasses.interfaces.functors. | |
| Section ops. | |
| Context (M : Type → Type). | |
| diff --git a/interfaces/naturals.v b/interfaces/naturals.v | |
| index 14d22c6..f0d88dc 100644 | |
| --- a/interfaces/naturals.v | |
| +++ b/interfaces/naturals.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - abstract_algebra theory.categories | |
| - varieties.semirings categories.varieties. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.categories | |
| + MathClasses.varieties.semirings MathClasses.categories.varieties. | |
| Module bad. | |
| Class Naturals (A: semirings.Object) `{!InitialArrow A}: Prop := | |
| diff --git a/interfaces/orders.v b/interfaces/orders.v | |
| index b587409..4761777 100644 | |
| --- a/interfaces/orders.v | |
| +++ b/interfaces/orders.v | |
| @@ -1,4 +1,4 @@ | |
| -Require Import abstract_algebra. | |
| +Require Import MathClasses.interfaces.abstract_algebra. | |
| (* | |
| In this file we describe interfaces for ordered structures. Since we are in a | |
| diff --git a/interfaces/rationals.v b/interfaces/rationals.v | |
| index f767507..3298895 100644 | |
| --- a/interfaces/rationals.v | |
| +++ b/interfaces/rationals.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.integers field_of_fractions theory.integers. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.implementations.field_of_fractions MathClasses.theory.integers. | |
| Section rationals_to_frac. | |
| Context (A : Type). | |
| diff --git a/interfaces/sequences.v b/interfaces/sequences.v | |
| index a2fbed5..d764ebc 100644 | |
| --- a/interfaces/sequences.v | |
| +++ b/interfaces/sequences.v | |
| @@ -1,10 +1,10 @@ | |
| Require Import | |
| - List abstract_algebra theory.categories forget_algebra forget_variety | |
| - theory.rings interfaces.universal_algebra interfaces.functors | |
| - categories.setoids categories.varieties. | |
| + Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.theory.forget_algebra MathClasses.theory.forget_variety | |
| + MathClasses.theory.rings MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors | |
| + MathClasses.categories.setoids MathClasses.categories.varieties. | |
| Require | |
| - categories.product varieties.monoids categories.algebras | |
| - categories.categories theory.setoids. | |
| + MathClasses.categories.product MathClasses.varieties.monoids MathClasses.categories.algebras | |
| + MathClasses.categories.categories MathClasses.theory.setoids. | |
| Module ua := universal_algebra. | |
| diff --git a/interfaces/ua_basic.v b/interfaces/ua_basic.v | |
| index 1e2189b..8c322f3 100644 | |
| --- a/interfaces/ua_basic.v | |
| +++ b/interfaces/ua_basic.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - ne_list. | |
| + MathClasses.implementations.ne_list. | |
| Require Import | |
| - List abstract_algebra. | |
| + Coq.Lists.List MathClasses.interfaces.abstract_algebra. | |
| Local Notation ne_list := ne_list.L. | |
| diff --git a/interfaces/universal_algebra.v b/interfaces/universal_algebra.v | |
| index bd5c326..b3c11e2 100644 | |
| --- a/interfaces/universal_algebra.v | |
| +++ b/interfaces/universal_algebra.v | |
| @@ -1,10 +1,10 @@ | |
| Require | |
| - theory.setoids ne_list. | |
| + MathClasses.theory.setoids MathClasses.implementations.ne_list. | |
| Require Import | |
| - List | |
| - abstract_algebra util jections. | |
| + Coq.Lists.List | |
| + MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections. | |
| Require Export | |
| - ua_basic. | |
| + MathClasses.interfaces.ua_basic. | |
| Section for_signature. | |
| Variable σ: Signature. | |
| diff --git a/interfaces/vectorspace.v b/interfaces/vectorspace.v | |
| index c630ca8..ed5abf4 100644 | |
| --- a/interfaces/vectorspace.v | |
| +++ b/interfaces/vectorspace.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders. | |
| (** Scalar multiplication function class *) | |
| Class ScalarMult K V := scalar_mult: K → V → V. | |
| diff --git a/misc/JMrelation.v b/misc/JMrelation.v | |
| index 05e5af3..cdbf3b1 100644 | |
| --- a/misc/JMrelation.v | |
| +++ b/misc/JMrelation.v | |
| @@ -1,6 +1,6 @@ | |
| (* JMeq without the [eq] hard-wiring. Meant for use with [Require] only, not [Import]. *) | |
| -Require Import Relation_Definitions Setoid. | |
| -Require Export Unicode.Utf8 Utf8_core. | |
| +Require Import Coq.Relations.Relation_Definitions Coq.Setoids.Setoid. | |
| +Require Export Coq.Unicode.Utf8 Coq.Unicode.Utf8_core. | |
| Inductive R {A: Type} (r: relation A) (x: A): forall B: Type, relation B → B → Prop := relate y: r x y → R r x A r y. | |
| @@ -14,7 +14,7 @@ Lemma transitive A B C (Ra: relation A) (Rb: relation B) (Rc: relation C) (a:A) | |
| R Ra a _ Rb b → R Rb b _ Rc c → R Ra a _ Rc c. | |
| Proof. destruct 1. destruct 1. apply relate. transitivity y; assumption. Qed. | |
| -Require Import Eqdep. | |
| +Require Import Coq.Logic.Eqdep. | |
| Lemma unJM A (r: relation A) (x y:A) r' (E: R r x A r' y): r x y. | |
| Proof. | |
| diff --git a/misc/benchmarks_nobuild.v b/misc/benchmarks_nobuild.v | |
| index 788f682..eb53eba 100644 | |
| --- a/misc/benchmarks_nobuild.v | |
| +++ b/misc/benchmarks_nobuild.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - abstract_algebra interfaces.integers interfaces.additional_operations | |
| - implementations.dyadics fast_integers. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations | |
| + MathClasses.implementations.dyadics MathClasses.implementations.fast_integers. | |
| Section wolfram_sqrt. | |
| Context `{Integers Z} `{!RingOrder oZ} `{!TotalOrder oZ} | |
| diff --git a/misc/decision.v b/misc/decision.v | |
| index cf7ff58..e135712 100644 | |
| --- a/misc/decision.v | |
| +++ b/misc/decision.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - canonical_names util. | |
| + MathClasses.interfaces.canonical_names MathClasses.misc.util. | |
| Class Decision P := decide: sumbool P (¬P). | |
| Arguments decide _ {Decision}. | |
| diff --git a/misc/propholds.v b/misc/propholds.v | |
| index dc8fb7a..c215863 100644 | |
| --- a/misc/propholds.v | |
| +++ b/misc/propholds.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - canonical_names. | |
| + MathClasses.interfaces.canonical_names. | |
| (* | |
| The following class is nice to parametrize instances by additional properties, for example: | |
| diff --git a/misc/setoid_tactics.v b/misc/setoid_tactics.v | |
| index 96c6dc9..e9a309a 100644 | |
| --- a/misc/setoid_tactics.v | |
| +++ b/misc/setoid_tactics.v | |
| @@ -1,4 +1,4 @@ | |
| -Require Import Setoid canonical_names. | |
| +Require Import Coq.Setoids.Setoid MathClasses.interfaces.canonical_names. | |
| (* | |
| When math-classes is used as part of another development setoid_replace | |
| diff --git a/misc/stdlib_hints.v b/misc/stdlib_hints.v | |
| index 0f28950..3358804 100644 | |
| --- a/misc/stdlib_hints.v | |
| +++ b/misc/stdlib_hints.v | |
| @@ -1,5 +1,5 @@ | |
| -Require Import Setoid Morphisms RelationClasses. | |
| -Require Import Utf8. | |
| +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses. | |
| +Require Import Coq.Unicode.Utf8. | |
| Hint Unfold Proper respectful. | |
| diff --git a/misc/util.v b/misc/util.v | |
| index 9d99a8e..d67d777 100644 | |
| --- a/misc/util.v | |
| +++ b/misc/util.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Program Morphisms Setoid canonical_names. | |
| + Coq.Program.Program Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names. | |
| Section pointwise_dependent_relation. | |
| Context A (B: A → Type) (R: ∀ a, relation (B a)). | |
| diff --git a/misc/workarounds.v b/misc/workarounds.v | |
| index fce33c5..2910c56 100644 | |
| --- a/misc/workarounds.v | |
| +++ b/misc/workarounds.v | |
| @@ -1,5 +1,5 @@ | |
| -Require Import canonical_names. | |
| -Require Import Equivalence Morphisms RelationClasses. | |
| +Require Import MathClasses.interfaces.canonical_names. | |
| +Require Import Coq.Classes.Equivalence Coq.Classes.Morphisms Coq.Classes.RelationClasses. | |
| (* Remove some duplicate / obsolete instances *) | |
| Remove Hints Equivalence_Reflexive | |
| diff --git a/orders/dec_fields.v b/orders/dec_fields.v | |
| index 2e31aa1..79a4e5c 100644 | |
| --- a/orders/dec_fields.v | |
| +++ b/orders/dec_fields.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Relation_Definitions Ring | |
| - abstract_algebra interfaces.orders theory.rings theory.dec_fields. | |
| + Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields. | |
| Require Export | |
| - orders.rings. | |
| + MathClasses.orders.rings. | |
| Section contents. | |
| Context `{DecField F} `{Apart F} `{!TrivialApart F} `{!FullPseudoSemiRingOrder Fle Flt} `{∀ x y : F, Decision (x = y)}. | |
| diff --git a/orders/integers.v b/orders/integers.v | |
| index 236a542..d53c777 100644 | |
| --- a/orders/integers.v | |
| +++ b/orders/integers.v | |
| @@ -1,11 +1,11 @@ | |
| Require | |
| - theory.integers theory.int_abs. | |
| + MathClasses.theory.integers MathClasses.theory.int_abs. | |
| Require Import | |
| - Ring abstract_algebra interfaces.integers interfaces.naturals | |
| - interfaces.additional_operations interfaces.orders | |
| - natpair_integers orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders | |
| + MathClasses.implementations.natpair_integers MathClasses.orders.rings. | |
| Require Export | |
| - orders.nat_int. | |
| + MathClasses.orders.nat_int. | |
| Section integers. | |
| Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}. | |
| diff --git a/orders/lattices.v b/orders/lattices.v | |
| index 50c4261..8ac47e6 100644 | |
| --- a/orders/lattices.v | |
| +++ b/orders/lattices.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders orders.maps theory.lattices. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices. | |
| (* | |
| We prove that the algebraic definition of a lattice corresponds to the | |
| diff --git a/orders/maps.v b/orders/maps.v | |
| index ebbd170..d7bee98 100644 | |
| --- a/orders/maps.v | |
| +++ b/orders/maps.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders orders.orders theory.setoids theory.strong_setoids. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids. | |
| Local Existing Instance order_morphism_po_a. | |
| Local Existing Instance order_morphism_po_b. | |
| diff --git a/orders/minmax.v b/orders/minmax.v | |
| index f9f1976..01df5c1 100644 | |
| --- a/orders/minmax.v | |
| +++ b/orders/minmax.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders orders.orders | |
| - orders.lattices theory.setoids. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders | |
| + MathClasses.orders.lattices MathClasses.theory.setoids. | |
| Section contents. | |
| Context `{TotalOrder A} `{∀ x y: A, Decision (x ≤ y)}. | |
| diff --git a/orders/nat_int.v b/orders/nat_int.v | |
| index e2c45ca..b6e75c6 100644 | |
| --- a/orders/nat_int.v | |
| +++ b/orders/nat_int.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.naturals interfaces.orders | |
| - theory.naturals theory.rings peano_naturals. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders | |
| + MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals. | |
| Require Export | |
| - orders.semirings. | |
| + MathClasses.orders.semirings. | |
| (* | |
| We axiomatize the order on the naturals and the integers as a non trivial | |
| diff --git a/orders/naturals.v b/orders/naturals.v | |
| index 67063f4..ff083ef 100644 | |
| --- a/orders/naturals.v | |
| +++ b/orders/naturals.v | |
| @@ -1,9 +1,9 @@ | |
| Require | |
| - theory.naturals. | |
| + MathClasses.theory.naturals. | |
| Require Import | |
| - Ring abstract_algebra interfaces.naturals interfaces.orders orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings. | |
| Require Export | |
| - orders.nat_int. | |
| + MathClasses.orders.nat_int. | |
| Section naturals_order. | |
| Context `{Naturals N} `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder Nle Nlt}. | |
| diff --git a/orders/orders.v b/orders/orders.v | |
| index 21315bf..67a7701 100644 | |
| --- a/orders/orders.v | |
| +++ b/orders/orders.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.orders strong_setoids. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids. | |
| Lemma le_flip `{Le A} `{!TotalRelation (≤)} x y : ¬y ≤ x → x ≤ y. | |
| Proof. firstorder. Qed. | |
| diff --git a/orders/rationals.v b/orders/rationals.v | |
| index a54be86..b28f16d 100644 | |
| --- a/orders/rationals.v | |
| +++ b/orders/rationals.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring Field abstract_algebra interfaces.orders | |
| - interfaces.naturals interfaces.rationals interfaces.integers | |
| - natpair_integers theory.rationals theory.dec_fields theory.rings | |
| - orders.integers orders.dec_fields. | |
| + Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders | |
| + MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.integers | |
| + MathClasses.implementations.natpair_integers MathClasses.theory.rationals MathClasses.theory.dec_fields MathClasses.theory.rings | |
| + MathClasses.orders.integers MathClasses.orders.dec_fields. | |
| Section rationals_and_integers. | |
| Context `{Rationals Q} `{!SemiRingOrder Qle} | |
| diff --git a/orders/rings.v b/orders/rings.v | |
| index 5705976..f0f5cb9 100644 | |
| --- a/orders/rings.v | |
| +++ b/orders/rings.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.orders theory.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings. | |
| Require Export | |
| - orders.semirings. | |
| + MathClasses.orders.semirings. | |
| Section from_ring_order. | |
| Context `{Ring R} `{!PartialOrder Rle} | |
| diff --git a/orders/semirings.v b/orders/semirings.v | |
| index e7d3640..169d8d2 100644 | |
| --- a/orders/semirings.v | |
| +++ b/orders/semirings.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.orders theory.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings. | |
| Require Export | |
| - orders.orders orders.maps. | |
| + MathClasses.orders.orders MathClasses.orders.maps. | |
| Local Existing Instance srorder_semiring. | |
| Local Existing Instance strict_srorder_semiring. | |
| diff --git a/quote/classquote.v b/quote/classquote.v | |
| index 0fd83af..d89e684 100644 | |
| --- a/quote/classquote.v | |
| +++ b/quote/classquote.v | |
| @@ -1,4 +1,4 @@ | |
| -Require Import Morphisms Program Unicode.Utf8. | |
| +Require Import Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8. | |
| (* First, two ways to do quoting in the naive scenario without | |
| holes/variables in the expression: *) | |
| diff --git a/theory/abs.v b/theory/abs.v | |
| index b7aa413..c5f92bb 100644 | |
| --- a/theory/abs.v | |
| +++ b/theory/abs.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Ring abstract_algebra interfaces.orders orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings. | |
| Section contents. | |
| Context `{Ring R} `{Apart R} `{!TrivialApart R} `{!FullPseudoSemiRingOrder Rle Rlt} `{∀ x y, Decision (x = y)} `{a : !Abs R}. | |
| diff --git a/theory/adjunctions.v b/theory/adjunctions.v | |
| index 42f1a6f..0f360ba 100644 | |
| --- a/theory/adjunctions.v | |
| +++ b/theory/adjunctions.v | |
| @@ -1,8 +1,8 @@ | |
| (** We prove the equivalence of the two definitions of adjunction. *) | |
| Require Import | |
| - abstract_algebra theory.setoids interfaces.functors theory.categories | |
| - workaround_tactics theory.jections. | |
| -Require dual. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories | |
| + MathClasses.misc.workaround_tactics MathClasses.theory.jections. | |
| +Require MathClasses.categories.dual. | |
| Local Hint Unfold id compose: typeclass_instances. (* todo: move *) | |
| Local Existing Instance injective_mor. | |
| diff --git a/theory/categories.v b/theory/categories.v | |
| index ea921cb..89ea54a 100644 | |
| --- a/theory/categories.v | |
| +++ b/theory/categories.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra theory.setoids interfaces.functors theory.jections. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections. | |
| Notation "x ⇛ y" := (∀ a, x a ⟶ y a) (at level 90, right associativity) : mc_scope. | |
| (* Transformations (polymorphic arrows). Couldn't find an "arrow with dot over it" unicode character. *) | |
| diff --git a/theory/cut_minus.v b/theory/cut_minus.v | |
| index af83757..8ff0f70 100644 | |
| --- a/theory/cut_minus.v | |
| +++ b/theory/cut_minus.v | |
| @@ -1,8 +1,8 @@ | |
| Require | |
| - orders.semirings. | |
| + MathClasses.orders.semirings. | |
| Require Import | |
| - Ring abstract_algebra interfaces.additional_operations | |
| - interfaces.orders orders.minmax. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations | |
| + MathClasses.interfaces.orders MathClasses.orders.minmax. | |
| (* * Properties of Cut off Minus *) | |
| Section cut_minus_properties. | |
| diff --git a/theory/dec_fields.v b/theory/dec_fields.v | |
| index fc59101..5ada5df 100644 | |
| --- a/theory/dec_fields.v | |
| +++ b/theory/dec_fields.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Field Ring | |
| - abstract_algebra theory.fields theory.strong_setoids. | |
| + Coq.setoid_ring.Field Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.fields MathClasses.theory.strong_setoids. | |
| Require Export | |
| - theory.rings. | |
| + MathClasses.theory.rings. | |
| Section contents. | |
| Context `{DecField F} `{∀ x y: F, Decision (x = y)}. | |
| diff --git a/theory/fields.v b/theory/fields.v | |
| index e9072c5..3530665 100644 | |
| --- a/theory/fields.v | |
| +++ b/theory/fields.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - Ring abstract_algebra strong_setoids. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids. | |
| Require Export | |
| - theory.rings. | |
| + MathClasses.theory.rings. | |
| Section field_properties. | |
| Context `{Field F}. | |
| diff --git a/theory/finite_sets.v b/theory/finite_sets.v | |
| index c33a690..a7bb915 100644 | |
| --- a/theory/finite_sets.v | |
| +++ b/theory/finite_sets.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - theory.lattices varieties.monoids implementations.bool | |
| - implementations.list_finite_set orders.lattices | |
| - abstract_algebra interfaces.finite_sets interfaces.orders. | |
| + MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool | |
| + MathClasses.implementations.list_finite_set MathClasses.orders.lattices | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders. | |
| Definition fset_car_setoid A `{FSet A} : Setoid A := setoidmor_a singleton. | |
| diff --git a/theory/forget_algebra.v b/theory/forget_algebra.v | |
| index ef12dd1..87a64f9 100644 | |
| --- a/theory/forget_algebra.v | |
| +++ b/theory/forget_algebra.v | |
| @@ -2,9 +2,9 @@ | |
| This functor should nicely compose with the one forgetting variety laws. *) | |
| Require Import | |
| - abstract_algebra universal_algebra interfaces.functors | |
| - ua_homomorphisms theory.categories | |
| - categories.setoids categories.product categories.algebras. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors | |
| + MathClasses.theory.ua_homomorphisms MathClasses.theory.categories | |
| + MathClasses.categories.setoids MathClasses.categories.product MathClasses.categories.algebras. | |
| Section contents. | |
| Variable sign: Signature. | |
| diff --git a/theory/forget_variety.v b/theory/forget_variety.v | |
| index c48cdb6..638b86a 100644 | |
| --- a/theory/forget_variety.v | |
| +++ b/theory/forget_variety.v | |
| @@ -1,8 +1,8 @@ | |
| (* "Forgetting" a variety's laws (but keeping the algebraic operations) is a trivial functor. *) | |
| Require Import | |
| - canonical_names universal_algebra interfaces.functors | |
| - theory.categories categories.varieties categories.algebras. | |
| + MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors | |
| + MathClasses.theory.categories MathClasses.categories.varieties MathClasses.categories.algebras. | |
| Section contents. | |
| diff --git a/theory/functors.v b/theory/functors.v | |
| index 86839b2..f762525 100644 | |
| --- a/theory/functors.v | |
| +++ b/theory/functors.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - canonical_names abstract_algebra | |
| - interfaces.functors. | |
| + MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra | |
| + MathClasses.interfaces.functors. | |
| Require | |
| - categories.setoids. | |
| + MathClasses.categories.setoids. | |
| Section setoid_functor_as_posh_functor. | |
| Context `{Pfunctor : @SFunctor F map_eq map}. | |
| diff --git a/theory/groups.v b/theory/groups.v | |
| index 091424d..725d5a0 100644 | |
| --- a/theory/groups.v | |
| +++ b/theory/groups.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - theory.setoids. | |
| + MathClasses.theory.setoids. | |
| Require Import | |
| - Morphisms abstract_algebra. | |
| + Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra. | |
| Section semigroup_props. | |
| Context `{SemiGroup G}. | |
| diff --git a/theory/hom_functor.v b/theory/hom_functor.v | |
| index 02ab018..33fc110 100644 | |
| --- a/theory/hom_functor.v | |
| +++ b/theory/hom_functor.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - abstract_algebra theory.setoids interfaces.functors theory.categories. | |
| -Require categories.setoids. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.categories. | |
| +Require MathClasses.categories.setoids. | |
| Section contents. | |
| Context `{Category C} (x: C). | |
| diff --git a/theory/int_abs.v b/theory/int_abs.v | |
| index d1fa00f..ea6c595 100644 | |
| --- a/theory/int_abs.v | |
| +++ b/theory/int_abs.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - Ring interfaces.naturals abstract_algebra interfaces.orders | |
| - orders.nat_int theory.integers theory.rings orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders | |
| + MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings. | |
| Section contents. | |
| Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}. | |
| diff --git a/theory/int_pow.v b/theory/int_pow.v | |
| index f5c7b82..a045d53 100644 | |
| --- a/theory/int_pow.v | |
| +++ b/theory/int_pow.v | |
| @@ -1,10 +1,10 @@ | |
| Require | |
| - theory.naturals orders.semirings orders.integers orders.dec_fields. | |
| + MathClasses.theory.naturals MathClasses.orders.semirings MathClasses.orders.integers MathClasses.orders.dec_fields. | |
| Require Import | |
| - Ring Field | |
| - abstract_algebra interfaces.naturals interfaces.integers | |
| - interfaces.additional_operations interfaces.orders | |
| - theory.nat_pow theory.int_abs theory.dec_fields. | |
| + Coq.setoid_ring.Ring Coq.setoid_ring.Field | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders | |
| + MathClasses.theory.nat_pow MathClasses.theory.int_abs MathClasses.theory.dec_fields. | |
| (* * Properties of Int Pow *) | |
| Section int_pow_properties. | |
| diff --git a/theory/int_to_nat.v b/theory/int_to_nat.v | |
| index 50f538f..e4251f9 100644 | |
| --- a/theory/int_to_nat.v | |
| +++ b/theory/int_to_nat.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - Ring interfaces.naturals abstract_algebra interfaces.orders | |
| - orders.nat_int theory.integers theory.rings orders.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders | |
| + MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings. | |
| Section contents. | |
| Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}. | |
| diff --git a/theory/integers.v b/theory/integers.v | |
| index a4d216e..e0d0bee 100644 | |
| --- a/theory/integers.v | |
| +++ b/theory/integers.v | |
| @@ -1,10 +1,10 @@ | |
| (* General results about arbitrary integer implementations. *) | |
| Require | |
| - theory.nat_distance. | |
| + MathClasses.theory.nat_distance. | |
| Require Import | |
| - Ring interfaces.naturals abstract_algebra natpair_integers. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers. | |
| Require Export | |
| - interfaces.integers. | |
| + MathClasses.interfaces.integers. | |
| (* Any two integer implementations are trivially isomorphic because of their initiality, | |
| but it's nice to have this stated in terms of integers_to_ring being self-inverse: *) | |
| diff --git a/theory/jections.v b/theory/jections.v | |
| index 4f6f045..69a1b3c 100644 | |
| --- a/theory/jections.v | |
| +++ b/theory/jections.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - theory.setoids abstract_algebra. | |
| + MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra. | |
| Local Existing Instance injective_mor. | |
| Local Existing Instance surjective_mor. | |
| diff --git a/theory/lattices.v b/theory/lattices.v | |
| index 005ba76..109ace8 100644 | |
| --- a/theory/lattices.v | |
| +++ b/theory/lattices.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - abstract_algebra theory.groups. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.groups. | |
| Require | |
| - varieties.semigroups varieties.monoids. | |
| + MathClasses.varieties.semigroups MathClasses.varieties.monoids. | |
| Instance bounded_sl_is_sl `{BoundedSemiLattice L} : SemiLattice L. | |
| Proof. repeat (split; try apply _). Qed. | |
| diff --git a/theory/monads.v b/theory/monads.v | |
| index c221440..677ee1c 100644 | |
| --- a/theory/monads.v | |
| +++ b/theory/monads.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra interfaces.monads theory.functors. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors. | |
| Instance default_mon_join `{MonadBind M} : MonadJoin M | 20 := λ _, bind id. | |
| Instance default_mon_map `{MonadReturn M} `{MonadBind M} : SFmap M | 20 := λ _ _ f, bind (ret ∘ f). | |
| diff --git a/theory/monoid_normalization.v b/theory/monoid_normalization.v | |
| index a5881cc..06b42db 100644 | |
| --- a/theory/monoid_normalization.v | |
| +++ b/theory/monoid_normalization.v | |
| @@ -1,6 +1,6 @@ | |
| -Require Import Omega. | |
| -Require Import abstract_algebra ua_packed. | |
| -Require universal_algebra varieties.monoids. | |
| +Require Import Coq.omega.Omega. | |
| +Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.ua_packed. | |
| +Require MathClasses.interfaces.universal_algebra MathClasses.varieties.monoids. | |
| Notation msig := varieties.monoids.sig. | |
| Notation Op := (universal_algebra.Op msig False). | |
| diff --git a/theory/nat_distance.v b/theory/nat_distance.v | |
| index 71b4e02..120f16c 100644 | |
| --- a/theory/nat_distance.v | |
| +++ b/theory/nat_distance.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - orders.naturals peano_naturals. | |
| + MathClasses.orders.naturals MathClasses.implementations.peano_naturals. | |
| Require Import | |
| - Ring abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations. | |
| Section contents. | |
| Context `{Naturals N}. | |
| diff --git a/theory/nat_pow.v b/theory/nat_pow.v | |
| index 1f75b27..ff4deac 100644 | |
| --- a/theory/nat_pow.v | |
| +++ b/theory/nat_pow.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - theory.naturals. | |
| + MathClasses.theory.naturals. | |
| Require Import | |
| - Ring abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations. | |
| (* * Properties of Nat Pow *) | |
| Section nat_pow_properties. | |
| diff --git a/theory/naturals.v b/theory/naturals.v | |
| index edc3d56..0358ab5 100644 | |
| --- a/theory/naturals.v | |
| +++ b/theory/naturals.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring abstract_algebra peano_naturals theory.rings | |
| - categories.varieties theory.ua_transference. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings | |
| + MathClasses.categories.varieties MathClasses.theory.ua_transference. | |
| Require Export | |
| - interfaces.naturals. | |
| + MathClasses.interfaces.naturals. | |
| Lemma to_semiring_involutive N `{Naturals N} N2 `{Naturals N2} x : | |
| naturals_to_semiring N2 N (naturals_to_semiring N N2 x) = x. | |
| diff --git a/theory/products.v b/theory/products.v | |
| index f14dd14..16869c8 100644 | |
| --- a/theory/products.v | |
| +++ b/theory/products.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra. | |
| + MathClasses.interfaces.abstract_algebra. | |
| Definition prod_equiv `{Equiv A} `{Equiv B} : Equiv (A * B) := λ p q, fst p = fst q ∧ snd p = snd q. | |
| (* Avoid eager application *) | |
| diff --git a/theory/quote_monoid.v b/theory/quote_monoid.v | |
| index c813718..8bae0eb 100644 | |
| --- a/theory/quote_monoid.v | |
| +++ b/theory/quote_monoid.v | |
| @@ -1,10 +1,10 @@ | |
| -Require Import abstract_algebra. | |
| -Require universal_algebra. | |
| +Require Import MathClasses.interfaces.abstract_algebra. | |
| +Require MathClasses.interfaces.universal_algebra. | |
| Module ua := universal_algebra. | |
| -Require varieties.monoids. | |
| -Require monoid_normalization. | |
| +Require MathClasses.varieties.monoids. | |
| +Require MathClasses.theory.monoid_normalization. | |
| Notation msig := varieties.monoids.sig. | |
| Notation Op := (ua.Op msig False). | |
| diff --git a/theory/rationals.v b/theory/rationals.v | |
| index 9e865f4..30bdf6d 100644 | |
| --- a/theory/rationals.v | |
| +++ b/theory/rationals.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring | |
| - abstract_algebra interfaces.integers interfaces.naturals interfaces.rationals | |
| - field_of_fractions natpair_integers | |
| - theory.rings theory.integers theory.dec_fields. | |
| + Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals | |
| + MathClasses.implementations.field_of_fractions MathClasses.implementations.natpair_integers | |
| + MathClasses.theory.rings MathClasses.theory.integers MathClasses.theory.dec_fields. | |
| Program Instance slow_rat_dec `{Rationals Q} : ∀ x y: Q, Decision (x = y) | 10 := λ x y, | |
| match decide (rationals_to_frac Q (SRpair nat) x = rationals_to_frac Q (SRpair nat) y) with | |
| diff --git a/theory/ring_congruence.v b/theory/ring_congruence.v | |
| index bf39995..d3a5f01 100644 | |
| --- a/theory/ring_congruence.v | |
| +++ b/theory/ring_congruence.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - Ring abstract_algebra theory.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings. | |
| Class RingCongruence A (R : relation A) `{Ring A} := | |
| { ring_congr_equivalence : Equivalence R | |
| diff --git a/theory/ring_ideals.v b/theory/ring_ideals.v | |
| index aa8b710..2938f67 100644 | |
| --- a/theory/ring_ideals.v | |
| +++ b/theory/ring_ideals.v | |
| @@ -1,9 +1,9 @@ | |
| (* We define what a ring ideal is, show that they yield congruences, | |
| define what a kernel is, and show that kernels are ideal. *) | |
| Require Import | |
| - Ring abstract_algebra theory.rings. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings. | |
| Require Export | |
| - theory.ring_congruence. | |
| + MathClasses.theory.ring_congruence. | |
| (* Require ua_congruence varieties.rings. *) | |
| diff --git a/theory/rings.v b/theory/rings.v | |
| index b3b49a3..42282f1 100644 | |
| --- a/theory/rings.v | |
| +++ b/theory/rings.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - varieties.monoids theory.groups strong_setoids. | |
| + MathClasses.varieties.monoids MathClasses.theory.groups MathClasses.theory.strong_setoids. | |
| Require Import | |
| - Ring abstract_algebra. | |
| + Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra. | |
| Definition is_ne_0 `(x : R) `{Equiv R} `{Zero R} `{p : PropHolds (x ≠0)} : x ≠0 := p. | |
| Definition is_nonneg `(x : R) `{Equiv R} `{Le R} `{Zero R} `{p : PropHolds (0 ≤ x)} : 0 ≤ x := p. | |
| diff --git a/theory/sequences.v b/theory/sequences.v | |
| index 5779ba0..2b28843 100644 | |
| --- a/theory/sequences.v | |
| +++ b/theory/sequences.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - theory.categories | |
| - interfaces.functors | |
| - abstract_algebra | |
| - interfaces.sequences. | |
| + MathClasses.theory.categories | |
| + MathClasses.interfaces.functors | |
| + MathClasses.interfaces.abstract_algebra | |
| + MathClasses.interfaces.sequences. | |
| Section contents. | |
| Context `{Sequence sq}. | |
| diff --git a/theory/series.v b/theory/series.v | |
| index 57fd458..0dc2efb 100644 | |
| --- a/theory/series.v | |
| +++ b/theory/series.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - Ring Factorial workaround_tactics | |
| - abstract_algebra interfaces.additional_operations interfaces.orders | |
| - interfaces.naturals interfaces.integers | |
| - theory.nat_pow theory.int_pow theory.streams. | |
| + Coq.setoid_ring.Ring Coq.Arith.Factorial MathClasses.misc.workaround_tactics | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders | |
| + MathClasses.interfaces.naturals MathClasses.interfaces.integers | |
| + MathClasses.theory.nat_pow MathClasses.theory.int_pow MathClasses.theory.streams. | |
| Local Existing Instance srorder_semiring. | |
| diff --git a/theory/setoids.v b/theory/setoids.v | |
| index c1d7dc4..fcf156e 100644 | |
| --- a/theory/setoids.v | |
| +++ b/theory/setoids.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra theory.products. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.products. | |
| Lemma ext_equiv_refl `{Setoid_Morphism A B f} : f = f. | |
| Proof. intros ?? E. pose proof (setoidmor_b f). now rewrite E. Qed. | |
| diff --git a/theory/shiftl.v b/theory/shiftl.v | |
| index 5902725..0e60bce 100644 | |
| --- a/theory/shiftl.v | |
| +++ b/theory/shiftl.v | |
| @@ -1,9 +1,9 @@ | |
| Require | |
| - orders.integers theory.dec_fields theory.nat_pow. | |
| + MathClasses.orders.integers MathClasses.theory.dec_fields MathClasses.theory.nat_pow. | |
| Require Import | |
| - Ring | |
| - abstract_algebra interfaces.naturals interfaces.integers | |
| - interfaces.additional_operations interfaces.orders. | |
| + Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers | |
| + MathClasses.interfaces.additional_operations MathClasses.interfaces.orders. | |
| Section shiftl. | |
| Context `{SemiRing A} `{!LeftCancellation (.*.) (2:A)} `{SemiRing B} `{!Biinduction B} `{!ShiftLSpec A B sl}. | |
| diff --git a/theory/streams.v b/theory/streams.v | |
| index 8397103..4f6bf41 100644 | |
| --- a/theory/streams.v | |
| +++ b/theory/streams.v | |
| @@ -1,7 +1,7 @@ | |
| (* In the standard library equality on streams is defined as pointwise Leibniz equality. | |
| Here we prove similar results, but we use setoid equality instead. *) | |
| -Require Export Streams. | |
| -Require Import peano_naturals abstract_algebra. | |
| +Require Export Coq.Lists.Streams. | |
| +Require Import MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra. | |
| Section streams. | |
| Context `{Setoid A}. | |
| diff --git a/theory/strong_setoids.v b/theory/strong_setoids.v | |
| index 9a2bc17..6373752 100644 | |
| --- a/theory/strong_setoids.v | |
| +++ b/theory/strong_setoids.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra jections. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.theory.jections. | |
| Section contents. | |
| Context `{StrongSetoid A}. | |
| diff --git a/theory/ua_congruence.v b/theory/ua_congruence.v | |
| index b9927ad..ecbf24f 100644 | |
| --- a/theory/ua_congruence.v | |
| +++ b/theory/ua_congruence.v | |
| @@ -1,9 +1,9 @@ | |
| Require Import | |
| - Morphisms RelationClasses Relation_Definitions List | |
| - universal_algebra ua_homomorphisms canonical_names ua_subalgebraT util. | |
| -Require ua_products. | |
| + Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List | |
| + MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util. | |
| +Require MathClasses.theory.ua_products. | |
| -Require theory.categories. | |
| +Require MathClasses.theory.categories. | |
| (* Remove this *) | |
| Local Hint Transparent Equiv : typeclass_instances. | |
| diff --git a/theory/ua_homomorphisms.v b/theory/ua_homomorphisms.v | |
| index 709a0b4..2f45671 100644 | |
| --- a/theory/ua_homomorphisms.v | |
| +++ b/theory/ua_homomorphisms.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra universal_algebra. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra. | |
| Section contents. | |
| Variable σ: Signature. | |
| diff --git a/theory/ua_mapped_operations.v b/theory/ua_mapped_operations.v | |
| index d40cd50..33783d5 100644 | |
| --- a/theory/ua_mapped_operations.v | |
| +++ b/theory/ua_mapped_operations.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra universal_algebra. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra. | |
| Section contents. | |
| Variable Sorts: Set. | |
| diff --git a/theory/ua_packed.v b/theory/ua_packed.v | |
| index cecb08f..4f6fd5a 100644 | |
| --- a/theory/ua_packed.v | |
| +++ b/theory/ua_packed.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - canonical_names universal_algebra Program. | |
| + MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra Coq.Program.Program. | |
| Section packed. | |
| Context (σ: Signature) {V: Type}. | |
| diff --git a/theory/ua_products.v b/theory/ua_products.v | |
| index f21e356..2880fb3 100644 | |
| --- a/theory/ua_products.v | |
| +++ b/theory/ua_products.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - abstract_algebra | |
| - universal_algebra ua_homomorphisms | |
| - theory.categories categories.varieties. | |
| -Require theory.setoids. | |
| + MathClasses.interfaces.abstract_algebra | |
| + MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms | |
| + MathClasses.theory.categories MathClasses.categories.varieties. | |
| +Require MathClasses.theory.setoids. | |
| Section algebras. | |
| Context | |
| @@ -174,7 +174,7 @@ Section varieties. | |
| Qed. | |
| End varieties. | |
| -Require categories.varieties. | |
| +Require MathClasses.categories.varieties. | |
| Section categorical. | |
| Context | |
| diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v | |
| index 85684c9..1d24cad 100644 | |
| --- a/theory/ua_subalgebra.v | |
| +++ b/theory/ua_subalgebra.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - RelationClasses | |
| - universal_algebra ua_homomorphisms canonical_names theory.categories abstract_algebra. | |
| + Coq.Classes.RelationClasses | |
| + MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.interfaces.abstract_algebra. | |
| Require | |
| - categories.algebras forget_algebra. | |
| + MathClasses.categories.algebras MathClasses.theory.forget_algebra. | |
| Section subalgebras. | |
| Context `{Algebra sign A} (P: ∀ s, A s → Prop). | |
| diff --git a/theory/ua_subalgebraT.v b/theory/ua_subalgebraT.v | |
| index 3a107c5..b1a824e 100644 | |
| --- a/theory/ua_subalgebraT.v | |
| +++ b/theory/ua_subalgebraT.v | |
| @@ -4,10 +4,10 @@ instead of Prop (and with carrier sigT instead of sig). | |
| Hopefully one day Coq's universe polymorphism will permit a merge of sig and sigT, | |
| at which point we may try to merge ua_subalgebra and ua_subalgebraT as well. *) | |
| Require Import | |
| - RelationClasses | |
| - universal_algebra ua_homomorphisms theory.categories abstract_algebra. | |
| + Coq.Classes.RelationClasses | |
| + MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.interfaces.abstract_algebra. | |
| Require | |
| - categories.algebras. | |
| + MathClasses.categories.algebras. | |
| Section subalgebras. | |
| Context `{Algebra sign A} (P: ∀ s, A s → Type). | |
| diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v | |
| index bacb143..a86da26 100644 | |
| --- a/theory/ua_subvariety.v | |
| +++ b/theory/ua_subvariety.v | |
| @@ -1,6 +1,6 @@ | |
| Require Import | |
| - RelationClasses Morphisms Program | |
| - universal_algebra canonical_names ua_subalgebra. | |
| + Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program | |
| + MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra. | |
| (* In theory/ua_subalgebra.v we defined closed proper subsets and showed that | |
| they yield subalgebras. We now expand on this result and show that they | |
| diff --git a/theory/ua_term_monad.v b/theory/ua_term_monad.v | |
| index 98e6cf9..9c5360b 100644 | |
| --- a/theory/ua_term_monad.v | |
| +++ b/theory/ua_term_monad.v | |
| @@ -1,5 +1,5 @@ | |
| Require Import | |
| - abstract_algebra universal_algebra interfaces.monads. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.monads. | |
| Section contents. | |
| Context (operation: Set) (operation_type: operation → OpType unit). | |
| diff --git a/theory/ua_transference.v b/theory/ua_transference.v | |
| index 2b20098..25f51a8 100644 | |
| --- a/theory/ua_transference.v | |
| +++ b/theory/ua_transference.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms | |
| - canonical_names theory.categories ua_mapped_operations. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms | |
| + MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.theory.ua_mapped_operations. | |
| -Require categories.varieties. | |
| +Require MathClasses.categories.varieties. | |
| Section contents. | |
| diff --git a/varieties/abgroup.v b/varieties/abgroup.v | |
| index 91933cf..0736dfe 100644 | |
| --- a/varieties/abgroup.v | |
| +++ b/varieties/abgroup.v | |
| @@ -1,8 +1,8 @@ | |
| (* To be imported qualified. *) | |
| Require | |
| - categories.varieties categories.product forget_algebra forget_variety theory.groups. | |
| + MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety MathClasses.theory.groups. | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics. | |
| Inductive op := mult | inv | one. | |
| diff --git a/varieties/closed_terms.v b/varieties/closed_terms.v | |
| index f5a5d2f..f331931 100644 | |
| --- a/varieties/closed_terms.v | |
| +++ b/varieties/closed_terms.v | |
| @@ -1,8 +1,8 @@ | |
| Require Import | |
| - RelationClasses Relation_Definitions List Morphisms | |
| - universal_algebra ua_homomorphisms | |
| - abstract_algebra canonical_names | |
| - theory.categories categories.varieties. | |
| + Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms | |
| + MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names | |
| + MathClasses.theory.categories MathClasses.categories.varieties. | |
| Section contents. | |
| Variable et: EquationalTheory. | |
| diff --git a/varieties/empty.v b/varieties/empty.v | |
| index 2b15791..d6681c6 100644 | |
| --- a/varieties/empty.v | |
| +++ b/varieties/empty.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - theory.rings categories.varieties. | |
| + MathClasses.theory.rings MathClasses.categories.varieties. | |
| Require Import | |
| - abstract_algebra universal_algebra. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra. | |
| Definition op := False. | |
| diff --git a/varieties/groups.v b/varieties/groups.v | |
| index 6e7c69b..43b722c 100644 | |
| --- a/varieties/groups.v | |
| +++ b/varieties/groups.v | |
| @@ -1,8 +1,8 @@ | |
| (* To be imported qualified. *) | |
| Require | |
| - categories.varieties categories.product forget_algebra forget_variety theory.groups. | |
| + MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety MathClasses.theory.groups. | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics. | |
| Inductive op := mult | inv | one. | |
| diff --git a/varieties/monoids.v b/varieties/monoids.v | |
| index f1c736c..78c07da 100644 | |
| --- a/varieties/monoids.v | |
| +++ b/varieties/monoids.v | |
| @@ -1,9 +1,9 @@ | |
| (* To be imported qualified. *) | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics | |
| - categories.categories. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics | |
| + MathClasses.categories.categories. | |
| Require | |
| - categories.varieties categories.product forget_algebra forget_variety. | |
| + MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety. | |
| Inductive op := mult | one. | |
| diff --git a/varieties/open_terms.v b/varieties/open_terms.v | |
| index 526042d..0d1f5d8 100644 | |
| --- a/varieties/open_terms.v | |
| +++ b/varieties/open_terms.v | |
| @@ -1,7 +1,7 @@ | |
| Require Import | |
| - RelationClasses Relation_Definitions List Morphisms | |
| - universal_algebra abstract_algebra canonical_names | |
| - theory.categories categories.varieties. | |
| + Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms | |
| + MathClasses.interfaces.universal_algebra MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names | |
| + MathClasses.theory.categories MathClasses.categories.varieties. | |
| Section contents. | |
| Context | |
| diff --git a/varieties/rings.v b/varieties/rings.v | |
| index 1cbcc57..c4c1024 100644 | |
| --- a/varieties/rings.v | |
| +++ b/varieties/rings.v | |
| @@ -1,9 +1,9 @@ | |
| (* To be imported qualified. *) | |
| Require | |
| - categories.varieties theory.rings. | |
| + MathClasses.categories.varieties MathClasses.theory.rings. | |
| Require Import | |
| - Ring | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics. | |
| + Coq.setoid_ring.Ring | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics. | |
| Inductive op := plus | mult | zero | one | negate. | |
| diff --git a/varieties/semigroups.v b/varieties/semigroups.v | |
| index d4dd808..7d522ce 100644 | |
| --- a/varieties/semigroups.v | |
| +++ b/varieties/semigroups.v | |
| @@ -1,8 +1,8 @@ | |
| (* To be imported qualified. *) | |
| Require | |
| - categories.varieties categories.product forget_algebra forget_variety. | |
| + MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety. | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics. | |
| Inductive op := mult. | |
| diff --git a/varieties/semirings.v b/varieties/semirings.v | |
| index 4fc8910..ea977d6 100644 | |
| --- a/varieties/semirings.v | |
| +++ b/varieties/semirings.v | |
| @@ -1,8 +1,8 @@ | |
| (* To be imported qualified. *) | |
| Require | |
| - theory.rings categories.varieties. | |
| + MathClasses.theory.rings MathClasses.categories.varieties. | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms workaround_tactics. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics. | |
| Inductive op := plus | mult | zero | one. | |
| diff --git a/varieties/setoids.v b/varieties/setoids.v | |
| index fee4ec4..1564030 100644 | |
| --- a/varieties/setoids.v | |
| +++ b/varieties/setoids.v | |
| @@ -1,7 +1,7 @@ | |
| Require | |
| - categories.varieties. | |
| + MathClasses.categories.varieties. | |
| Require Import | |
| - abstract_algebra universal_algebra ua_homomorphisms. | |
| + MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms. | |
| Definition op := False. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment