Merge branch 'master' into updating-pr-1945

Author: jamesmckinna

.github/workflows/ci-ubuntu.yml

@@ -48,8 +48,8 @@ on:
 ########################################################################
 
 env:
-  GHC_VERSION: 9.10.1
-  CABAL_VERSION: 3.12.1.0
+  GHC_VERSION: 9.12.2
+  CABAL_VERSION: 3.16.0.0
   CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
   AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc
@@ -76,11 +76,12 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=ef912c68fd329ad3046d156e3c1a70a7fec19ba1" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=3d04bacca842729f9c0869b9287256321b5f450f" >> "${GITHUB_ENV}";
+              # Andreas, 2025-10-07: 3d04bacca842729f9c0869b9287256321b5f450f is tags/v2.8.0
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.8.0-rc3" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 
@@ -148,7 +149,7 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout stdlib
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Test stdlib
         run: |

CHANGELOG.md

@@ -11,6 +11,8 @@ Bug-fixes
 
 * Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`.
 
+* Fix a typo in `Algebra.Morphism.Construct.DirectProduct`.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -20,6 +22,9 @@ Minor improvements
 * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
+  Furthermore, because the *eager* insertion of implicit arguments during type
+  inference interacts badly with `contradiction`, we introduce an explicit name
+  `contradiction′` for its `flip`ped version.
 
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
@@ -44,20 +49,61 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Properties.BooleanRing`.
+
+* `Algebra.Properties.BooleanSemiring`.
+
+* `Algebra.Properties.CommutativeRing`.
+
+* `Algebra.Properties.Semiring`.
+
 * `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
 * `Data.Vec.Functional.Algebra(.{Base|Properties})` - structures and bundles about functional vectors and modules.
 
+* `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
+
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles`:
+  ```agda
+  record BooleanSemiring _ _ : Set _
+  record BooleanRing _ _     : Set _
+  ```
+
+* In `Algebra.Consequences.Propositional`:
+  ```agda
+  binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ →
+    ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  ```
+
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  binomial-expansion : Congruent₂ _∙_  → Associative _∙_ → _◦_ DistributesOver _∙_ →
+    ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  ```
+
+* In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`:
+  ```agda
+  ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
+  ⊕-∧-booleanRing   : BooleanRing _ _
+  ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
   ```
 
+* In `Algebra.Structures`:
+  ```agda
+  record IsBooleanSemiring + * 0# 1# : Set _
+  record IsBooleanRing + * - 0# 1# : Set _
+  ```
+  NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
@@ -74,10 +120,18 @@ Additions to existing modules
   ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   ```
 
+* In `Data.Nat.ListAction.Properties`
+  ```agda
+  *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)
+  *-distribʳ-sum : ∀ m ns → sum ns * m ≡ sum (map (_* m) ns)
+  ^-distribʳ-product : ∀ m ns → product ns ^ m ≡ product (map (_^ m) ns)
+  ```
+
 * In `Data.Nat.Properties`:
   ```agda
   ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
   ```
 
 * In `Data.Vec.Properties`:
@@ -103,5 +157,12 @@ Additions to existing modules
 
 * In `Relation.Nullary.Negation.Core`
   ```agda
-  ¬¬-η : A → ¬ ¬ A
+  ¬¬-η           : A → ¬ ¬ A
+  contradiction′ : ¬ A → A → Whatever
+  ```
+
+* In `System.Random`:
+  ```agda
+  randomIO : IO Bool
+  randomRIO : RandomRIO {A = Bool} _≤_
   ```

GenerateEverything.hs

@@ -59,6 +59,8 @@ unsafeModules = map modToFile
   , "Debug.Trace"
   , "Effect.Monad.IO"
   , "Effect.Monad.IO.Instances"
+  , "Effect.Monad.Random"
+  , "Effect.Monad.Random.Instances"
   , "Foreign.Haskell"
   , "Foreign.Haskell.Coerce"
   , "Foreign.Haskell.Either"

src/Algebra/Bundles.agda

@@ -921,6 +921,41 @@ record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; rawMonoid to *-rawMonoid
     )
 
+record BooleanSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier           : Set c
+    _≈_               : Rel Carrier ℓ
+    _+_               : Op₂ Carrier
+    _*_               : Op₂ Carrier
+    0#                : Carrier
+    1#                : Carrier
+    isBooleanSemiring : IsBooleanSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsBooleanSemiring isBooleanSemiring public
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma;  *-magma;  *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; rawNearSemiring ; rawSemiring; nearSemiring
+    ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+    )
+
+  *-idempotentMonoid :  IdempotentMonoid c ℓ
+  *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid }
+
+  open IdempotentMonoid *-idempotentMonoid public
+    using () renaming (band to *-band)
+
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 1 element
 ------------------------------------------------------------------------
@@ -1106,7 +1141,10 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   ring : Ring _ _
   ring = record { isRing = isRing }
 
-  open Ring ring public using (_≉_; rawRing; +-invertibleMagma; +-invertibleUnitalMagma; +-group; +-abelianGroup)
+  open Ring ring public
+    using (_≉_; rawRing
+          ; +-invertibleMagma; +-invertibleUnitalMagma
+          ; +-group; +-abelianGroup)
 
   commutativeSemiring : CommutativeSemiring _ _
   commutativeSemiring =
