Merge branch 'master' of /home/robbert/formath/math-classes

Conflicts:
	MathClasses/categories/algebra.v
	MathClasses/categories/cat.v
	MathClasses/categories/functor.v
	MathClasses/categories/setoid.v
	MathClasses/categories/variety.v
	MathClasses/varieties/group.v
	MathClasses/varieties/monoid.v
	MathClasses/varieties/ring.v
	MathClasses/varieties/semigroup.v
	MathClasses/varieties/semiring.v
	MathClasses/varieties/setoid.v
	papers/mscs/mscs.tex
	src/categories/algebra.v
	src/categories/algebras.v
	src/categories/cat.v
	src/categories/categories.v
	src/categories/functor.v
	src/categories/functors.v
	src/categories/setoid.v
	src/categories/setoids.v
	src/categories/varieties.v
	src/categories/variety.v
	src/varieties/group.v
	src/varieties/groups.v
	src/varieties/monoid.v
	src/varieties/monoids.v
	src/varieties/ring.v
	src/varieties/rings.v
	src/varieties/semigroup.v
	src/varieties/semigroups.v
	src/varieties/semiring.v
	src/varieties/semirings.v
	src/varieties/setoid.v
	src/varieties/setoids.v
	tools/DepsToDot.hs

MathClasses/categories/JMcat.v

@@ -1,8 +1,7 @@
 Require
   JMrelation.
 Require Import
