Refactor Algebra.Solver.*Monoid (#2407)

* refactor `Solver` infrastructure

* refactor `Solver` infrastructure

* tighten imports and some `with`

* tidy up `Solver.Monoid`

* refactor `Algebra.Solver.*Monoid`

* regularise vocabulary: deprecations

* `variable`s for `Algebra.Solver.Ring`

* tweaks

* forgot to add `Expression` module

* refactor: use existing lemma

* fixed deprecations to `v2.2`

* v2.2 `CHANGELOG`

* use `zipWith`!

* remove dependency on `Data.Nat.GeneralisedArithmetic.fold`

* simplify `import` dependencies

* refactor: tweaks

* change `Level` parameterisation of `NormalAPI`

* clarify exports from `module R`?

* deprecations

* knock-on effects

* deprecations

* fixed exports of `Normal` form instantiations

* fixed exports of `Solver`

* fixed deprecations in `CHANGELOG`

* note on import strategy in `CHANGELOG`

* name of `Solver` module

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -30,6 +30,28 @@ Deprecated names
   ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
   ```
 
+* In `Algebra.Solver.CommutativeMonoid`:
+  ```agda
+  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
+  distr              ↦  Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙
+  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.Monoid`:
+  ```agda
+  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
+  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree
@@ -51,9 +73,28 @@ New modules
   Algebra.Properties.IdempotentCommutativeMonoid
   ```
 
+* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
+  a single `Solver` 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.Solver
+  ```
+
+  NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
+
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Solver.Ring`
+  ```agda
+  Env : ℕ → Set _
+  Env = Vec Carrier
+ ```
+
 * In `Data.List.Properties`:
   ```agda
   product≢0 : All NonZero ns → NonZero (product ns)

src/Algebra/Solver/CommutativeMonoid.agda

@@ -8,196 +8,40 @@
 
 {-# 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.Solver as Solver
 
-open import Function.Base using (_∘_)
-
-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
+open CommutativeMonoid M using (monoid)
 
 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.
+  module N = Normal M
 
-⟦_⟧ : 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
+open N public
+  renaming (correct to normalise-correct)
 
 ------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty bag.
-
-empty : Normal n
-empty = replicate _ 0
-
--- A singleton bag.
+-- Proof procedures
 
-sg : (i : Fin n) → Normal n
-sg zero    = 1 ∷ empty
-sg (suc i) = 0 ∷ sg i
+open Solver monoid (record { N }) public
 
--- The composition of normal forms.
-
-_•_  : (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 : 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 _ _))
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- 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₂ ⟧ ρ
-  ∎
-
-------------------------------------------------------------------------
--- "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."
+#-}