Refactor Algebra.Solver.*Monoid (further!)

src/Algebra/Solver/CommutativeMonoid.agda

@@ -8,196 +8,43 @@
 
 {-# 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
+-- Expressions and Normal forms
 
--- An environment contains one value for every variable.
+open module N = Normal M public
+-- for deprecation below
+  renaming (∙-homo to comp-correct; correct to normalise-correct)
+  hiding (module Expr)
 
-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₂ ⟧ ρ
+open N.Expr public
+-- for backwards compatibility
+  renaming (‵var to var; ‵ε to id; _‵∙_ to _⊕_)
 
 ------------------------------------------------------------------------
--- Normal forms
-
--- A normal form is a vector of multiplicities (a bag).
+-- Tactic
 
-Normal : ℕ → Set
-Normal n = Vec ℕ n
+open Tactic monoid normal public
 
--- 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
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- 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 _ _))
-
-------------------------------------------------------------------------
--- 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."
+#-}

src/Algebra/Solver/CommutativeMonoid/Normal.agda

@@ -0,0 +1,145 @@
+------------------------------------------------------------------------
+-- 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
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
+open import Data.Vec.Relation.Binary.Equality.DecPropositional using (_≡?_)
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open CommutativeMonoid M
+open MonoidMultProperties monoid using (_×_; ×-homo-1; ×-homo-+)
+open CommutativeSemigroupProperties commutativeSemigroup using (interchange)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression monoid public
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of multiplicities (a bag).
+
+private
+  N : ℕ → Set
+  N n = Vec ℕ n
+
+-- Constructions on normal forms
+
+-- The empty bag.
+
+  empty : N n
+  empty = replicate _ 0
+
+-- A singleton bag.
+
+  sg : (i : Fin n) → N n
+  sg zero    = 1 ∷ empty
+  sg (suc i) = 0 ∷ sg i
+
+-- The composition of normal forms: bag union.
+  infixr 10 _•_
+
+  _•_  : (v w : N n) → N n
+  _•_ = zipWith _+_
+
+-- Packaging up the normal forms
+
+NF : ℕ → RawMonoid _ _
+NF n = record { Carrier = N n ; _≈_ = _≡_ ; _∙_ = _•_ ; ε = empty }
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : N n → Env n → Carrier
+⟦ []    ⟧⇓ _       = ε
+⟦ n ∷ v ⟧⇓ (a ∷ ρ) = (n × a) ∙ (⟦ v ⟧⇓ ρ)
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (N n)
+_≟_ = _≡?_ ℕ._≟_
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty bag stands for the unit ε.
+
+ε-homo : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+ε-homo [] = refl
+ε-homo (a ∷ ρ) = begin
+    ε ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ empty ⟧⇓ ρ       ≈⟨ ε-homo ρ ⟩
+    ε                  ∎
+
+-- The singleton bag stands for a single variable.
+
+sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
+sg-correct zero (x ∷ ρ) = begin
+    (1 × x) ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congʳ (×-homo-1 _) ⟩
+    x ∙ ⟦ empty ⟧⇓ ρ         ≈⟨ ∙-congˡ (ε-homo ρ) ⟩
+    x ∙ ε                    ≈⟨ identityʳ _ ⟩
+    x                        ∎
+sg-correct (suc x) (_ ∷ ρ) = begin
+    ε ∙ ⟦ sg x ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ sg x ⟧⇓ ρ       ≈⟨ sg-correct x ρ ⟩
+    lookup ρ x        ∎
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+∙-homo : ∀ v w (ρ : Env n) →
+         ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+∙-homo [] [] _ =  sym (identityˡ _)
+∙-homo (l ∷ v) (m ∷ w) (a ∷ ρ) = begin
+  ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ              ≈⟨ ∙-congʳ  (×-homo-+ a l m) ⟩
+  (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ          ≈⟨ ∙-congˡ  (∙-homo v w ρ) ⟩
+  (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩
+  ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ)   ∎
+
+------------------------------------------------------------------------
+-- Packaging everything up
+
+normal : NormalAPI
+normal = record
+  { NF       = NF
+  ; var      = sg
+  ; _≟_      = _≟_
+  ; ⟦_⟧⇓     = ⟦_⟧⇓
+  ; ⟦var_⟧⇓  = sg-correct
+  ; ⟦⟧⇓-homo = λ ρ → record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = λ where ≡.refl → refl }
+      ; homo = λ v w → ∙-homo v w ρ
+      }
+    ; ε-homo = ε-homo ρ
+    }
+  }
+
+open NormalAPI normal public
+  using (normalise; correct)