-  Relation_Definitions Morphisms Setoid Program
-  abstract_algebra interfaces.functors theory.categories.
+  Relation_Definitions abstract_algebra interfaces.functors theory.categories.
 
 Record Object := object
   { obj:> Type

MathClasses/categories/algebra.v → MathClasses/categories/algebras.v

@@ -1,8 +1,8 @@
 (* Show that algebras with homomorphisms between them form a category. *)
 Require Import
-  Morphisms Setoid abstract_algebra Program universal_algebra ua_homomorphisms theory.categories.
+  abstract_algebra universal_algebra ua_homomorphisms theory.categories.
 Require
-  categories.setoid categories.product.
+  categories.setoids categories.product.
 
 Record Object (sign: Signature) : Type := object
   { algebra_carriers:> sorts sign → Type

MathClasses/categories/cat.v → MathClasses/categories/categories.v

@@ -1,6 +1,5 @@
 Require Import
-  Relation_Definitions Morphisms Setoid Program
-  abstract_algebra interfaces.functors theory.categories.
+  Relation_Definitions abstract_algebra interfaces.functors theory.categories.
 
 Record Object := object
   { obj:> Type

MathClasses/categories/dual.v

@@ -1,6 +1,5 @@
 Require Import
-  Relation_Definitions Morphisms Setoid Program
-  abstract_algebra theory.categories interfaces.functors.
+  Relation_Definitions abstract_algebra theory.categories interfaces.functors.
 
 Section contents.
 

MathClasses/categories/functor.v → MathClasses/categories/functors.v

@@ -1,6 +1,6 @@
 Require Import
-  Morphisms RelationClasses Equivalence Setoid
-  abstract_algebra interfaces.functors categories.
+  RelationClasses Equivalence
+  abstract_algebra interfaces.functors theory.categories.
 
 Section natural_transformations_id_comp.
   Context

MathClasses/categories/product.v

@@ -1,7 +1,7 @@
 Require Import
-  Relation_Definitions Morphisms Setoid Program
+  Relation_Definitions
   abstract_algebra ChoiceFacts interfaces.functors 
-  theory.categories categories.cat.
+  theory.categories categories.categories.
 
 (* Axiom dependent_functional_choice: DependentFunctionalChoice. *)
 
@@ -42,12 +42,12 @@ Section contents.
    repeat intro. apply id_r.
   Qed.
 
-  Let product_object := cat.object (Object O).
+  Let product_object := categories.object (Object O).
 
-  Notation ith_obj i := (cat.object (O i)).
+  Notation ith_obj i := (categories.object (O i)).
 
-  Program Definition project i: cat.object (Object O) ⟶ ith_obj i :=
-    cat.arrow (λ d, d i) (λ _ _ a, a i) _.
+  Program Definition project i: categories.object (Object O) ⟶ ith_obj i :=
+    categories.arrow (λ d, d i) (λ _ _ a, a i) _.
   Next Obligation. Proof. (* functorial *)
    constructor; intros; try reflexivity; try apply _.
    constructor; try apply _.
@@ -56,13 +56,13 @@ Section contents.
 
   Section factors.
 
-    Variables (C: cat.Object) (X: ∀ i, C ⟶ ith_obj i).
+    Variables (C: categories.Object) (X: ∀ i, C ⟶ ith_obj i).
 
-    Let ith_functor i := cat.Functor_inst _ _ (X i).
+    Let ith_functor i := categories.Functor_inst _ _ (X i).
       (* todo: really necessary? *)
 
     Program Definition factor: C ⟶ product_object
-      := cat.arrow (λ (c: C) i, X i c) (λ (x y: C) (c: x ⟶ y) i, fmap (X i) c) _.
+      := categories.arrow (λ (c: C) i, X i c) (λ (x y: C) (c: x ⟶ y) i, fmap (X i) c) _.
     Next Obligation. Proof with try reflexivity; intuition. (* functorial *)
      constructor; intros; try apply _.
        constructor; try apply _.
@@ -86,7 +86,7 @@ Section contents.
      simpl.
      intros [x H4].
      unfold equiv.
-     unfold cat.e.
+     unfold categories.e.
      unfold compose in H4.
      set (P := λ v, prod (alt v ⟶ (λ i, (X i) v)) ((λ i, (X i) v) ⟶ alt v)).
      set (d := λ v, (λ i, snd (` (x i v)), λ i, fst (` (x i v))): P v).
@@ -107,17 +107,17 @@ Section contents.
      simpl in *.
      unfold uncurry in *.
      unfold iso_arrows in *.
-     destruct (cat.Functor_inst _ _ alt).
+     destruct (categories.Functor_inst _ _ alt).
      unfold compose in x, aa0, a1a2.
      simpl in *.
      unfold fmap.
      match goal with
-       |- appcontext [ cat.Fmap_inst _ ?cat ?alt ] => set (f:=cat.Fmap_inst _ cat alt) in |- *
+       |- appcontext [ categories.Fmap_inst _ ?cat ?alt ] => set (f:=categories.Fmap_inst _ cat alt) in |- *
      end.
      setoid_rewrite <- (left_identity (f p q r i ◎ fst aa0)).
      transitivity ((fst a1a2 ◎ snd a1a2) ◎ (f p q r i ◎ fst aa0)).
       apply comp_proper...
-     apply transitivity with ((fst a1a2) ◎ (((snd a1a2) ◎ (cat.Fmap_inst _ _ alt p q r i)) ◎ (fst aa0))).
+     apply transitivity with ((fst a1a2) ◎ (((snd a1a2) ◎ (categories.Fmap_inst _ _ alt p q r i)) ◎ (fst aa0))).
       repeat rewrite associativity...
      simpl.
      rewrite <- H5.

MathClasses/categories/setoid.v → MathClasses/categories/setoids.v

@@ -1,6 +1,5 @@
 Require Import
-  Relation_Definitions Morphisms Setoid Program
-  abstract_algebra theory.categories.
+  Relation_Definitions abstract_algebra theory.categories.
 
 Inductive Object := object { T:> Type; e: Equiv T; setoid_proof: Setoid T }.
 

MathClasses/categories/unit.v

@@ -1,6 +1,6 @@
 Require Import
-  Morphisms RelationClasses Equivalence Setoid
-  categories abstract_algebra functors.
+  RelationClasses Equivalence
+  categories.categories abstract_algebra categories.functors.
 
 Instance: Arrows unit := λ _ _, unit.
 Instance: CatId unit := λ _, tt.

MathClasses/categories/variety.v → MathClasses/categories/varieties.v

@@ -5,7 +5,7 @@ factor out the commonality.
 
  *)
 Require Import 
-  Morphisms abstract_algebra Program universal_algebra ua_homomorphisms.
+  abstract_algebra universal_algebra ua_homomorphisms.
 
 Record Object (et: EquationalTheory) : Type := object
   { variety_carriers:> sorts et → Type

MathClasses/implementations/NType_naturals.v

@@ -36,7 +36,7 @@ Proof. repeat split; repeat intro; axioms.zify; auto with zarith. Qed.
 
 Instance: SemiRing t | 10 := rings.from_stdlib_semiring_theory NType_semiring_theory.
 
-Instance inject_NType_N: Coerce t N := to_N.
+Instance inject_NType_N: Cast t N := to_N.
 
 Instance: Proper ((=) ==> (=)) to_N. 
 Proof. intros x y E. unfold equiv, NType_equiv, eq in E. unfold to_N. now rewrite E. Qed.
@@ -50,7 +50,7 @@ Proof.
   unfold mon_unit, ringone_is_monoidunit, NType_1. now rewrite spec_1.
 Qed.
 
-Instance inject_N_NType: Coerce N t := of_N.
+Instance inject_N_NType: Cast N t := of_N.
 Instance: Inverse to_N := of_N.
 
 Instance: Surjective to_N.
@@ -81,7 +81,7 @@ Proof. change (SemiRing_Morphism (to_N⁻¹)). split; apply _. Qed.
 Instance: NaturalsToSemiRing t := naturals.retract_is_nat_to_sr of_N.
 Instance: Naturals t := naturals.retract_is_nat of_N.
 
-Instance inject_NType_Z: Coerce t Z := to_Z.
+Instance inject_NType_Z: Cast t Z := to_Z.
 
 Instance: Proper ((=) ==> (=)) to_Z. 
 Proof. now intros x y E. Qed.

MathClasses/implementations/QType_rationals.v

@@ -1,7 +1,7 @@
 Require
   theory.fields stdlib_rationals theory.int_pow.
 Require Import
-  Program QArith QSig
+  QArith QSig
   abstract_algebra interfaces.orders
   interfaces.integers interfaces.rationals interfaces.additional_operations
   theory.rings theory.rationals.
@@ -53,15 +53,15 @@ Proof.
 Qed.
 
 (* Type-classified facts about to_Q/of_Q: *)
-Instance inject_QType_Q: Coerce t Q := to_Q.
+Instance inject_QType_Q: Cast t Q := to_Q.
 
 Instance: Setoid_Morphism to_Q.
 Proof. constructor; try apply _. intros x y. auto. Qed.
 
 Instance: SemiRing_Morphism to_Q.
 Proof. repeat (constructor; try apply _); intros; qify; reflexivity. Qed.
 
-Instance inject_Q_QType: Coerce Q t := of_Q.
+Instance inject_Q_QType: Cast Q t := of_Q.
 Instance: Inverse to_Q := of_Q.
 
 Instance: Surjective to_Q.

MathClasses/implementations/ZType_integers.v

@@ -1,7 +1,7 @@
 Require 
   stdlib_binary_integers theory.integers orders.semirings.
 Require Import 
-  ZSig ZSigZAxioms NArith ZArith Program Morphisms
+  ZSig ZSigZAxioms NArith ZArith
   nonneg_integers_naturals interfaces.orders
   abstract_algebra interfaces.integers interfaces.additional_operations.  
 
@@ -38,7 +38,7 @@ Proof. repeat split; repeat intro; axioms.zify; auto with zarith. Qed.
 
 Instance: Ring t | 10 := rings.from_stdlib_ring_theory ZType_ring_theory.
 
-Instance inject_ZType_Z: Coerce t Z := to_Z.
+Instance inject_ZType_Z: Cast t Z := to_Z.
 
 Instance: Proper ((=) ==> (=)) to_Z. 
 Proof. intros x y E. easy. Qed.
@@ -52,7 +52,7 @@ Proof.
   exact spec_1.
 Qed.
 
-Instance inject_Z_ZType: Coerce Z t := of_Z.
+Instance inject_Z_ZType: Cast Z t := of_Z.
 Instance: Inverse to_Z := of_Z.
 
 Instance: Surjective to_Z.

MathClasses/implementations/cons_list.v

@@ -1,5 +1,5 @@
 Require Import
- Morphisms List Program
+ List
  abstract_algebra interfaces.monads.
 
 Implicit Arguments app [[A]].

MathClasses/implementations/dyadics.v

@@ -4,7 +4,7 @@
    embedded into any [Rationals] implementation [Q]. 
 *)
 Require Import
-  Morphisms Ring Program RelationClasses Setoid
+  Ring RelationClasses
   abstract_algebra 
   interfaces.integers interfaces.naturals interfaces.rationals
   interfaces.additional_operations interfaces.orders
@@ -35,7 +35,7 @@ Global Program Instance dy_plus: RingPlus Dyadic := λ x y,
 Next Obligation. now apply rings.flip_nonneg_minus. Qed.
 Next Obligation. apply rings.flip_nonneg_minus. now apply orders.le_flip. Qed.
 
-Global Instance dy_inject: Coerce Z Dyadic := λ x, x $ 0.
+Global Instance dy_inject: Cast Z Dyadic := λ x, x $ 0.
 Global Instance dy_opp: GroupInv Dyadic := λ x, -mant x $ expo x.
 Global Instance dy_mult: RingMult Dyadic := λ x y, mant x * mant y $ expo x + expo y.
 Global Instance dy_0: RingZero Dyadic := ('0 : Dyadic).
@@ -67,7 +67,7 @@ Section with_rationals.
   Proof.
     rewrite shiftl_nat_pow.
     rewrite rings.preserves_mult, nat_pow.preserves_nat_pow, rings.preserves_2.
-    now rewrite <-(int_pow_nat_pow (f:=coerce (Z⁺) Z)).
+    now rewrite <-(int_pow_nat_pow (f:=cast (Z⁺) Z)).
   Qed.
 
   Lemma DtoQ_slow_preserves_plus x y : DtoQ_slow' (x + y) = DtoQ_slow' x + DtoQ_slow' y.

MathClasses/implementations/fast_integers.v

@@ -1,13 +1,13 @@
 Require Import 
-  Morphisms BigZ
-  interfaces.abstract_algebra interfaces.integers 
+  BigZ
+  interfaces.abstract_algebra interfaces.integers
   interfaces.additional_operations fast_naturals.
 Require Export
   ZType_integers.
 
 Module BigZ_Integers := ZType_Integers BigZ.
 
-Instance inject_fastN_fastZ: Coerce bigN bigZ := BigZ.Pos.
+Instance inject_fastN_fastZ: Cast bigN bigZ := BigZ.Pos.
 
 Instance: SemiRing_Morphism inject_fastN_fastZ.
 Proof. repeat (split; try apply _); intuition. Qed.
@@ -22,7 +22,7 @@ Proof.
   intros x n.
   rewrite rings.preserves_plus, rings.preserves_1, BigZ.add_1_l.
   apply BigZ.pow_succ_r.
-  change (0 ≤ coerce bigN bigZ n).
+  change (0 ≤ cast bigN bigZ n).
   now apply naturals.to_semiring_nonneg.
 Qed.
 
@@ -32,6 +32,6 @@ Instance: ShiftLSpec bigZ bigN _.
 Proof.
   apply shiftl_spec_from_nat_pow.
   intros. apply BigZ.shiftl_mul_pow2.
-  change (0 ≤ coerce bigN bigZ n).
+  change (0 ≤ cast bigN bigZ n).
   now apply naturals.to_semiring_nonneg.
 Qed.

MathClasses/implementations/fast_rationals.v

@@ -1,19 +1,19 @@
 Require
   theory.shiftl theory.int_pow.
 Require Import
-  QArith BigQ Morphisms Program
-  abstract_algebra interfaces.integers interfaces.rationals 
-  interfaces.additional_operations
+  QArith BigQ
+  abstract_algebra
+  interfaces.integers interfaces.rationals interfaces.additional_operations
   fast_naturals fast_integers field_of_fractions stdlib_rationals.
-Require Export 
+Require Export
   QType_rationals.
 
 Module Import BigQ_Rationals := QType_Rationals BigQ.
 
 (* Embedding of [bigZ] into [bigQ] *)
-Instance inject_bigZ_bigQ: Coerce bigZ bigQ := BigQ.Qz.
-Instance inject_bigN_bigQ: Coerce bigN bigQ := coerce bigZ bigQ ∘ coerce bigN bigZ.
-Instance inject_Z_bigQ: Coerce Z bigQ := coerce bigZ bigQ ∘ coerce Z bigZ.
+Instance inject_bigZ_bigQ: Cast bigZ bigQ := BigQ.Qz.
+Instance inject_bigN_bigQ: Cast bigN bigQ := cast bigZ bigQ ∘ cast bigN bigZ.
+Instance inject_Z_bigQ: Cast Z bigQ := cast bigZ bigQ ∘ cast Z bigZ.
 
 Instance: Proper ((=) ==> (=)) inject_bigZ_bigQ.
 Proof.
@@ -55,11 +55,11 @@ Proof.
 Qed.
 
 Lemma bigQ_div_bigQq_alt (n : bigZ) (d : bigN) :
-  BigQ.Qq n d = 'n / 'coerce bigN bigZ d.
+  BigQ.Qq n d = 'n / 'cast bigN bigZ d.
 Proof. apply bigQ_div_bigQq. Qed.
 
 (* Embedding of [bigQ] into [Frac bigZ] *)
-Instance inject_bigQ_frac_bigZ: Coerce bigQ (Frac bigZ) := λ x,
+Instance inject_bigQ_frac_bigZ: Cast bigQ (Frac bigZ) := λ x,
   match x with
   | BigQ.Qz n => 'n
   | BigQ.Qq n d =>
@@ -70,19 +70,19 @@ Instance inject_bigQ_frac_bigZ: Coerce bigQ (Frac bigZ) := λ x,
   end.
 
 Lemma inject_bigQ_frac_bigZ_correct:
- coerce bigQ (Frac bigZ) = rationals_to_frac bigQ bigZ.
+ cast bigQ (Frac bigZ) = rationals_to_frac bigQ bigZ.
 Proof.
   intros x y E. rewrite <-E. clear y E.
   destruct x as [n|n d].
    rapply (integers.to_ring_unique_alt 
-     (coerce bigZ (Frac bigZ)) (rationals_to_frac bigQ bigZ ∘ coerce bigZ bigQ)).
-  unfold coerce at 1. simpl.
+     (cast bigZ (Frac bigZ)) (rationals_to_frac bigQ bigZ ∘ cast bigZ bigQ)).
+  unfold cast at 1. simpl.
   rewrite bigQ_div_bigQq_alt.
   rewrite rings.preserves_mult, dec_fields.preserves_dec_mult_inv.
   case (decide_rel (=) ('d : bigZ) 0); intros Ed.
    rewrite Ed, !rings.preserves_0, dec_mult_inv_0.
    now rewrite rings.mult_0_r.
-  rewrite 2!(integers.to_ring_twice _ _ (coerce bigZ (Frac bigZ))).
+  rewrite 2!(integers.to_ring_twice _ _ (cast bigZ (Frac bigZ))).
   now rewrite Frac_dec_mult_num_den at 1.
 Qed.
 
@@ -121,18 +121,18 @@ Proof.
     change (BigZ.Neg k) with (-'k : bigZ).
     rewrite int_pow.int_pow_opp.
     rewrite bigQ_div_bigQq, shiftl.preserves_shiftl.
-    rewrite <-(shiftl.preserves_shiftl_exp (f:=coerce bigN bigZ)).
+    rewrite <-(shiftl.preserves_shiftl_exp (f:=cast bigN bigZ)).
     now rewrite rings.preserves_1, shiftl.shiftl_base_1_int_pow.
    rewrite 2!bigQ_div_bigQq.
    rewrite shiftl.preserves_shiftl.
-   rewrite <-(shiftl.preserves_shiftl_exp (f:=coerce bigN bigZ)).
+   rewrite <-(shiftl.preserves_shiftl_exp (f:=cast bigN bigZ)).
    rewrite shiftl.shiftl_int_pow.
-   now rewrite <-2!associativity, (commutativity (/coerce bigN bigQ d)).
+   now rewrite <-2!associativity, (commutativity (/cast bigN bigQ d)).
   change (BigZ.Neg k) with (-'k : bigZ).
   rewrite int_pow.int_pow_opp.
   rewrite 2!bigQ_div_bigQq.
   rewrite shiftl.preserves_shiftl.
-  rewrite <-(shiftl.preserves_shiftl_exp (f:=coerce bigN bigZ)).
+  rewrite <-(shiftl.preserves_shiftl_exp (f:=cast bigN bigZ)).
   rewrite shiftl.shiftl_int_pow.
   now rewrite dec_fields.dec_mult_inv_distr, associativity.
 Qed.

MathClasses/implementations/field_of_fractions.v

@@ -32,7 +32,7 @@ Global Instance Frac_dec : ∀ x y: Frac R, Decision (x = y)
   := λ x y, decide_rel (=) (num x * den y) (num y * den x).
 
 (* injection from R *)
-Global Program Instance Frac_inject: Coerce R (Frac R) := λ r, frac r 1 _.
+Global Program Instance Frac_inject: Cast R (Frac R) := λ r, frac r 1 _.
 Next Obligation. exact (is_ne_0 1). Qed.
 
 Instance: Proper ((=) ==> (=)) Frac_inject.

MathClasses/implementations/intfrac_rationals.v

@@ -8,5 +8,5 @@ Section intfrac_rationals.
   Context `{Integers Z}.
 
   Global Instance: RationalsToFrac (Frac Z) := alt_to_frac id.
-  Global Instance: Rationals (Frac Z) := alt_Build_Rationals id (coerce Z (Frac Z)).
+  Global Instance: Rationals (Frac Z) := alt_Build_Rationals id (cast Z (Frac Z)).
 End intfrac_rationals.