Refactor Algebra.Solver.*Monoid

CHANGELOG.md

@@ -21,8 +21,42 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Solver.CommutativeMonoid`:
+  ```agda
+  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
+  ```
+
+* In `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
+  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
+  ```
+
+* In `Algebra.Solver.Monoid`:
+  ```agda
+  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
+  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
+  ```
+
 New modules
 -----------
 
+* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
+  a single `Tactic` module API based on the existing `Expr`, and
+  a common `Normal`-form API:
+  ```agda
+  Algebra.Solver.CommutativeMonoid.Normal
+  Algebra.Solver.IdempotentCommutativeMonoid.Normal
+  Algebra.Solver.Monoid.Expression
+  Algebra.Solver.Monoid.Normal
+  Algebra.Solver.Monoid.Tactic
+  ```
+
 Additions to existing modules
 -----------------------------
+
+* In `Algebra.Solver.Ring`
+  ```agda
+  Env : ℕ → Set _
+  Env = Vec Carrier
+  ```

src/Algebra/Solver/CommutativeMonoid.agda

@@ -8,196 +8,37 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (CommutativeMonoid)
 
-module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where
+module Algebra.Solver.CommutativeMonoid {c ℓ} (M : CommutativeMonoid c ℓ) where
 
-open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Nat.GeneralisedArithmetic using (fold)
-open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
+import Algebra.Solver.CommutativeMonoid.Normal as Normal
+import Algebra.Solver.Monoid.Tactic as Tactic
 
-open import Function.Base using (_∘_)
+open CommutativeMonoid M using (monoid)
 
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Binary.Reflection as Reflection
-import Relation.Nullary.Decidable as Dec
-import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
-
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable as Dec using (Dec)
-
-open CommutativeMonoid M
-open ≈-Reasoning setoid
-
-private
-  variable
-    n : ℕ
-
-------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-infixr 10 _•_
-
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
-
--- An environment contains one value for every variable.
-
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
-
-⟦_⟧ : Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
 
 ------------------------------------------------------------------------
 -- Normal forms
 
--- A normal form is a vector of multiplicities (a bag).
-
-Normal : ℕ → Set
-Normal n = Vec ℕ n
-
--- The semantics of a normal form.
-
-⟦_⟧⇓ : Normal n → Env n → Carrier
-⟦ []    ⟧⇓ _ = ε
-⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n
-
-------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty bag.
-
-empty : Normal n
-empty = replicate _ 0
-
--- A singleton bag.
-
-sg : (i : Fin n) → Normal n
-sg zero    = 1 ∷ empty
-sg (suc i) = 0 ∷ sg i
-
--- The composition of normal forms.
-
-_•_  : (v w : Normal n) → Normal n
-[]      • []      = []
-(l ∷ v) • (m ∷ w) = l + m ∷ v • w
+open module N = Normal M public
+  renaming (correct to normalise-correct)
 
 ------------------------------------------------------------------------
--- Correctness of the constructions on normal forms
-
--- The empty bag stands for the unit ε.
-
-empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
-empty-correct [] = refl
-empty-correct (a ∷ ρ) = empty-correct ρ
+-- Tactic
 
--- The singleton bag stands for a single variable.
+open Tactic monoid (record { N }) public
 
-sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
-sg-correct zero (x ∷ ρ) = begin
-    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
-    x ∙ ε              ≈⟨ identityʳ _ ⟩
-    x                  ∎
-sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
-
--- Normal form composition corresponds to the composition of the monoid.
-
-comp-correct : (v w : Normal n) (ρ : Env n) →
-              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
-comp-correct [] [] ρ =  sym (identityˡ _)
-comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ)
-  where
-    flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
-    flip12 a b c = begin
-        a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
-        (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
-        (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
-        b ∙ (a ∙ c)  ∎
-    lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) →
-      fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m
-    lemma zero zero p = p
-    lemma zero (suc m) p = trans (∙-congˡ (lemma zero m p)) (flip12 _ _ _)
-    lemma (suc l) m p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _))
 
 ------------------------------------------------------------------------
--- Normalization
-
--- A normaliser.
-
-normalise : Expr n → Normal n
-normalise (var x)   = sg x
-normalise id        = empty
-normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct : (e : Expr n) (ρ : Env n) →
-    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x)   ρ = sg-correct x ρ
-normalise-correct id        ρ = empty-correct ρ
-normalise-correct (e₁ ⊕ e₂) ρ =  begin
-
-    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
-
-    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-
-    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
-  ∎
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
-
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
-
-_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
-  where open Pointwise
-
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
-
-prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
-
--- This procedure can be combined with from-just.
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
-prove _ e₁ e₂ = from-just (prove′ e₁ e₂)
+-- Version 2.2
 
--- prove : ∀ n (es : Expr n × Expr n) →
---         From-just (uncurry prove′ es)
--- prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead."
+#-}

src/Algebra/Solver/CommutativeMonoid/Normal.agda

@@ -0,0 +1,135 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Normal forms in commutative monoids
+--
+-- Adapted from Algebra.Solver.Monoid.Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (CommutativeMonoid)
+
+module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where
+
+import Algebra.Properties.CommutativeSemigroup as CSProperties
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
+open import Data.Nat.GeneralisedArithmetic using (fold)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
+import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
+open import Relation.Binary.Definitions using (DecidableEquality)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Relation.Nullary.Decidable as Dec
+
+open CommutativeMonoid M
+open CSProperties commutativeSemigroup using (x∙yz≈y∙xz)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression rawMonoid public
+  hiding (NormalAPI)
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of multiplicities (a bag).
+
+Normal : ℕ → Set
+Normal n = Vec ℕ n
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : Normal n → Env n → Carrier
+⟦ []    ⟧⇓ _       = ε
+⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (Normal n)
+nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
+  where open Pointwise using (Pointwise-≡↔≡; decidable)
+
+------------------------------------------------------------------------
+-- Constructions on normal forms
+
+-- The empty bag.
+
+empty : Normal n
+empty = replicate _ 0
+
+-- A singleton bag.
+
+sg : (i : Fin n) → Normal n
+sg zero    = 1 ∷ empty
+sg (suc i) = 0 ∷ sg i
+
+-- The composition of normal forms.
+infixr 10 _•_
+
+_•_  : (v w : Normal n) → Normal n
+[]      • []      = []
+(l ∷ v) • (m ∷ w) = l + m ∷ v • w
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty bag stands for the unit ε.
+
+empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+empty-correct [] = refl
+empty-correct (a ∷ ρ) = empty-correct ρ
+
+-- The singleton bag stands for a single variable.
+
+sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
+sg-correct zero (x ∷ ρ) = begin
+    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
+    x ∙ ε              ≈⟨ identityʳ _ ⟩
+    x                  ∎
+sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+comp-correct : ∀ v w (ρ : Env n) →
+               ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+comp-correct [] [] _ =  sym (identityˡ _)
+comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ)
+  where
+  lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) →
+          fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m
+  lemma zero    zero    p = p
+  lemma zero    (suc m) p = trans (∙-congˡ (lemma zero m p)) (x∙yz≈y∙xz _ _ _)
+  lemma (suc l) m       p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _))
+
+------------------------------------------------------------------------
+-- Normalization
+
+-- A normaliser.
+
+normalise : Expr n → Normal n
+normalise (var x)   = sg x
+normalise id        = empty
+normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
+
+-- The normaliser preserves the semantics of the expression.
+
+correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+correct (var x)   ρ = sg-correct x ρ
+correct id        ρ = empty-correct ρ
+correct (e₁ ⊕ e₂) ρ = begin
+  ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
+    ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
+  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
+    ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
+  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+    ∎