Merge branch 'master' into modular-arithmetic

CHANGELOG.md

@@ -16,6 +16,14 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now
+  parametrized by _raw_ bundles rather than lawful bundles, in line with other
+  modules defining morphism structures.
+* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now
+  parametrized by _raw_ bundles, and as such take a proof of transitivity.
+* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
+  parametrized by _raw_ bundles, and as such take a proof of reflexivity.
+
 Other major improvements
 ------------------------
 
@@ -25,6 +33,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.Semiring.Mult`:
+  ```agda
+  1×-identityʳ  ↦  ×-homo-1
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -33,6 +46,8 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
+
 * Integer arithmetic modulo `n`, based on `Data.Nat.Bounded.*`:
   ```agda
   Data.Integer.Modulo.Base
@@ -43,6 +58,64 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
+  ```agda
+  rawNearSemiring   : RawNearSemiring _ _
+  rawRingWithoutOne : RawRingWithoutOne _ _
+  +-rawGroup        : RawGroup _ _
+  ```
+
+* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
+
+* In `Algebra.Module.Construct.DirectProduct`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawLeftModule      : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawRightModule     : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawBisemimodule    : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawBimodule        : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawSemimodule      : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  rawModule          : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
+  ```
+
+* In `Algebra.Module.Construct.TensorUnit`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule _ c ℓ
+  rawLeftModule      : RawLeftModule _ c ℓ
+  rawRightSemimodule : RawRightSemimodule _ c ℓ
+  rawRightModule     : RawRightModule _ c ℓ
+  rawBisemimodule    : RawBisemimodule _ _ c ℓ
+  rawBimodule        : RawBimodule _ _ c ℓ
+  rawSemimodule      : RawSemimodule _ c ℓ
+  rawModule          : RawModule _ c ℓ
+  ```
+
+* In `Algebra.Module.Construct.Zero`:
+  ```agda
+  rawLeftSemimodule  : RawLeftSemimodule R c ℓ
+  rawLeftModule      : RawLeftModule R c ℓ
+  rawRightSemimodule : RawRightSemimodule R c ℓ
+  rawRightModule     : RawRightModule R c ℓ
+  rawBisemimodule    : RawBisemimodule R c ℓ
+  rawBimodule        : RawBimodule R c ℓ
+  rawSemimodule      : RawSemimodule R c ℓ
+  rawModule          : RawModule R c ℓ
+  ```
+
+* In `Algebra.Properties.Monoid.Mult`:
+  ```agda
+  ×-homo-0 : ∀ x → 0 × x ≈ 0#
+  ×-homo-1 : ∀ x → 1 × x ≈ x
+  ```
+
+* In `Algebra.Properties.Semiring.Mult`:
+  ```agda
+  ×-homo-0#     : ∀ x → 0 × x ≈ 0# * x
+  ×-homo-1#     : ∀ x → 1 × x ≈ 1# * x
+  idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n
@@ -99,3 +172,25 @@ Additions to existing modules
 
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
   be used infix.
+
+* Added new definitions in `Relation.Binary`
+  ```
+  Stable          : Pred A ℓ → Set _
+  ```
+
+* Added new definitions in `Relation.Nullary`
+  ```
+  Recomputable    : Set _
+  WeaklyDecidable : Set _
+  ```
+
+* Added new definitions in `Relation.Unary`
+  ```
+  Stable          : Pred A ℓ → Set _
+  WeaklyDecidable : Pred A ℓ → Set _
+  ```
+
+* Added new proof in `Relation.Nullary.Decidable`:
+  ```agda
+  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  ```

doc/README.agda

@@ -222,6 +222,10 @@ import Text.Printf
 
 import README.Case
 
+-- Showcasing the framework for well-scoped substitutions
+
+import README.Data.Fin.Substitution.UntypedLambda
+
 -- Some examples showing how combinators can be used to emulate
 -- "functional reasoning"
 

doc/README/Data/Fin/Substitution/UntypedLambda.agda

@@ -14,7 +14,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_)

doc/style-guide.md

@@ -121,15 +121,31 @@ automate most of this.
 
 * If it is important that certain names only come into scope later in
   the file then the module should still be imported at the top of the
-  file but it can be given a shorter name using the keyword `as` and then
-  opened later on in the file when needed, e.g.
+  file but it can be imported *qualified*, i.e. given a shorter name
+  using the keyword `as` and then opened later on in the file when needed,
+  e.g.
   ```agda
   import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
   ...
   ...
   open SetoidEquality S
   ```
 
