From 7db8db78aa5e4b5473fc845f07dcd0fe1b809363 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 13:21:42 +0100 Subject: [PATCH 01/16] refactor API for normal forms and its use for `Algebra.Monoid.Solver` --- src/Algebra/Solver/Monoid.agda | 151 +++++++--------------- src/Algebra/Solver/Monoid/Expression.agda | 126 ++++++++++++++++++ src/Algebra/Solver/Monoid/Normal.agda | 107 +++++++++++++++ src/Algebra/Solver/Monoid/Tactic.agda | 52 ++++++++ 4 files changed, 329 insertions(+), 107 deletions(-) create mode 100644 src/Algebra/Solver/Monoid/Expression.agda create mode 100644 src/Algebra/Solver/Monoid/Normal.agda create mode 100644 src/Algebra/Solver/Monoid/Tactic.agda diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 7debc4e1aa..9524236c05 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -6,133 +6,70 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra +open import Algebra.Bundles using (Monoid) -module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where +module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where -open import Data.Fin.Base as Fin -import Data.Fin.Properties as Fin -open import Data.List.Base hiding (lookup) -import Data.List.Relation.Binary.Equality.DecPropositional as ListEq +import Algebra.Solver.Monoid.Normal as Normal +import Algebra.Solver.Monoid.Tactic as Tactic open import Data.Maybe.Base as Maybe - using (Maybe; From-just; from-just) -open import Data.Nat.Base using (ℕ) + using (From-just; from-just) open import Data.Product.Base using (_×_; uncurry) -open import Data.Vec.Base using (Vec; lookup) -open import Function.Base using (_∘_; _$_) -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.Definitions using (DecidableEquality) +open import Function.Base using (_∘_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) -import Relation.Binary.Reflection -import Relation.Nullary.Decidable.Core as Dec - -open Monoid M -open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. - -infixr 5 _⊕_ - -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. +-- Expressions and Normal forms -Env : ℕ → Set _ -Env n = Vec Carrier n +open module N = Normal M public +-- for deprecation below + renaming (∙-homo to homomorphic; correct to normalise-correct) + hiding (module Expr) --- The semantics of an expression is a function from an environment to --- a value. - -⟦_⟧ : ∀ {n} → 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 list of variables. - -Normal : ℕ → Set -Normal n = List (Fin n) - --- The semantics of a normal form. +-- Tactic -⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier -⟦ [] ⟧⇓ ρ = ε -⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ +open module T = Tactic M normal public + hiding (prove) --- A normaliser. - -normalise : ∀ {n} → Expr n → Normal n -normalise (var x) = x ∷ [] -normalise id = [] -normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂ - --- The normaliser is homomorphic with respect to _++_/_∙_. - -homomorphic : ∀ {n} (nf₁ nf₂ : Normal n) (ρ : Env n) → - ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) -homomorphic [] nf₂ ρ = begin - ⟦ nf₂ ⟧⇓ ρ ≈⟨ sym $ identityˡ _ ⟩ - ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ -homomorphic (x ∷ nf₁) nf₂ ρ = begin - lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩ - lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ sym $ assoc _ _ _ ⟩ - lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ - --- The normaliser preserves the semantics of the expression. +prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es) +prove _ = from-just ∘ uncurry prove′ -normalise-correct : - ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ -normalise-correct (var x) ρ = begin - lookup ρ x ∙ ε ≈⟨ identityʳ _ ⟩ - lookup ρ x ∎ -normalise-correct id ρ = begin - ε ∎ -normalise-correct (e₁ ⊕ e₂) ρ = begin - ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩ - ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩ - ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ ------------------------------------------------------------------------ --- "Tactic. - -open module R = Relation.Binary.Reflection - setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct - public using (solve; _⊜_) +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. --- We can decide if two normal forms are /syntactically/ equal. +-- Version 2.2 -infix 5 _≟_ +{-# WARNING_ON_USAGE homomorphic +"Warning: homomorphic was deprecated in v2.2. +Please use (relevant field `homo` of) Algebra.Solver.Monoid.Normal.⟦⟧⇓-homo instead." +#-} -_≟_ : ∀ {n} → DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ListEq Fin._≟_ +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Normal.correct instead." +#-} --- We can also give a sound, but not necessarily complete, procedure --- for determining if two expressions have the same semantics. +{-# WARNING_ON_USAGE var +"Warning: var was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Expression.‵var instead." +#-} -prove′ : ∀ {n} (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₂ ⟧⇓ ρ ∎) +{-# WARNING_ON_USAGE id +"Warning: id was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Expression.‵ε instead." +#-} --- This procedure can be combined with from-just. +{-# WARNING_ON_USAGE _⊕_ +"Warning: _⊕_ was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Expression._‵∙_ instead." +#-} -prove : ∀ n (es : Expr n × Expr n) → - From-just (uncurry prove′ es) -prove _ = from-just ∘ uncurry prove′ diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda new file mode 100644 index 0000000000..d821db9373 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -0,0 +1,126 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) + +module Algebra.Solver.Monoid.Expression {c ℓ} (M : Monoid c ℓ) where + +open import Algebra.Bundles.Raw using (RawMonoid) +open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) +open import Algebra.Structures using (IsMonoid) +open import Data.Fin.Base using (Fin) +open import Data.Maybe.Base as Maybe using (Maybe) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (Vec; lookup) +open import Level using (suc; _⊔_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.Definitions using (DecidableEquality) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +private + variable + n : ℕ + + module M = Monoid M + + +------------------------------------------------------------------------ +-- Monoid expressions + +-- There is one constructor for every operation, plus one for +-- variables; there may be at most n variables. + +infixr 5 _‵∙_ + +data Expr (n : ℕ) : Set where + ‵var : Fin n → Expr n + ‵ε : Expr n + _‵∙_ : Expr n → Expr n → Expr n + +-- An environment contains one value for every variable. + +Env : ℕ → Set _ +Env n = Vec M.Carrier n + +-- The semantics of an expression is a function from an environment to +-- a value. + +⟦_⟧ : Expr n → Env n → M.Carrier +⟦ ‵var x ⟧ ρ = lookup ρ x +⟦ ‵ε ⟧ ρ = M.ε +⟦ e₁ ‵∙ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ + +------------------------------------------------------------------------ +-- API for normal expressions + +record NormalAPI {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where + infix 5 _≟_ + + field + + NF : ℕ → RawMonoid a r + + private + N : ℕ → Set a + N n = RawMonoid.Carrier (NF n) + + field + + var : Fin n → N n + +-- We can decide if two normal forms are /syntactically/ equal. + + _≟_ : DecidableEquality (N n) + +-- The semantics of a normal form. + ⟦_⟧⇓ : N n → Env n → M.Carrier + +-- Which "agrees with the environment on variables". + ⟦var_⟧⇓ : ∀ x ρ → ⟦ var x ⟧⇓ ρ M.≈ lookup {n = n} ρ x + +-- And which is a monoid homomorphism between NF and M + ⟦⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) M.rawMonoid λ e → ⟦ e ⟧⇓ ρ + +------------------------------------------------------------------------ +-- The normaliser and its correctness proof, as manifest fields of `Normal` + + module _ {n} where + + open module N = RawMonoid (NF n) + +-- Definition + + normalise : Expr n → N n + normalise (‵var x) = var x + normalise ‵ε = N.ε + normalise (e₁ ‵∙ e₂) = (normalise e₁) N.∙ (normalise e₂) + +-- The normaliser preserves the semantics of the expression. + + correct : ∀ e ρ → ⟦ normalise e ⟧⇓ ρ M.≈ ⟦ e ⟧ ρ + correct (‵var x) ρ = ⟦var x ⟧⇓ ρ + correct ‵ε ρ = ε-homo + where open IsMonoidHomomorphism (⟦⟧⇓-homo ρ) + correct (e₁ ‵∙ e₂) ρ = begin + ⟦ normalise e₁ N.∙ normalise e₂ ⟧⇓ ρ + ≈⟨ homo (normalise e₁) (normalise e₂) ⟩ + ⟦ normalise e₁ ⟧⇓ ρ M.∙ ⟦ normalise e₂ ⟧⇓ ρ + ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ + ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ + ∎ + where + open IsMonoid M.isMonoid using (∙-cong; setoid) + open ≈-Reasoning setoid + open IsMonoidHomomorphism (⟦⟧⇓-homo ρ) + +-- Semi-decision procedure for equality of normalised expressions + + _semi≟_ : ∀ e₁ e₂ → Maybe (normalise e₁ ≡ normalise e₂) + e₁ semi≟ e₂ = dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) + diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda new file mode 100644 index 0000000000..45d8a24469 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -0,0 +1,107 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Normal forms in commutative monoids +-- +-- Adapted from Algebra.Solver.Monoid.Normal +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) + +module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where + +open import Algebra.Bundles.Raw using (RawMonoid) +import Algebra.Properties.Monoid.Mult as MultProperties +import Algebra.Properties.Semigroup as Properties +open import Data.Fin.Base using (Fin; zero; suc) +import Data.Fin.Properties as Fin +open import Data.List.Base as List using (List; []; _∷_; [_]; _++_) +import Data.List.Properties as List +import Data.List.Relation.Binary.Equality.DecPropositional as ≋ +open import Data.Nat as ℕ using (ℕ; zero; suc; _+_) +open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith) +import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +open import Relation.Binary.Definitions using (DecidableEquality) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open Monoid M +open MultProperties M using (_×_; ×-homo-1; ×-homo-+) +open Properties semigroup using (x∙yz≈xy∙z) +open ≈-Reasoning setoid + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Monoid expressions + +open import Algebra.Solver.Monoid.Expression M public + +------------------------------------------------------------------------ +-- Normal forms + +-- A normal form is a list of variables. + +NF : ℕ → RawMonoid _ _ +NF n = List.++-[]-rawMonoid (Fin n) + +private + + N : ℕ → Set _ + N n = RawMonoid.Carrier (NF n) + +-- The semantics of a normal form. + +⟦_⟧⇓ : ∀ {n} → N n → Env n → Carrier +⟦ [] ⟧⇓ ρ = ε +⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ + +-- The normaliser is homomorphic with respect to _++_/_∙_. + +∙-homo : ∀ {n} (nf₁ nf₂ : N n) (ρ : Env n) → + ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) +∙-homo [] nf₂ ρ = begin + ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ + ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ +∙-homo (x ∷ nf₁) nf₂ ρ = begin + lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (∙-homo nf₁ nf₂ ρ) ⟩ + lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ x∙yz≈xy∙z _ _ _ ⟩ + lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : ∀ {n} → DecidableEquality (N n) +nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) + where open ≋ Fin._≟_ using (≋⇒≡; ≡⇒≋; _≋?_) + +------------------------------------------------------------------------ +-- Packaging everything up + +normal : NormalAPI +normal = record + { NF = NF + ; var = [_] + ; _≟_ = _≟_ + ; ⟦_⟧⇓ = ⟦_⟧⇓ + ; ⟦var_⟧⇓ = λ x ρ → identityʳ (lookup ρ x) + ; ⟦⟧⇓-homo = λ ρ → record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = λ where ≡.refl → refl + } + ; homo = λ nf₁ nf₂ → ∙-homo nf₁ nf₂ ρ + } + ; ε-homo = refl + } + } + +open NormalAPI normal public + using (correct) diff --git a/src/Algebra/Solver/Monoid/Tactic.agda b/src/Algebra/Solver/Monoid/Tactic.agda new file mode 100644 index 0000000000..46631cb1cc --- /dev/null +++ b/src/Algebra/Solver/Monoid/Tactic.agda @@ -0,0 +1,52 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) +import Algebra.Solver.Monoid.Expression as Expression + +module Algebra.Solver.Monoid.Tactic {a r c ℓ} + (M : Monoid c ℓ) + (open Monoid M using (setoid; _≈_)) + (open Expression M) + (N : NormalAPI {a} {r}) + where + +open import Data.Maybe.Base as Maybe using (Maybe; From-just; from-just) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Binary.Reflection as Reflection + +open NormalAPI N + + +------------------------------------------------------------------------ +-- Tactic + +-- Package the tactical behaviours + +open module R = Reflection setoid ‵var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct public + using (solve; _⊜_) + +-- We can also give a sound, but not necessarily complete, procedure +-- for determining if two expressions have the same semantics. + +prove′ : ∀ {n} e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ e₁ e₂ = Maybe.map lemma $ e₁ semi≟ e₂ + where + open ≈-Reasoning setoid + 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. + +prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) +prove _ e₁ e₂ = from-just $ prove′ e₁ e₂ + From e3a20b6403b492ffca6355342bb1f1af4b9d9c9d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 13:30:09 +0100 Subject: [PATCH 02/16] refactor use of `NormalAPI` for `CommutativeMonoid` --- src/Algebra/Solver/CommutativeMonoid.agda | 199 ++---------------- .../Solver/CommutativeMonoid/Normal.agda | 146 +++++++++++++ 2 files changed, 169 insertions(+), 176 deletions(-) create mode 100644 src/Algebra/Solver/CommutativeMonoid/Normal.agda diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 04d4d372e6..55ed56a539 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/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." +#-} diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..32b3b211fc --- /dev/null +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -0,0 +1,146 @@ +------------------------------------------------------------------------ +-- 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 CSProperties +import Algebra.Properties.Monoid.Mult as MultProperties +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) +import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +open import Relation.Binary.Definitions using (DecidableEquality) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open CommutativeMonoid M +open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) +open CSProperties 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. + 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) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) + where open Pointwise using (Pointwise-≡↔≡; decidable) + +------------------------------------------------------------------------ +-- 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 (correct) From 4d05510dadaf9e4fed32fc1c3728a1c76a88f182 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 13:49:13 +0100 Subject: [PATCH 03/16] refactor use of `NormalAPI` for `IdempotentCommutativeMonoid` --- .../Solver/CommutativeMonoid/Normal.agda | 3 +- .../Solver/IdempotentCommutativeMonoid.agda | 213 ++---------------- .../IdempotentCommutativeMonoid/Normal.agda | 163 ++++++++++++++ 3 files changed, 188 insertions(+), 191 deletions(-) create mode 100644 src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index 32b3b211fc..b43236d03f 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -10,7 +10,8 @@ open import Algebra.Bundles using (CommutativeMonoid) -module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where +module Algebra.Solver.CommutativeMonoid.Normal + {c ℓ} (M : CommutativeMonoid c ℓ) where open import Algebra.Bundles.Raw using (RawMonoid) import Algebra.Properties.CommutativeSemigroup as CSProperties diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 00b8824975..923f59f050 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -10,208 +10,41 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid) -open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) -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.Base as ℕ using (ℕ; zero; suc; _+_) -open import Data.Product.Base using (_×_; uncurry) -open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) +module Algebra.Solver.IdempotentCommutativeMonoidNEW + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where -open import Function.Base using (_∘_) +import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal +import Algebra.Solver.Monoid.Tactic as Tactic -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Relation.Binary.Reflection as Reflection -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.Binary.PropositionalEquality.Properties using (decSetoid) -open import Relation.Nullary.Decidable as Dec using (Dec) - - -module Algebra.Solver.IdempotentCommutativeMonoid - {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where - -open IdempotentCommutativeMonoid M -open ≈-Reasoning setoid - -private - variable - n : ℕ +open IdempotentCommutativeMonoid M using (monoid) ------------------------------------------------------------------------ --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. +-- Expressions and Normal forms -infixr 5 _⊕_ -infixr 10 _•_ +open module N = Normal M public +-- for deprecation below + renaming (∙-homo to comp-correct; correct to normalise-correct) + hiding (module Expr) -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. - -⟦_⟧ : ∀ {n} → 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 bits (a set). - -Normal : ℕ → Set -Normal n = Vec Bool n +-- Tactic --- The semantics of a normal form. +open Tactic monoid normal public -⟦_⟧⇓ : Normal n → Env n → Carrier -⟦ [] ⟧⇓ _ = ε -⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ) ------------------------------------------------------------------------ --- Constructions on normal forms - --- The empty set. - -empty : Normal n -empty = replicate _ false - --- A singleton set. - -sg : (i : Fin n) → Normal n -sg zero = true ∷ empty -sg (suc i) = false ∷ 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 set stands for the unit ε. - -empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε -empty-correct [] = refl -empty-correct (a ∷ ρ) = empty-correct ρ - --- The singleton set 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. - -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) ∎ - -distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c) -distr a b c = begin - a ∙ (b ∙ c) ≈⟨ ∙-cong (sym (idem a)) refl ⟩ - (a ∙ a) ∙ (b ∙ c) ≈⟨ assoc _ _ _ ⟩ - a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (sym (assoc _ _ _)) ⟩ - a ∙ ((a ∙ b) ∙ c) ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩ - a ∙ ((b ∙ a) ∙ c) ≈⟨ ∙-congˡ (assoc _ _ _) ⟩ - a ∙ (b ∙ (a ∙ c)) ≈⟨ sym (assoc _ _ _) ⟩ - (a ∙ b) ∙ (a ∙ c) ∎ - -comp-correct : ∀ (v w : Normal n) (ρ : Env n) → - ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) -comp-correct [] [] ρ = sym (identityˡ _) -comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _) -comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (sym (assoc _ _ _)) -comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (flip12 _ _ _) -comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = - comp-correct v w ρ - ------------------------------------------------------------------------- --- 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 Bool._≟_ 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.IdempotentCommutativeMonoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..b3e8100d3f --- /dev/null +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -0,0 +1,163 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Normal forms in commutative monoids +-- +-- Adapted from Algebra.Solver.Monoid.Normal +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (IdempotentCommutativeMonoid) + +module Algebra.Solver.IdempotentCommutativeMonoid.Normal + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where + +open import Algebra.Bundles.Raw using (RawMonoid) +import Algebra.Properties.CommutativeSemigroup as CSProperties +open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) +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) +import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +open import Relation.Binary.Definitions using (DecidableEquality) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open IdempotentCommutativeMonoid M +open CSProperties commutativeSemigroup using (interchange; x∙yz≈xy∙z; x∙yz≈y∙xz) +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 Bool n + +-- Constructions on normal forms + +-- The empty bag. + + empty : N n + empty = replicate _ false + +-- A singleton bag. + + sg : (i : Fin n) → N n + sg zero = true ∷ empty + sg (suc i) = false ∷ sg i + +-- The composition of normal forms. + 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 +⟦ [] ⟧⇓ _ = ε +⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ) + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (N n) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) + where open Pointwise using (Pointwise-≡↔≡; decidable) + +------------------------------------------------------------------------ +-- Correctness of the constructions on normal forms + +-- The empty bag stands for the unit ε. + +ε-homo : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε +ε-homo [] = refl +ε-homo (a ∷ ρ) = ε-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 + x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (ε-homo ρ) ⟩ + x ∙ ε ≈⟨ identityʳ _ ⟩ + x ∎ +sg-correct (suc x) (_ ∷ ρ) = sg-correct x ρ + +-- Normal form composition corresponds to the composition of the monoid. + +distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c) +distr a b c = begin + a ∙ (b ∙ c) ≈⟨ ∙-congʳ (idem a) ⟨ + (a ∙ a) ∙ (b ∙ c) ≈⟨ interchange _ _ _ _ ⟩ + (a ∙ b) ∙ (a ∙ c) ∎ + +∙-homo : ∀ v w (ρ : Env n) → + ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) +∙-homo [] [] ρ = sym (identityˡ _) +∙-homo (true ∷ v) (true ∷ w) (a ∷ ρ) = + trans (∙-congˡ (∙-homo v w ρ)) (distr _ _ _) +∙-homo (true ∷ v) (false ∷ w) (a ∷ ρ) = + trans (∙-congˡ (∙-homo v w ρ)) (x∙yz≈xy∙z _ _ _) +∙-homo (false ∷ v) (true ∷ w) (a ∷ ρ) = + trans (∙-congˡ (∙-homo v w ρ)) (x∙yz≈y∙xz _ _ _) +∙-homo (false ∷ v) (false ∷ w) (a ∷ ρ) = + ∙-homo v w ρ + +------------------------------------------------------------------------ +-- 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 (correct) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +flip12 = x∙yz≈y∙xz +{-# WARNING_ON_USAGE flip12 +"Warning: flip12 was deprecated in v2.2. +Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead." +#-} From 35ef5a5066764e8403ce3ed0079f8c1210cada07 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 14:44:34 +0100 Subject: [PATCH 04/16] additional exports --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 2 +- src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index b43236d03f..0ff967c985 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -144,4 +144,4 @@ normal = record } open NormalAPI normal public - using (correct) + using (normalise; correct) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index b3e8100d3f..43dbf12d24 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -145,7 +145,7 @@ normal = record } open NormalAPI normal public - using (correct) + using (normalise; correct) ------------------------------------------------------------------------ From d5a1f6336af408276ca4895d4c3642c174695474 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 16:30:38 +0100 Subject: [PATCH 05/16] refactor: simplify `import`s --- src/Algebra/Solver/Monoid/Normal.agda | 33 ++++++++++++--------------- 1 file changed, 14 insertions(+), 19 deletions(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 45d8a24469..d228443486 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -14,23 +14,19 @@ module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where open import Algebra.Bundles.Raw using (RawMonoid) import Algebra.Properties.Monoid.Mult as MultProperties -import Algebra.Properties.Semigroup as Properties -open import Data.Fin.Base using (Fin; zero; suc) -import Data.Fin.Properties as Fin -open import Data.List.Base as List using (List; []; _∷_; [_]; _++_) -import Data.List.Properties as List -import Data.List.Relation.Binary.Equality.DecPropositional as ≋ -open import Data.Nat as ℕ using (ℕ; zero; suc; _+_) -open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith) -import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +import Algebra.Properties.Semigroup as SemigroupProperties +open import Data.Fin as Fin using (Fin) +open import Data.List.Base using (List; []; _∷_; [_]; _++_; ++-[]-rawMonoid) +open import Data.List.Relation.Binary.Equality.DecPropositional using (_≡?_) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (lookup) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Relation.Nullary.Decidable as Dec open Monoid M open MultProperties M using (_×_; ×-homo-1; ×-homo-+) -open Properties semigroup using (x∙yz≈xy∙z) +open SemigroupProperties semigroup using (x∙yz≈xy∙z) open ≈-Reasoning setoid private @@ -49,7 +45,7 @@ open import Algebra.Solver.Monoid.Expression M public -- A normal form is a list of variables. NF : ℕ → RawMonoid _ _ -NF n = List.++-[]-rawMonoid (Fin n) +NF n = ++-[]-rawMonoid (Fin n) private @@ -58,14 +54,14 @@ private -- The semantics of a normal form. -⟦_⟧⇓ : ∀ {n} → N n → Env n → Carrier +⟦_⟧⇓ : N n → Env n → Carrier ⟦ [] ⟧⇓ ρ = ε ⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ -- The normaliser is homomorphic with respect to _++_/_∙_. -∙-homo : ∀ {n} (nf₁ nf₂ : N n) (ρ : Env n) → - ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) +∙-homo : (nf₁ nf₂ : N n) (ρ : Env n) → + ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ∙-homo [] nf₂ ρ = begin ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ @@ -78,9 +74,8 @@ private infix 5 _≟_ -_≟_ : ∀ {n} → DecidableEquality (N n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ≋ Fin._≟_ using (≋⇒≡; ≡⇒≋; _≋?_) +_≟_ : DecidableEquality (N n) +_≟_ = _≡?_ Fin._≟_ ------------------------------------------------------------------------ -- Packaging everything up @@ -104,4 +99,4 @@ normal = record } open NormalAPI normal public - using (correct) + using (normalise; correct) From b958d4855b3993f9acf7c4e687ecec384ceee9a2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 16:52:51 +0100 Subject: [PATCH 06/16] refactor: simplify `import`s --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index 0ff967c985..cb511b2fb7 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -19,7 +19,7 @@ import Algebra.Properties.Monoid.Mult as MultProperties 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) -import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +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 @@ -84,8 +84,7 @@ NF n = record { Carrier = N n ; _≈_ = _≡_ ; _∙_ = _•_ ; ε = empty } infix 5 _≟_ _≟_ : DecidableEquality (N n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) - where open Pointwise using (Pointwise-≡↔≡; decidable) +_≟_ = _≡?_ ℕ._≟_ ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms From 6a08273654eb208860936f6ef78a623544c5bd68 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 16:53:36 +0100 Subject: [PATCH 07/16] temporary commit: separate PR incoming --- .../Vec/Relation/Binary/Equality/DecPropositional.agda | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda b/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda index e8a288b338..e6dbf84f81 100644 --- a/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda +++ b/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda @@ -11,6 +11,8 @@ open import Relation.Binary.Definitions using (DecidableEquality) module Data.Vec.Relation.Binary.Equality.DecPropositional {a} {A : Set a} (_≟_ : DecidableEquality A) where +open import Data.Vec.Base using (Vec) +open import Data.Vec.Properties using (≡-dec) import Data.Vec.Relation.Binary.Equality.Propositional as PEq import Data.Vec.Relation.Binary.Equality.DecSetoid as DSEq open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) @@ -22,3 +24,11 @@ open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) open PEq public open DSEq (decSetoid _≟_) public using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid) + +------------------------------------------------------------------------ +-- Additional proofs + +infix 4 _≡?_ + +_≡?_ : ∀ {n} → DecidableEquality (Vec A n) +_≡?_ = ≡-dec _≟_ From 5a21ad1e6605936b7e456659e629bebdb7527b0f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 16:55:04 +0100 Subject: [PATCH 08/16] refactor: simplify `import`s --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index cb511b2fb7..f404f2e197 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -23,7 +23,6 @@ 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 -import Relation.Nullary.Decidable as Dec open CommutativeMonoid M open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) @@ -114,7 +113,7 @@ sg-correct (suc x) (_ ∷ ρ) = begin -- Normal form composition corresponds to the composition of the monoid. ∙-homo : ∀ v w (ρ : Env n) → - ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) + ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ∙-homo [] [] _ = sym (identityˡ _) ∙-homo (l ∷ v) (m ∷ w) (a ∷ ρ) = begin ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-+ a l m) ⟩ From 98c44c733aa1e9183201e5dff731d39dd7bb017e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 16:58:57 +0100 Subject: [PATCH 09/16] refactor: simplify `import`s --- .../IdempotentCommutativeMonoid/Normal.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 43dbf12d24..6c744b7e71 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -14,19 +14,19 @@ module Algebra.Solver.IdempotentCommutativeMonoid.Normal {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where open import Algebra.Bundles.Raw using (RawMonoid) -import Algebra.Properties.CommutativeSemigroup as CSProperties +import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) open import Data.Fin.Base using (Fin; zero; suc) -open import Data.Nat as ℕ using (ℕ; zero; suc; _+_) +open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith) -import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +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 -import Relation.Nullary.Decidable as Dec open IdempotentCommutativeMonoid M -open CSProperties commutativeSemigroup using (interchange; x∙yz≈xy∙z; x∙yz≈y∙xz) +open CommutativeSemigroupProperties commutativeSemigroup + using (interchange; x∙yz≈xy∙z; x∙yz≈y∙xz) open ≈-Reasoning setoid private @@ -83,8 +83,7 @@ NF n = record { Carrier = N n ; _≈_ = _≡_ ; _∙_ = _•_ ; ε = empty } infix 5 _≟_ _≟_ : DecidableEquality (N n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) - where open Pointwise using (Pointwise-≡↔≡; decidable) +_≟_ = _≡?_ Bool._≟_ ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms @@ -113,7 +112,7 @@ distr a b c = begin (a ∙ b) ∙ (a ∙ c) ∎ ∙-homo : ∀ v w (ρ : Env n) → - ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) + ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ∙-homo [] [] ρ = sym (identityˡ _) ∙-homo (true ∷ v) (true ∷ w) (a ∷ ρ) = trans (∙-congˡ (∙-homo v w ρ)) (distr _ _ _) From b37d16a5ae93861e861f250d85221b636e785442 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 31 Jul 2024 17:10:18 +0100 Subject: [PATCH 10/16] refactor: bring `Monoid M` into scope --- src/Algebra/Solver/Monoid/Expression.agda | 26 +++++++++++------------ 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda index d821db9373..c460cc2e01 100644 --- a/src/Algebra/Solver/Monoid/Expression.agda +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -27,7 +27,7 @@ private variable n : ℕ - module M = Monoid M +open Monoid M using (Carrier; _≈_; ε; _∙_; rawMonoid; isMonoid) ------------------------------------------------------------------------ @@ -46,15 +46,15 @@ data Expr (n : ℕ) : Set where -- An environment contains one value for every variable. Env : ℕ → Set _ -Env n = Vec M.Carrier n +Env n = Vec Carrier n -- The semantics of an expression is a function from an environment to -- a value. -⟦_⟧ : Expr n → Env n → M.Carrier +⟦_⟧ : Expr n → Env n → Carrier ⟦ ‵var x ⟧ ρ = lookup ρ x -⟦ ‵ε ⟧ ρ = M.ε -⟦ e₁ ‵∙ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ +⟦ ‵ε ⟧ ρ = ε +⟦ e₁ ‵∙ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ------------------------------------------------------------------------ -- API for normal expressions @@ -79,20 +79,20 @@ record NormalAPI {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where _≟_ : DecidableEquality (N n) -- The semantics of a normal form. - ⟦_⟧⇓ : N n → Env n → M.Carrier + ⟦_⟧⇓ : N n → Env n → Carrier -- Which "agrees with the environment on variables". - ⟦var_⟧⇓ : ∀ x ρ → ⟦ var x ⟧⇓ ρ M.≈ lookup {n = n} ρ x + ⟦var_⟧⇓ : ∀ x ρ → ⟦ var x ⟧⇓ ρ ≈ lookup {n = n} ρ x -- And which is a monoid homomorphism between NF and M - ⟦⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) M.rawMonoid λ e → ⟦ e ⟧⇓ ρ + ⟦⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) rawMonoid λ e → ⟦ e ⟧⇓ ρ ------------------------------------------------------------------------ -- The normaliser and its correctness proof, as manifest fields of `Normal` module _ {n} where - open module N = RawMonoid (NF n) + private module N = RawMonoid (NF n) -- Definition @@ -103,19 +103,19 @@ record NormalAPI {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where -- The normaliser preserves the semantics of the expression. - correct : ∀ e ρ → ⟦ normalise e ⟧⇓ ρ M.≈ ⟦ e ⟧ ρ + correct : ∀ e ρ → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ correct (‵var x) ρ = ⟦var x ⟧⇓ ρ correct ‵ε ρ = ε-homo where open IsMonoidHomomorphism (⟦⟧⇓-homo ρ) correct (e₁ ‵∙ e₂) ρ = begin ⟦ normalise e₁ N.∙ normalise e₂ ⟧⇓ ρ ≈⟨ homo (normalise e₁) (normalise e₂) ⟩ - ⟦ normalise e₁ ⟧⇓ ρ M.∙ ⟦ normalise e₂ ⟧⇓ ρ + ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ - ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ + ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ where - open IsMonoid M.isMonoid using (∙-cong; setoid) + open IsMonoid isMonoid using (∙-cong; setoid) open ≈-Reasoning setoid open IsMonoidHomomorphism (⟦⟧⇓-homo ρ) From 369ba7af3ae08fafa1846f6abf2f40be80d36c35 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 14 Aug 2024 09:08:46 +0100 Subject: [PATCH 11/16] bring up-to-date with recent PRs to `master` --- .../Solver/IdempotentCommutativeMonoid.agda | 2 +- .../IdempotentCommutativeMonoid/Normal.agda | 32 ++++++++++--------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 923f59f050..dfb8f50ab5 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -10,7 +10,7 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid) -module Algebra.Solver.IdempotentCommutativeMonoidNEW +module Algebra.Solver.IdempotentCommutativeMonoid {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 6c744b7e71..0c09a42c4e 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -15,6 +15,7 @@ module Algebra.Solver.IdempotentCommutativeMonoid.Normal open import Algebra.Bundles.Raw using (RawMonoid) import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties +import Algebra.Properties.IdempotentCommutativeMonoid as IdempotentCommutativeMonoidProperties open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Nat.Base using (ℕ; zero; suc; _+_) @@ -25,8 +26,9 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open IdempotentCommutativeMonoid M +open IdempotentCommutativeMonoidProperties M using (∙-distrˡ-∙) open CommutativeSemigroupProperties commutativeSemigroup - using (interchange; x∙yz≈xy∙z; x∙yz≈y∙xz) + using (x∙yz≈xy∙z; x∙yz≈y∙xz) open ≈-Reasoning setoid private @@ -42,7 +44,7 @@ open import Algebra.Solver.Monoid.Expression monoid public ------------------------------------------------------------------------ -- Normal forms --- A normal form is a vector of multiplicities (a bag). +-- A normal form is a vector of Booleans (a set of variable occurrences). private N : ℕ → Set @@ -50,18 +52,18 @@ private -- Constructions on normal forms --- The empty bag. +-- The empty set. empty : N n empty = replicate _ false --- A singleton bag. +-- A singleton set. sg : (i : Fin n) → N n sg zero = true ∷ empty sg (suc i) = false ∷ sg i --- The composition of normal forms. +-- The composition of normal forms: set union. infixr 10 _•_ _•_ : (v w : N n) → N n @@ -98,24 +100,18 @@ _≟_ = _≡?_ Bool._≟_ sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x sg-correct zero (x ∷ ρ) = begin - x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (ε-homo ρ) ⟩ - x ∙ ε ≈⟨ identityʳ _ ⟩ - x ∎ + x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (ε-homo ρ) ⟩ + x ∙ ε ≈⟨ identityʳ _ ⟩ + x ∎ sg-correct (suc x) (_ ∷ ρ) = sg-correct x ρ -- Normal form composition corresponds to the composition of the monoid. -distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c) -distr a b c = begin - a ∙ (b ∙ c) ≈⟨ ∙-congʳ (idem a) ⟨ - (a ∙ a) ∙ (b ∙ c) ≈⟨ interchange _ _ _ _ ⟩ - (a ∙ b) ∙ (a ∙ c) ∎ - ∙-homo : ∀ v w (ρ : Env n) → ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ∙-homo [] [] ρ = sym (identityˡ _) ∙-homo (true ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (∙-homo v w ρ)) (distr _ _ _) + trans (∙-congˡ (∙-homo v w ρ)) (∙-distrˡ-∙ _ _ _) ∙-homo (true ∷ v) (false ∷ w) (a ∷ ρ) = trans (∙-congˡ (∙-homo v w ρ)) (x∙yz≈xy∙z _ _ _) ∙-homo (false ∷ v) (true ∷ w) (a ∷ ρ) = @@ -160,3 +156,9 @@ flip12 = x∙yz≈y∙xz "Warning: flip12 was deprecated in v2.2. Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead." #-} + +distr = ∙-distrˡ-∙ +{-# WARNING_ON_USAGE distr +"Warning: distr was deprecated in v2.2. +Please use Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ instead." +#-} From 75eaac195c3ecc0b671af937408a5f7f54d37faf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 14 Aug 2024 09:22:24 +0100 Subject: [PATCH 12/16] bring up-to-date with recent PRs to `master`; tidy up names --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 10 +++++----- src/Algebra/Solver/Monoid/Tactic.agda | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index f404f2e197..d1810bcb8a 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -14,8 +14,8 @@ module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where open import Algebra.Bundles.Raw using (RawMonoid) -import Algebra.Properties.CommutativeSemigroup as CSProperties -import Algebra.Properties.Monoid.Mult as MultProperties +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) @@ -25,8 +25,8 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open CommutativeMonoid M -open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) -open CSProperties commutativeSemigroup using (interchange) +open MonoidMultProperties monoid using (_×_; ×-homo-1; ×-homo-+) +open CommutativeSemigroupProperties commutativeSemigroup using (interchange) open ≈-Reasoning setoid private @@ -61,7 +61,7 @@ private sg zero = 1 ∷ empty sg (suc i) = 0 ∷ sg i --- The composition of normal forms. +-- The composition of normal forms: bag union. infixr 10 _•_ _•_ : (v w : N n) → N n diff --git a/src/Algebra/Solver/Monoid/Tactic.agda b/src/Algebra/Solver/Monoid/Tactic.agda index 46631cb1cc..6f5e406b54 100644 --- a/src/Algebra/Solver/Monoid/Tactic.agda +++ b/src/Algebra/Solver/Monoid/Tactic.agda @@ -11,7 +11,6 @@ import Algebra.Solver.Monoid.Expression as Expression module Algebra.Solver.Monoid.Tactic {a r c ℓ} (M : Monoid c ℓ) - (open Monoid M using (setoid; _≈_)) (open Expression M) (N : NormalAPI {a} {r}) where @@ -22,6 +21,7 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reflection as Reflection +open Monoid M using (setoid; _≈_) open NormalAPI N From f309b5af349a0631ecd895400d6fe188cd2fa02f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 15 Aug 2024 16:02:52 +0100 Subject: [PATCH 13/16] made the `(Raw)Monoid` operation on normal forms explicit, rather than implicit --- src/Algebra/Solver/Monoid/Normal.agda | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index d228443486..98fc0dd6d8 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -49,8 +49,10 @@ NF n = ++-[]-rawMonoid (Fin n) private + module NF {n : ℕ} = RawMonoid (NF n) + N : ℕ → Set _ - N n = RawMonoid.Carrier (NF n) + N n = NF.Carrier {n} -- The semantics of a normal form. @@ -58,15 +60,15 @@ private ⟦ [] ⟧⇓ ρ = ε ⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ --- The normaliser is homomorphic with respect to _++_/_∙_. +-- The normaliser is homomorphic with respect to _++_ =def NF._∙_. ∙-homo : (nf₁ nf₂ : N n) (ρ : Env n) → - ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) + ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ∙-homo [] nf₂ ρ = begin ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ ∙-homo (x ∷ nf₁) nf₂ ρ = begin - lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (∙-homo nf₁ nf₂ ρ) ⟩ + lookup ρ x ∙ ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (∙-homo nf₁ nf₂ ρ) ⟩ lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ x∙yz≈xy∙z _ _ _ ⟩ lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ From f0961dad8787faf8699285a77694520fe46776b5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 15 Aug 2024 16:04:20 +0100 Subject: [PATCH 14/16] fix whitespace --- src/Algebra/Solver/Monoid/Normal.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 98fc0dd6d8..79cd0bdf03 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -50,7 +50,7 @@ NF n = ++-[]-rawMonoid (Fin n) private module NF {n : ℕ} = RawMonoid (NF n) - + N : ℕ → Set _ N n = NF.Carrier {n} From c90806fd6c7595cbb369ad7fd91cb64c5cde9b17 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 15 Aug 2024 16:12:09 +0100 Subject: [PATCH 15/16] redundant parentheses --- src/Algebra/Solver/Monoid/Normal.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 79cd0bdf03..a3385eadee 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -63,7 +63,7 @@ private -- The normaliser is homomorphic with respect to _++_ =def NF._∙_. ∙-homo : (nf₁ nf₂ : N n) (ρ : Env n) → - ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) + ⟦ nf₁ NF.∙ nf₂ ⟧⇓ ρ ≈ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∙-homo [] nf₂ ρ = begin ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ From 662fed9aa6b64331c638487f03f56cb1eddb5a85 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 16 Aug 2024 14:06:00 +0100 Subject: [PATCH 16/16] tighten `import`s --- src/Algebra/Solver/Monoid/Normal.agda | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index a3385eadee..0d93f1a68e 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -13,7 +13,6 @@ open import Algebra.Bundles using (Monoid) module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where open import Algebra.Bundles.Raw using (RawMonoid) -import Algebra.Properties.Monoid.Mult as MultProperties import Algebra.Properties.Semigroup as SemigroupProperties open import Data.Fin as Fin using (Fin) open import Data.List.Base using (List; []; _∷_; [_]; _++_; ++-[]-rawMonoid) @@ -21,11 +20,10 @@ open import Data.List.Relation.Binary.Equality.DecPropositional using (_≡?_) open import Data.Nat.Base using (ℕ) open import Data.Vec.Base using (lookup) open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Relation.Binary.PropositionalEquality.Core as ≡ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open Monoid M -open MultProperties M using (_×_; ×-homo-1; ×-homo-+) open SemigroupProperties semigroup using (x∙yz≈xy∙z) open ≈-Reasoning setoid @@ -49,7 +47,7 @@ NF n = ++-[]-rawMonoid (Fin n) private - module NF {n : ℕ} = RawMonoid (NF n) + module NF {n} = RawMonoid (NF n) N : ℕ → Set _ N n = NF.Carrier {n}