From d666858d9f8d00efd1effcd2770eab926367a320 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 15:22:54 +0100 Subject: [PATCH 1/8] Add new `Bool` action on a `RawMonoid` plus properties --- CHANGELOG.md | 13 +++++++++++++ src/Algebra/Definitions/RawMonoid.agda | 18 +++++++++++++++++- src/Algebra/Properties/Monoid/Mult.agda | 18 ++++++++++++++++-- 3 files changed, 46 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80da9ee48e..a9aee06faa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,3 +26,16 @@ New modules Additions to existing modules ----------------------------- + +* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid: + ```agda + _∧_ : Bool → Carrier → Carrier + _∧′_∙_ : Bool → Carrier → Carrier → Carrier + ``` + +* Properties of the Boolean action on a RawMonoid: + ```agda + ∧-homo-true : true ∧ x ≈ x + -assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x + ∧∙-≗∧+ : b ∧′ x ∙ y ≈ (b ∧ x) + y + ``` diff --git a/src/Algebra/Definitions/RawMonoid.agda b/src/Algebra/Definitions/RawMonoid.agda index cbb095ab40..478671627c 100644 --- a/src/Algebra/Definitions/RawMonoid.agda +++ b/src/Algebra/Definitions/RawMonoid.agda @@ -7,6 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles using (RawMonoid) +open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Vec.Functional as Vector using (Vector) @@ -21,7 +22,7 @@ open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# ) open import Algebra.Definitions.RawMagma rawMagma public ------------------------------------------------------------------------ --- Multiplication by natural number +-- Multiplication by natural number: action of the (0,+)-rawMonoid ------------------------------------------------------------------------ -- Standard definition @@ -65,3 +66,18 @@ suc n ×′ x = n ×′ x + x sum : ∀ {n} → Vector Carrier n → Carrier sum = Vector.foldr _+_ 0# + +------------------------------------------------------------------------ +-- 'Conjunction' with a Boolean: action of the Boolean (true,∧)-rawMonoid +------------------------------------------------------------------------ + +infixr 8 _∧_ + +_∧_ : Bool → Carrier → Carrier +b ∧ x = if b then x else 0# + +-- tail-recursive optimisation +infixl 8 _∧′_∙_ + +_∧′_∙_ : Bool → Carrier → Carrier → Carrier +b ∧′ x ∙ y = if b then x + y else y diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index ce837c8134..320b2c4ef4 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -7,6 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles using (Monoid) +open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) @@ -34,7 +35,7 @@ open import Algebra.Definitions _≈_ -- Definition open import Algebra.Definitions.RawMonoid rawMonoid public - using (_×_) + using (_×_; _∧_; _∧′_∙_) ------------------------------------------------------------------------ -- Properties of _×_ @@ -60,7 +61,7 @@ open import Algebra.Definitions.RawMonoid rawMonoid public ×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x ×-homo-+ x 0 n = sym (+-identityˡ (n × x)) ×-homo-+ x (suc m) n = begin - x + (m ℕ.+ n) × x ≈⟨ +-cong refl (×-homo-+ x m n) ⟩ + x + (m ℕ.+ n) × x ≈⟨ +-congˡ (×-homo-+ x m n) ⟩ x + (m × x + n × x) ≈⟨ sym (+-assoc x (m × x) (n × x)) ⟩ x + m × x + n × x ∎ @@ -78,3 +79,16 @@ open import Algebra.Definitions.RawMonoid rawMonoid public n × x + m × n × x ≈⟨ +-congˡ (×-assocˡ x m n) ⟩ n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨ (suc m ℕ.* n) × x ∎ + +-- _∧_ is homomorphic with respect to _Bool∧_. + +∧-homo-true : ∀ x → true ∧ x ≈ x +∧-homo-true x = refl + +∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x +∧-assocˡ false b x = refl +∧-assocˡ true b x = refl + +∧∙-≗∧+ : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y +∧∙-≗∧+ true x y = refl +∧∙-≗∧+ false x y = sym (+-identityˡ y) From 7d4d3a0db19ae1c5faeb30ae946edbfbe050577b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 16 Aug 2024 07:53:40 +0100 Subject: [PATCH 2/8] response to review comments on draft --- CHANGELOG.md | 4 ++-- src/Algebra/Properties/Monoid/Mult.agda | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a9aee06faa..57bafa0b0b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -36,6 +36,6 @@ Additions to existing modules * Properties of the Boolean action on a RawMonoid: ```agda ∧-homo-true : true ∧ x ≈ x - -assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x - ∧∙-≗∧+ : b ∧′ x ∙ y ≈ (b ∧ x) + y + ∧-assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x + b∧x∙y≈b∧x+y : b ∧′ x ∙ y ≈ (b ∧ x) + y ``` diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index 320b2c4ef4..4f824b087f 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -80,15 +80,15 @@ open import Algebra.Definitions.RawMonoid rawMonoid public n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨ (suc m ℕ.* n) × x ∎ --- _∧_ is homomorphic with respect to _Bool∧_. +-- _∧_ is homomorphic with respect to Bool._∧_. ∧-homo-true : ∀ x → true ∧ x ≈ x -∧-homo-true x = refl +∧-homo-true _ = refl ∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x -∧-assocˡ false b x = refl -∧-assocˡ true b x = refl +∧-assocˡ false _ _ = refl +∧-assocˡ true _ _ = refl -∧∙-≗∧+ : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y -∧∙-≗∧+ true x y = refl -∧∙-≗∧+ false x y = sym (+-identityˡ y) +b∧x∙y≈b∧x+y : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y +b∧x∙y≈b∧x+y true _ _ = refl +b∧x∙y≈b∧x+y false _ y = sym (+-identityˡ y) From eac420ad3ad64149dffdded0e131ccbd319874e5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 10 Jan 2026 19:45:43 +0000 Subject: [PATCH 3/8] reset: `CHANGELOG` --- CHANGELOG.md | 312 +++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 265 insertions(+), 47 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a49ee8d084..e159cc52df 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.2-dev +Version 2.4-dev =============== -The library has been tested using Agda 2.6.4.3. +The library has been tested using Agda 2.8.0. Highlights ---------- @@ -9,8 +9,11 @@ Highlights Bug-fixes --------- -* Removed unnecessary parameter `#-trans : Transitive _#_` from - `Relation.Binary.Reasoning.Base.Apartness`. +* Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`. + +* Fix a typo in `Algebra.Morphism.Construct.DirectProduct`. + +* Fix a typo in `Function.Construct.Constant`. Non-backwards compatible changes -------------------------------- @@ -18,91 +21,306 @@ Non-backwards compatible changes 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. + +* More generally, `Relation.Nullary.Negation.Core` has been reorganised into two + parts: the first concerns definitions and properties of negation considered as + a connective in *minimal logic*; the second making actual use of *ex falso* in + the form of `Data.Empty.⊥-elim`. + +* Refactored usages of `+-∸-assoc 1` to `∸-suc` in: + ```agda + README.Data.Fin.Relation.Unary.Top + Algebra.Properties.Semiring.Binomial + Data.Fin.Subset.Properties + Data.Nat.Binary.Subtraction + Data.Nat.Combinatorics + ``` + +* In `Data.Vec.Relation.Binary.Pointwise.{Inductive,Extensional}`, the types of + `refl`, `sym`, and `trans` have been weakened to allow relations of different + levels to be used. + Deprecated modules ------------------ Deprecated names ---------------- -* In `Data.Vec.Properties`: +* In `Algebra.Properties.CommutativeSemigroup`: + ```agda + interchange ↦ medial + ``` + +* In `Algebra.Properties.Monoid`: + ```agda + ε-comm ↦ ε-central + ``` + +* In `Data.Fin.Properties`: ```agda - ++-assoc _ ↦ ++-assoc-eqFree - ++-identityʳ _ ↦ ++-identityʳ-eqFree - unfold-∷ʳ _ ↦ unfold-∷ʳ-eqFree - ++-∷ʳ _ ↦ ++-∷ʳ-eqFree - ∷ʳ-++ _ ↦ ∷ʳ-++-eqFree - reverse-++ _ ↦ reverse-++-eqFree - ∷-ʳ++ _ ↦ ∷-ʳ++-eqFree - ++-ʳ++ _ ↦ ++-ʳ++-eqFree - ʳ++-ʳ++ _ ↦ ʳ++-ʳ++-eqFree + ¬∀⟶∃¬-smallest ↦ ¬∀⇒∃¬-smallest + ¬∀⟶∃¬- ↦ ¬∀⇒∃¬ + ``` + +* In `Relation.Nullary.Decidable.Core`: + ```agda + ⊤-dec ↦ ⊤? + ⊥-dec ↦ ⊥? + _×-dec_ ↦ _×?_ + _⊎-dec_ ↦ _⊎?_ + _→-dec_ ↦ _→?_ + +* In `Relation.Nullary.Negation`: + ```agda + ∃⟶¬∀¬ ↦ ∃⇒¬∀¬ + ∀⟶¬∃¬ ↦ ∀⇒¬∃¬ + ¬∃⟶∀¬ ↦ ¬∃⇒∀¬ + ∀¬⟶¬∃ ↦ ∀¬⇒¬∃ + ∃¬⟶¬∀ ↦ ∃¬⇒¬∀ ``` New modules ----------- -* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`: - ```agda - Algebra.Properties.IdempotentCommutativeMonoid +* `Algebra.Construct.Sub.Group` for the definition of subgroups. + +* `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules. + +* `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. + +* `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint. + +* Various additions over non-empty lists: + ``` + Data.List.NonEmpty.Relation.Binary.Pointwise + Data.List.NonEmpty.Relation.Unary.Any + Data.List.NonEmpty.Membership.Propositional + Data.List.NonEmpty.Membership.Setoid ``` +* `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`, + and a function `f : A → B`, construct the canonical `IsRelMonomorphism` + between `_∼_ on f` and `_∼_`, witnessed by `f` itself. + Additions to existing modules ----------------------------- -* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid: +* In `Algebra.Bundles`: ```agda - _∧_ : Bool → Carrier → Carrier - _∧′_∙_ : Bool → Carrier → Carrier → Carrier + record BooleanSemiring _ _ : Set _ + record BooleanRing _ _ : Set _ ``` -* In `Algebra.Properties.Monoid.Mult` properties of the Boolean action on a RawMonoid: +* In `Algebra.Consequences.Propositional`: ```agda - ∧-homo-true : true ∧ x ≈ x - ∧-assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x - b∧x∙y≈b∧x+y : b ∧′ x ∙ y ≈ (b ∧ x) + y - ``` + binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ → + ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + identity⇒central : Identity e _∙_ → Central _∙_ e + zero⇒central : Zero e _∙_ → Central _∙_ e + ``` + +* In `Algebra.Consequences.Setoid`: + ```agda + sel⇒idem : Selective _∙_ → Idempotent _∙_ + binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → + ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + identity⇒central : Identity e _∙_ → Central _∙_ e + zero⇒central : Zero e _∙_ → Central _∙_ e + ``` + +* In `Algebra.Definitions`: + ```agda + Central : Op₂ A → A → Set _ + ``` + +* 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 + transpose[i,j,j]≡i : (i j : Fin n) → transpose i j j ≡ i + transpose[i,j,i]≡j : (i j : Fin n) → transpose i j i ≡ j + transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k + ``` + +* In `Data.Fin.Properties`: + ```agda + ≡-irrelevant : Irrelevant {A = Fin n} _≡_ + ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq + ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl + ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j + inject-< : inject j < i + + record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where + constructor least + field + witness : Fin n + example : P witness + minimal : ∀ {j} → .(j < witness) → ¬ P j + + search-least⟨_⟩ : Decidable P → Π[ ∁ P ] ⊎ Least⟨ P ⟩ + search-least⟨¬_⟩ : Decidable P → Π[ P ] ⊎ Least⟨ ∁ P ⟩ + ``` + +* In `Data.List.NonEmpty.Relation.Unary.All`: + ``` + map : P ⊆ Q → All P xs → All Q xs + ``` + +* 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.Product.Properties`: + ```agda + swap-↔ : (A × B) ↔ (B × A) + _,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D) + ``` + +* In `Data.Vec.Properties`: + ```agda + map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) → + map f (removeAt xs i) ≡ removeAt (map f xs) i + + updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) → + updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f) + + truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) → + truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys) + + truncate-zipWith-truncate : (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o) (xs : Vec A o) (ys : Vec B n) → + truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡ + zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys) + + truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) → + updateAt (truncate m≤n xs) i f ≡ + truncate m≤n (updateAt xs (inject≤ i m≤n) f) + + updateAt-truncate : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) → + updateAt (truncate (m≤m+n m n) xs) i f ≡ + truncate (m≤m+n m n) (updateAt xs (inject≤ i (m≤m+n m n)) f) + + map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) → + map f (truncate m≤n xs) ≡ truncate m≤n (map f xs) + + padRight-lookup : (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i + + padRight-map : (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) + + padRight-zipWith : (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) → + zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys) + + padRight-zipWith₁ : (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) → + zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡ + padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys)) + + padRight-take : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs + + padRight-drop : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a + + padRight-updateAt : (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) → + updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f) + ``` -* In `Data.List.Relation.Unary.All`: +* In `Relation.Binary.Construct.Add.Extrema.NonStrict`: ```agda - search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs + ≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_ + ≤±-respʳ-≡ : _≤±_ Respectsʳ _≡_ + ≤±-resp-≡ : _≤±_ Respects₂ _≡_ + ≤±-respˡ-≈± : _≤_ Respectsˡ _≈_ → _≤±_ Respectsˡ _≈±_ + ≤±-respʳ-≈± : _≤_ Respectsʳ _≈_ → _≤±_ Respectsʳ _≈±_ + ≤±-resp-≈± : _≤_ Respects₂ _≈_ → _≤±_ Respects₂ _≈±_ ``` -* In `Data.List.Relation.Binary.Equality.Setoid`: +* In `Relation.Binary.Construct.Add.Infimum.NonStrict`: ```agda - ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs - ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs + ≤₋-respˡ-≡ : _≤₋_ Respectsˡ _≡_ + ≤₋-respʳ-≡ : _≤₋_ Respectsʳ _≡_ + ≤₋-resp-≡ : _≤₋_ Respects₂ _≡_ + ≤₋-respˡ-≈₋ : _≤_ Respectsˡ _≈_ → _≤₋_ Respectsˡ _≈₋_ + ≤₋-respʳ-≈₋ : _≤_ Respectsʳ _≈_ → _≤₋_ Respectsʳ _≈₋_ + ≤₋-resp-≈₋ : _≤_ Respects₂ _≈_ → _≤₋_ Respects₂ _≈₋_ ``` -* In `Data.List.Relation.Binary.Pointwise`: +* In `Relation.Binary.Construct.Add.Extrema.Supremum.NonStrict`: ```agda - ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) - ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) + ≤⁺-respˡ-≡ : _≤⁺_ Respectsˡ _≡_ + ≤⁺-respʳ-≡ : _≤⁺_ Respectsʳ _≡_ + ≤⁺-resp-≡ : _≤⁺_ Respects₂ _≡_ + ≤⁺-respˡ-≈⁺ : _≤_ Respectsˡ _≈_ → _≤⁺_ Respectsˡ _≈⁺_ + ≤⁺-respʳ-≈⁺ : _≤_ Respectsʳ _≈_ → _≤⁺_ Respectsʳ _≈⁺_ + ≤⁺-resp-≈⁺ : _≤_ Respects₂ _≈_ → _≤⁺_ Respects₂ _≈⁺_ ``` -* New lemmas in `Data.Nat.Properties`: adjunction between `suc` and `pred` +* In `Data.Vec.Relation.Binary.Pointwise.Inductive` ```agda - suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n - m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n + irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m}) + antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {m n} → + Antisym P Q R → Antisym (Pointwise P {m}) (Pointwise Q {n}) (Pointwise R) ``` -* New lemma in `Data.Vec.Properties`: +* In `Data.Vec.Relation.Binary.Pointwise.Extensional` ```agda - map-concat : map f (concat xss) ≡ concat (map (map f) xss) + antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {n} → + Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R) ``` -* In `Data.Vec.Relation.Binary.Equality.DecPropositional`: +* In `Relation.Nullary.Negation.Core` ```agda - _≡?_ : DecidableEquality (Vec A n) + ¬¬-η : A → ¬ ¬ A + contradiction′ : ¬ A → A → Whatever ``` -* In `Relation.Nullary.Decidable`: +* In `Relation.Unary` ```agda - does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? - does-≡ : (a? b? : Dec A) → does a? ≡ does b? + ⟨_⟩⊢_ : (A → B) → Pred A ℓ → Pred B _ + [_]⊢_ : (A → B) → Pred A ℓ → Pred B _ ``` -* In `Relation.Nullary.Properties`: +* In `System.Random`: ```agda - map : P ≐ Q → Decidable P → Decidable Q - does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q? - does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′ + randomIO : IO Bool + randomRIO : RandomRIO {A = Bool} _≤_ ``` From 38117b8d383f3cecef5cda2210f5b17113f6c6db Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 11 Jan 2026 12:24:15 +0000 Subject: [PATCH 4/8] restore: new `CHANGELOG` entries --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e159cc52df..3a49b0e0be 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -149,12 +149,25 @@ Additions to existing modules Central : Op₂ A → A → Set _ ``` +* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid: + ```agda + _∧_ : Bool → Carrier → Carrier + _∧′_∙_ : Bool → Carrier → Carrier → Carrier + ``` + * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: ```agda ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ ⊕-∧-booleanRing : BooleanRing _ _ ``` +* In `Algebra.Properties.Monoid.Mult` properties of the Boolean action on a RawMonoid: + ```agda + ∧-homo-true : true ∧ x ≈ x + ∧-assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x + b∧x∙y≈b∧x+y : b ∧′ x ∙ y ≈ (b ∧ x) + y + ``` + * In `Algebra.Properties.RingWithoutOne`: ```agda [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y From 2adec9721dcef175db66cfdf2906987787a2effb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 11 Jan 2026 12:53:03 +0000 Subject: [PATCH 5/8] change: notation --- src/Algebra/Definitions/RawMonoid.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Definitions/RawMonoid.agda b/src/Algebra/Definitions/RawMonoid.agda index 4680cc70f4..266654f7c3 100644 --- a/src/Algebra/Definitions/RawMonoid.agda +++ b/src/Algebra/Definitions/RawMonoid.agda @@ -69,16 +69,16 @@ sum : ∀ {n} → Vector Carrier n → Carrier sum = Vector.foldr _+_ 0# ------------------------------------------------------------------------ --- 'Conjunction' with a Boolean: action of the Boolean (true,∧)-rawMonoid +-- 'Guard' with a Boolean: action of the Boolean (true,∧)-rawMonoid ------------------------------------------------------------------------ -infixr 8 _∧_ +infixr 8 _?>₀_ -_∧_ : Bool → Carrier → Carrier -b ∧ x = if b then x else 0# +_?>₀_ : Bool → Carrier → Carrier +b ?>₀ x = if b then x else 0# --- tail-recursive optimisation -infixl 8 _∧′_∙_ +-- accumulator optimisation +infixl 8 _?>_∙_ -_∧′_∙_ : Bool → Carrier → Carrier → Carrier -b ∧′ x ∙ y = if b then x + y else y +_?>_∙_ : Bool → Carrier → Carrier → Carrier +b ?> x ∙ y = if b then x + y else y From 94f8e981da1b68d7b4c9064e82ea6417d733581f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 11 Jan 2026 12:53:32 +0000 Subject: [PATCH 6/8] refactor: use new notation, plus add new lemma --- CHANGELOG.md | 13 +++++++------ src/Algebra/Properties/Monoid/Mult.agda | 26 ++++++++++++++----------- 2 files changed, 22 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3a49b0e0be..b2f294363d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -151,8 +151,8 @@ Additions to existing modules * In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid: ```agda - _∧_ : Bool → Carrier → Carrier - _∧′_∙_ : Bool → Carrier → Carrier → Carrier + _?>₀_ : Bool → Carrier → Carrier + _?>_∙_ : Bool → Carrier → Carrier → Carrier ``` * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: @@ -163,10 +163,11 @@ Additions to existing modules * In `Algebra.Properties.Monoid.Mult` properties of the Boolean action on a RawMonoid: ```agda - ∧-homo-true : true ∧ x ≈ x - ∧-assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x - b∧x∙y≈b∧x+y : b ∧′ x ∙ y ≈ (b ∧ x) + y - ``` + ?>₀-homo-true : true ?>₀ x ≈ x + ?>₀-assocˡ : b ?>₀ b′ ?>₀ x ≈ (b ∧ b′) ?>₀ x + b?>x∙y≈b?>₀x+y : b ?> x ∙ y ≈ (b ?>₀ x) + y + b?>₀x≈b?>x+0 : b ?>₀ x ≈ b ?> x ∙ 0# + ``` * In `Algebra.Properties.RingWithoutOne`: ```agda diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index 4f824b087f..6366f84913 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -7,7 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles using (Monoid) -open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) +open import Data.Bool.Base as Bool using (true; false; _∧_) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) @@ -35,7 +35,7 @@ open import Algebra.Definitions _≈_ -- Definition open import Algebra.Definitions.RawMonoid rawMonoid public - using (_×_; _∧_; _∧′_∙_) + using (_×_; _?>₀_; _?>_∙_) ------------------------------------------------------------------------ -- Properties of _×_ @@ -80,15 +80,19 @@ open import Algebra.Definitions.RawMonoid rawMonoid public n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨ (suc m ℕ.* n) × x ∎ --- _∧_ is homomorphic with respect to Bool._∧_. +-- _?>₀_ is homomorphic with respect to Bool._∧_. -∧-homo-true : ∀ x → true ∧ x ≈ x -∧-homo-true _ = refl +?>₀-homo-true : ∀ x → true ?>₀ x ≈ x +?>₀-homo-true _ = refl -∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x -∧-assocˡ false _ _ = refl -∧-assocˡ true _ _ = refl +?>₀-assocˡ : ∀ b b′ x → b ?>₀ b′ ?>₀ x ≈ (b ∧ b′) ?>₀ x +?>₀-assocˡ false _ _ = refl +?>₀-assocˡ true _ _ = refl -b∧x∙y≈b∧x+y : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y -b∧x∙y≈b∧x+y true _ _ = refl -b∧x∙y≈b∧x+y false _ y = sym (+-identityˡ y) +b?>x∙y≈b?>₀x+y : ∀ b x y → b ?> x ∙ y ≈ b ?>₀ x + y +b?>x∙y≈b?>₀x+y true _ _ = refl +b?>x∙y≈b?>₀x+y false _ y = sym (+-identityˡ y) + +b?>₀x≈b?>x+0 : ∀ b x → b ?>₀ x ≈ b ?> x ∙ 0# +b?>₀x≈b?>x+0 true _ = sym (+-identityʳ _) +b?>₀x≈b?>x+0 false x = refl From 08ecae50c5e0e8e7eb52e9d217332d91837d90c2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 11 Jan 2026 12:55:45 +0000 Subject: [PATCH 7/8] refactor: tweak notation --- CHANGELOG.md | 2 +- src/Algebra/Properties/Monoid/Mult.agda | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b2f294363d..2e91a89852 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -166,7 +166,7 @@ Additions to existing modules ?>₀-homo-true : true ?>₀ x ≈ x ?>₀-assocˡ : b ?>₀ b′ ?>₀ x ≈ (b ∧ b′) ?>₀ x b?>x∙y≈b?>₀x+y : b ?> x ∙ y ≈ (b ?>₀ x) + y - b?>₀x≈b?>x+0 : b ?>₀ x ≈ b ?> x ∙ 0# + b?>₀x≈b?>x∙0 : b ?>₀ x ≈ b ?> x ∙ 0# ``` * In `Algebra.Properties.RingWithoutOne`: diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index 6366f84913..c1ba6515dd 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -93,6 +93,6 @@ b?>x∙y≈b?>₀x+y : ∀ b x y → b ?> x ∙ y ≈ b ?>₀ x + y b?>x∙y≈b?>₀x+y true _ _ = refl b?>x∙y≈b?>₀x+y false _ y = sym (+-identityˡ y) -b?>₀x≈b?>x+0 : ∀ b x → b ?>₀ x ≈ b ?> x ∙ 0# -b?>₀x≈b?>x+0 true _ = sym (+-identityʳ _) -b?>₀x≈b?>x+0 false x = refl +b?>₀x≈b?>x∙0 : ∀ b x → b ?>₀ x ≈ b ?> x ∙ 0# +b?>₀x≈b?>x∙0 true _ = sym (+-identityʳ _) +b?>₀x≈b?>x∙0 false x = refl From 2f104b663026bb294cfcd92538b11e1d612ce1d3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 11 Jan 2026 18:31:05 +0000 Subject: [PATCH 8/8] refactor: proof following Jacques' suggestion --- src/Algebra/Properties/Monoid/Mult.agda | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index c1ba6515dd..b2dd011fdd 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -7,13 +7,14 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles using (Monoid) + +module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where + open import Data.Bool.Base as Bool using (true; false; _∧_) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero) open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) -module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where - -- View of the monoid operator as addition open Monoid M renaming @@ -27,9 +28,9 @@ open Monoid M ; ε to 0# ) -open import Relation.Binary.Reasoning.Setoid setoid - open import Algebra.Definitions _≈_ +open import Algebra.Properties.Semigroup semigroup +open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ -- Definition @@ -60,10 +61,7 @@ open import Algebra.Definitions.RawMonoid rawMonoid public ×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x ×-homo-+ x 0 n = sym (+-identityˡ (n × x)) -×-homo-+ x (suc m) n = begin - x + (m ℕ.+ n) × x ≈⟨ +-congˡ (×-homo-+ x m n) ⟩ - x + (m × x + n × x) ≈⟨ sym (+-assoc x (m × x) (n × x)) ⟩ - x + m × x + n × x ∎ +×-homo-+ x (suc m) n = sym (uv≈w⇒xu∙v≈xw (sym (×-homo-+ x m n)) x) ×-idem : ∀ {c} → _+_ IdempotentOn c → ∀ n → .{{_ : NonZero n}} → n × c ≈ c