+* Naming conventions for qualified `import`s: if importing a module under
+  a root of the form `Data.X` (e.g. the `Base` module for basic operations,
+  or `Properties` for lemmas about them etc.) then conventionally, the
+  qualified name(s) for the import(s) should (all) share as qualfied name
+  that of the name of the `X` datatype defined: i.e. `Data.Nat.Base`
+  should be imported as `ℕ`, `Data.List.Properties` as `List`,  etc.
+  In this spirit, the convention applies also to (the datatype defined by)
+  `Relation.Binary.PropositionalEquality.*` which should be imported qualified
+  with the name `≡`.
+  Other modules should be given a 'suitable' qualified name based on its 'long'
+  path-derived name (such as `SetoidEquality` in the example above); commonly
+  occcurring examples such as `Algebra.Structures` should be imported qualified
+  as `Structures` etc.
+  NB. Historical legacy means that these conventions have not always been observed!
+
 * When using only a few items (i.e. < 5) from a module, it is a good practice to
   enumerate the items that will be used by declaring the import statement
   with the directive `using`. This makes the dependencies clearer, e.g.
@@ -532,3 +548,22 @@ word within a compound word is capitalized except for the first word.
 
 * The names of patterns for reflected syntax are also *appended* with an
   additional backtick.
+
+#### Specific pragmatics/idiomatic patterns
+
+## Use of `with` notation
+
+Thinking on this has changed since the early days of the library, with
+a desire to avoid 'unnecessary' uses of `with`: see Issues
+[#1937](https://github.com/agda/agda-stdlib/issues/1937) and
+[#2123](https://github.com/agda/agda-stdlib/issues/2123).
+
+## Proving instances of `Decidable` for sets, predicates, relations, ...
+
+Issue [#803](https://github.com/agda/agda-stdlib/issues/803)
+articulates a programming pattern for writing proofs of decidability,
+used successfully in PR
+[#799](https://github.com/agda/agda-stdlib/pull/799) and made
+systematic for `Nary` relations in PR
+[#811](https://github.com/agda/agda-stdlib/pull/811)
+

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -21,7 +21,7 @@ open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
 open import Algebra.Properties.Ring ring
   using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
 open import Relation.Binary.Definitions using (Symmetric)
-import Relation.Binary.Reasoning.Setoid as ReasonSetoid
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
 
 private variable
@@ -50,7 +50,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
     = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
     where
-    open ReasonSetoid setoid
+    open ≈-Reasoning setoid
 
     y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
     y⁻¹*x⁻¹*x*y≈1 = begin
@@ -67,7 +67,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
 #-sym : Symmetric _#_
 #-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
   where
-  open ReasonSetoid setoid
+  open ≈-Reasoning setoid
   InvX-Y : Invertible _≈_ 1# _*_ (x - y)
   InvX-Y = #⇒invertible x#y
 
@@ -96,7 +96,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
     = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
     where
-    open ReasonSetoid setoid
+    open ≈-Reasoning setoid
 
     x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
     x-z⁻¹*y-z≈1 = begin

src/Algebra/Bundles.agda

@@ -961,6 +961,9 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; semiringWithoutAnnihilatingZero
     )
 
+  open NearSemiring nearSemiring public
+    using (rawNearSemiring)
+
   open AbelianGroup +-abelianGroup public
     using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma)
 
@@ -974,6 +977,9 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; 1#  = 1#
     }
 
+  open RawRing rawRing public
+    using (rawRingWithoutOne; +-rawGroup)
+
 
 record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_

src/Algebra/Construct/Flip/Op.agda

@@ -10,7 +10,7 @@
 module Algebra.Construct.Flip.Op where
 
 open import Algebra
-import Data.Product.Base as Prod
+import Data.Product.Base as Product
 import Data.Sum.Base as Sum
 open import Function.Base using (flip)
 open import Level using (Level)
@@ -39,7 +39,7 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
   associative sym assoc x y z = sym (assoc z y x)
 
   identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙)
-  identity id = Prod.swap id
+  identity id = Product.swap id
 
   commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙)
   commutative comm = flip comm
@@ -51,7 +51,7 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
   idempotent idem = idem
 
   inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙)
-  inverse inv = Prod.swap inv
+  inverse inv = Product.swap inv
 
 ------------------------------------------------------------------------
 -- Structures

src/Algebra/Construct/LexProduct.agda

@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction; contradiction₂)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct
   {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)

src/Algebra/Construct/LiftedChoice.agda

@@ -20,7 +20,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary using (Pred)
 