@@ -1124,6 +1162,47 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; commutativeSemiringWithoutOne
     )
 
+
+record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    _+_           : Op₂ Carrier
+    _*_           : Op₂ Carrier
+    -_            : Op₁ Carrier
+    0#            : Carrier
+    1#            : Carrier
+    isBooleanRing : IsBooleanRing _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsBooleanRing isBooleanRing public
+    using (isCommutativeRing; *-idem)
+
+  open IsCommutativeRing isCommutativeRing public
+
+  commutativeRing : CommutativeRing _ _
+  commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+  open CommutativeRing commutativeRing public
+    using
+    (_≉_; rawRing
+    ; +-invertibleMagma; +-invertibleUnitalMagma
+    ; +-group; +-abelianGroup
+    ; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero; semiring
+    ; commutativeSemiringWithoutOne; commutativeSemiring
+    ; ring
+    )
+
+
 ------------------------------------------------------------------------
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------

src/Algebra/Consequences/Propositional.agda

@@ -42,6 +42,7 @@ open Base public
   ; subst∧comm⇒sym
   ; wlog
   ; sel⇒idem
+  ; binomial-expansion
 -- plus all the deprecated versions of the above
   ; comm+assoc⇒middleFour
   ; identity+middleFour⇒assoc
@@ -101,6 +102,15 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
   comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
   comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
 
+module _ {_∙_ _◦_ : Op₂ A}
+         (∙-assoc : Associative _∙_)
+         (distrib : _◦_ DistributesOver _∙_)
+         where
+
+  binomial-expansion : ∀ w x y z →
+             ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
+
 ------------------------------------------------------------------------
 -- Selectivity
 

src/Algebra/Consequences/Setoid.agda

@@ -292,6 +292,21 @@ module _ {_∙_ _◦_ : Op₂ A}
     (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
     (x ∙ y) ◦ (x ∙ z)              ∎
 
+module _ {_∙_ _◦_ : Op₂ A}
+         (∙-cong  : Congruent₂ _∙_)
+         (∙-assoc : Associative _∙_)
+         (distrib@(distribˡ , distribʳ) : _◦_ DistributesOver _∙_)
+         where
+
+  binomial-expansion : ∀ w x y z →
+             ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  binomial-expansion w x y z = begin
+    (w ∙ x) ◦ (y ∙ z)                         ≈⟨ distribʳ _ _ _ ⟩
+    (w ◦ (y ∙ z)) ∙ (x ◦ (y ∙ z))             ≈⟨ ∙-cong (distribˡ _ _ _) (distribˡ _ _ _) ⟩
+    ((w ◦ y) ∙ (w ◦ z)) ∙ ((x ◦ y) ∙ (x ◦ z)) ≈⟨ ∙-assoc _ _ _ ⟨
+    (((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z) ∎
+
+
 ------------------------------------------------------------------------
 -- Ring-like structures
 

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -6,30 +6,31 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice.Bundles
+open import Algebra.Lattice.Bundles using (BooleanAlgebra)
 
 module Algebra.Lattice.Properties.BooleanAlgebra
-  {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
+  {c ℓ} (booleanAlgebra : BooleanAlgebra c ℓ)
   where
 
-open BooleanAlgebra B
+open import Algebra.Bundles
+  using (CommutativeSemiring; CommutativeRing; BooleanRing)
+open import Algebra.Core using (Op₂)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _$_; _⟨_⟩_)
+open import Function.Bundles using (_⇔_; module Equivalence)
 
-import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties
-open import Algebra.Core using (Op₁; Op₂)
+open BooleanAlgebra booleanAlgebra
 open import Algebra.Structures _≈_
 open import Algebra.Definitions _≈_
 open import Algebra.Consequences.Setoid setoid
-open import Algebra.Bundles using (CommutativeSemiring; CommutativeRing)
 open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Function.Base using (id; _$_; _⟨_⟩_)
-open import Function.Bundles using (_⇔_; module Equivalence)
-open import Data.Product.Base using (_,_)
+
 
 ------------------------------------------------------------------------
 -- Export properties from distributive lattices
 
-open DistribLatticeProperties distributiveLattice public
+open import Algebra.Lattice.Properties.DistributiveLattice distributiveLattice public
 
 ------------------------------------------------------------------------
 -- The dual construction is also a boolean algebra
@@ -529,6 +530,12 @@ module XorRing
     { isCommutativeRing = ⊕-∧-isCommutativeRing
     }
 
+  ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
+  ⊕-∧-isBooleanRing = record
+    { isCommutativeRing = ⊕-∧-isCommutativeRing ; *-idem = ∧-idem }
+
+  ⊕-∧-booleanRing : BooleanRing _ _
+  ⊕-∧-booleanRing = record { isBooleanRing = ⊕-∧-isBooleanRing }
 
 infixl 6 _⊕_
 

src/Algebra/Morphism/Construct/DirectProduct.agda

@@ -133,7 +133,7 @@ module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where
     module N = RawMonoid N
 
   module _ {refl : Reflexive M._≈_} where
-    proj₁ = Proj₁.isMonoidHomomorphism M M refl
+    proj₁ = Proj₁.isMonoidHomomorphism M N refl
 
   module _ {refl : Reflexive N._≈_} where
     proj₂ = Proj₂.isMonoidHomomorphism M N refl