-import Relation.Binary.Reasoning.Setoid as EqReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
@@ -46,7 +46,7 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
 
   private module M = IsSelectiveMagma ∙-isSelectiveMagma
   open M hiding (sel; isMagma)
-  open EqReasoning setoid
+  open ≈-Reasoning setoid
 
   module _ (f : A → B) where
 

src/Algebra/Construct/Subst/Equality.agda

@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product.Base as Prod
+open import Data.Product.Base as Product
 open import Relation.Binary.Core
 
 module Algebra.Construct.Subst.Equality
@@ -45,13 +45,13 @@ sel : ∀ {∙} → Selective ≈₁ ∙ → Selective ≈₂ ∙
 sel sel x y = Sum.map to to (sel x y)
 
 identity : ∀ {∙ e} → Identity ≈₁ e ∙ → Identity ≈₂ e ∙
-identity = Prod.map (to ∘_) (to ∘_)
+identity = Product.map (to ∘_) (to ∘_)
 
 inverse : ∀ {∙ e ⁻¹} → Inverse ≈₁ ⁻¹ ∙ e → Inverse ≈₂ ⁻¹ ∙ e
-inverse = Prod.map (to ∘_) (to ∘_)
+inverse = Product.map (to ∘_) (to ∘_)
 
 absorptive : ∀ {∙ ◦} → Absorptive ≈₁ ∙ ◦ → Absorptive ≈₂ ∙ ◦
-absorptive = Prod.map (λ f x y → to (f x y)) (λ f x y → to (f x y))
+absorptive = Product.map (λ f x y → to (f x y)) (λ f x y → to (f x y))
 
 distribˡ : ∀ {∙ ◦} → _DistributesOverˡ_ ≈₁ ∙ ◦ → _DistributesOverˡ_ ≈₂ ∙ ◦
 distribˡ distribˡ x y z = to (distribˡ x y z)
@@ -60,7 +60,7 @@ distribʳ : ∀ {∙ ◦} → _DistributesOverʳ_ ≈₁ ∙ ◦ → _Distribute
 distribʳ distribʳ x y z = to (distribʳ x y z)
 
 distrib : ∀ {∙ ◦} → _DistributesOver_ ≈₁ ∙ ◦ → _DistributesOver_ ≈₂ ∙ ◦
-distrib {∙} {◦} = Prod.map (distribˡ {∙} {◦}) (distribʳ {∙} {◦})
+distrib {∙} {◦} = Product.map (distribˡ {∙} {◦}) (distribʳ {∙} {◦})
 
 ------------------------------------------------------------------------
 -- Structures
@@ -92,7 +92,7 @@ isSelectiveMagma S = record
 isMonoid : ∀ {∙ ε} → IsMonoid ≈₁ ∙ ε → IsMonoid ≈₂ ∙ ε
 isMonoid S = record
   { isSemigroup = isSemigroup S.isSemigroup
-  ; identity    = Prod.map (to ∘_) (to ∘_) S.identity
+  ; identity    = Product.map (to ∘_) (to ∘_) S.identity
   } where module S = IsMonoid S
 
 isCommutativeMonoid : ∀ {∙ ε} →
@@ -113,7 +113,7 @@ isIdempotentCommutativeMonoid {∙} S = record
 isGroup : ∀ {∙ ε ⁻¹} → IsGroup ≈₁ ∙ ε ⁻¹ → IsGroup ≈₂ ∙ ε ⁻¹
 isGroup S = record
   { isMonoid = isMonoid S.isMonoid
-  ; inverse  = Prod.map (to ∘_) (to ∘_) S.inverse
+  ; inverse  = Product.map (to ∘_) (to ∘_) S.inverse
   ; ⁻¹-cong  = cong₁ S.⁻¹-cong
   } where module S = IsGroup S
 
@@ -141,7 +141,7 @@ isSemiringWithoutOne {+} {*} S = record
   ; *-cong                = cong₂ S.*-cong
   ; *-assoc               = assoc {*} S.*-assoc
   ; distrib               = distrib {*} {+} S.distrib
-  ; zero                  = Prod.map (to ∘_) (to ∘_) S.zero
+  ; zero                  = Product.map (to ∘_) (to ∘_) S.zero
   } where module S = IsSemiringWithoutOne S
 
 isCommutativeSemiringWithoutOne : ∀ {+ * 0#} →

src/Algebra/Lattice/Construct/Subst/Equality.agda

@@ -12,7 +12,7 @@
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Lattice.Structures
-open import Data.Product.Base as Prod
+open import Data.Product.Base using (_,_)
 open import Function.Base
 open import Relation.Binary.Core