From 1e5eec16a96748c18f682e323865f3a4ac538ab2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 8 Jun 2024 13:26:14 +0100 Subject: [PATCH 01/26] refactor `Solver` infrastructure --- src/Algebra/Solver/CommutativeMonoid.agda | 26 +++++++++-------- .../Solver/IdempotentCommutativeMonoid.agda | 28 ++++++++++--------- src/Algebra/Solver/Monoid.agda | 26 +++++++++-------- src/Algebra/Solver/Ring.agda | 15 ++++++---- src/Relation/Binary/Reflection.agda | 14 ++++------ 5 files changed, 60 insertions(+), 49 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index f15f83824f..f95f055bd6 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -14,14 +14,16 @@ module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe - using (Maybe; decToMaybe; From-just; from-just) + 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) -open import Function.Base using (_∘_) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.Definitions using (DecidableEquality) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reflection as Reflection import Relation.Nullary.Decidable as Dec @@ -44,7 +46,6 @@ private -- variables; there may be at most n variables. infixr 5 _⊕_ -infixr 10 _•_ data Expr (n : ℕ) : Set where var : Fin n → Expr n @@ -93,11 +94,20 @@ 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 +-- 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 + ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms @@ -171,20 +181,12 @@ 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 (decToMaybe (normalise e₁ ≟ normalise e₂)) + Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) where lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ lemma eq ρ = diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 9ce8836bd4..435f55aad0 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -13,13 +13,15 @@ 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; decToMaybe; From-just; from-just) + 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) -open import Function.Base using (_∘_) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.Definitions using (DecidableEquality) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reflection as Reflection import Relation.Nullary.Decidable as Dec @@ -46,7 +48,6 @@ private -- variables; there may be at most n variables. infixr 5 _⊕_ -infixr 10 _•_ data Expr (n : ℕ) : Set where var : Fin n → Expr n @@ -61,7 +62,7 @@ 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 +⟦_⟧ : Expr n → Env n → Carrier ⟦ var x ⟧ ρ = lookup ρ x ⟦ id ⟧ ρ = ε ⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ @@ -95,11 +96,20 @@ sg zero = true ∷ empty sg (suc i) = false ∷ sg i -- The composition of normal forms. +infixr 10 _•_ _•_ : (v w : Normal n) → Normal n [] • [] = [] (l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) + where open Pointwise + ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms @@ -185,20 +195,12 @@ 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 (decToMaybe (normalise e₁ ≟ normalise e₂)) + Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) where lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ lemma eq ρ = diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 0928586c41..43656fea61 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -15,11 +15,12 @@ import Data.Fin.Properties as Fin open import Data.List.Base hiding (lookup) import Data.List.Relation.Binary.Equality.DecPropositional as ListEq open import Data.Maybe.Base as Maybe - using (Maybe; decToMaybe; From-just; from-just) + using (Maybe; From-just; from-just) open import Data.Nat.Base using (ℕ) 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 Relation.Binary.PropositionalEquality.Core using (_≡_; cong) @@ -30,6 +31,10 @@ import Relation.Nullary.Decidable as Dec open Monoid M open import Relation.Binary.Reasoning.Setoid setoid +private + variable + n : ℕ + ------------------------------------------------------------------------ -- Monoid expressions @@ -51,7 +56,7 @@ 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 +⟦_⟧ : Expr n → Env n → Carrier ⟦ var x ⟧ ρ = lookup ρ x ⟦ id ⟧ ρ = ε ⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ @@ -70,6 +75,13 @@ Normal n = List (Fin n) ⟦ [] ⟧⇓ ρ = ε ⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) where open ListEq Fin._≟_ + -- A normaliser. normalise : ∀ {n} → Expr n → Normal n @@ -110,20 +122,12 @@ open module R = Relation.Binary.Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct public using (solve; _⊜_) --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ - -_≟_ : ∀ {n} → DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ListEq Fin._≟_ - -- We can also give a sound, but not necessarily complete, procedure -- for determining if two expressions have the same semantics. prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) prove′ e₁ e₂ = - Maybe.map lemma $ decToMaybe (normalise e₁ ≟ normalise e₂) + Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) where lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ lemma eq ρ = diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index a2a982d5c2..333f052113 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -95,7 +95,12 @@ sem : Op → Op₂ Carrier sem [+] = _+_ sem [*] = _*_ -⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier +-- An environment contains one value for every variable. + +Env : ℕ → Set _ +Env = Vec Carrier + +⟦_⟧ : ∀ {n} → Polynomial n → Env n → Carrier ⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ ⟦ con c ⟧ ρ = ⟦ c ⟧′ ⟦ var x ⟧ ρ = lookup ρ x @@ -147,11 +152,11 @@ mutual -- Semantics. - ⟦_⟧H : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier + ⟦_⟧H : ∀ {n} → HNF (suc n) → Env (suc n) → Carrier ⟦ ∅ ⟧H _ = 0# ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ - ⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier + ⟦_⟧N : ∀ {n} → Normal n → Env n → Carrier ⟦ con c ⟧N _ = ⟦ c ⟧′ ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ @@ -325,7 +330,7 @@ normalise (:- t) = -N normalise t -- Evaluation after normalisation. -⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier +⟦_⟧↓ : ∀ {n} → Polynomial n → Env n → Carrier ⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ ------------------------------------------------------------------------ @@ -502,7 +507,7 @@ mutual ------------------------------------------------------------------------ -- Correctness -correct-con : ∀ {n} (c : C.Carrier) (ρ : Vec Carrier n) → +correct-con : ∀ {n} (c : C.Carrier) (ρ : Env n) → ⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′ correct-con c [] = refl correct-con c (x ∷ ρ) = begin diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda index 12665df8cc..cf7cf77e11 100644 --- a/src/Relation/Binary/Reflection.agda +++ b/src/Relation/Binary/Reflection.agda @@ -10,11 +10,10 @@ open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (ℕ) open import Data.Vec.Base as Vec using (Vec; allFin) -open import Function.Base using (id; _⟨_⟩_) +open import Function.Base using (id) open import Function.Bundles using (module Equivalence) open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.PropositionalEquality.Core as ≡ -- Think of the parameters as follows: -- @@ -33,18 +32,17 @@ import Relation.Binary.PropositionalEquality.Core as ≡ module Relation.Binary.Reflection {e a s} {Expr : ℕ → Set e} {A : Set a} - (Sem : Setoid a s) + (Sem : Setoid a s) (open Setoid Sem using (Carrier; _≈_)) (var : ∀ {n} → Fin n → Expr n) - (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Setoid.Carrier Sem) - (correct : ∀ {n} (e : Expr n) ρ → - ⟦ e ⇓⟧ ρ ⟨ Setoid._≈_ Sem ⟩ ⟦ e ⟧ ρ) + (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Carrier) + (correct : ∀ {n} (e : Expr n) ρ → ⟦ e ⇓⟧ ρ ≈ ⟦ e ⟧ ρ) where open import Data.Vec.N-ary open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +import Relation.Binary.PropositionalEquality.Core as ≡ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open Setoid Sem open ≈-Reasoning Sem -- If two normalised expressions are semantically equal, then their @@ -54,7 +52,7 @@ prove : ∀ {n} (ρ : Vec A n) e₁ e₂ → ⟦ e₁ ⇓⟧ ρ ≈ ⟦ e₂ ⇓⟧ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ prove ρ e₁ e₂ hyp = begin - ⟦ e₁ ⟧ ρ ≈⟨ sym (correct e₁ ρ) ⟩ + ⟦ e₁ ⟧ ρ ≈⟨ correct e₁ ρ ⟨ ⟦ e₁ ⇓⟧ ρ ≈⟨ hyp ⟩ ⟦ e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ ⟩ ⟦ e₂ ⟧ ρ ∎ From 036f8b51e71d2f1954d62731e81f83bdc35a67e8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Jun 2024 08:42:54 +0100 Subject: [PATCH 02/26] refactor `Solver` infrastructure --- .../List/Relation/Binary/Sublist/Heterogeneous/Solver.agda | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda index 57ae74303b..84aa29f931 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda @@ -32,6 +32,8 @@ open import Data.List.Relation.Binary.Sublist.Heterogeneous open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties open import Function.Base using (_$_; case_of_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≗_; sym; cong; cong₂; subst₂) open import Relation.Binary.PropositionalEquality.Properties as ≡ @@ -124,8 +126,8 @@ private -- Solver for items solveI : ∀ {n} (a b : Item n) → Maybe (a ⊆I b) -solveI (var k) (var l) = Maybe.map var $ decToMaybe (k Fin.≟ l) -solveI (val a) (val b) = Maybe.map val $ decToMaybe (R? a b) +solveI (var k) (var l) = Maybe.map var $ dec⇒weaklyDec Fin._≟_ k l +solveI (val a) (val b) = Maybe.map val $ dec⇒weaklyDec R? a b solveI _ _ = nothing -- Solver for linearised expressions From 8c6342ca7c5c9920f74ba9c99cbfe4751cf9f108 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Jun 2024 09:37:22 +0100 Subject: [PATCH 03/26] tighten imports and some `with` --- src/Tactic/RingSolver.agda | 1 - src/Tactic/RingSolver/NonReflective.agda | 4 +--- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda index 59475a3129..9c6cb29e8e 100644 --- a/src/Tactic/RingSolver.agda +++ b/src/Tactic/RingSolver.agda @@ -20,7 +20,6 @@ open import Data.Unit.Base using (⊤) open import Data.String.Base as String using (String; _++_; parens) open import Data.Product.Base using (_,_; proj₁) open import Function.Base -open import Relation.Nullary.Decidable open import Reflection open import Reflection.AST.Argument diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda index cc0b747037..fb33a2b9e0 100644 --- a/src/Tactic/RingSolver/NonReflective.agda +++ b/src/Tactic/RingSolver/NonReflective.agda @@ -33,9 +33,7 @@ open import Algebra.Properties.Semiring.Exp.TCOptimised semiring module Ops where zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x - zero-homo x _ with 0≟ x - zero-homo x _ | just p = p - zero-homo x () | nothing + zero-homo x _ with just p ← 0≟ x = p homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂ homo = record From e8ac5fddbc62c6cc694ba25399017ea1fab98f74 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Jun 2024 11:18:15 +0100 Subject: [PATCH 04/26] tidy up `Solver.Monoid` --- src/Algebra/Solver/Monoid.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 43656fea61..f1d2cce195 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -71,7 +71,7 @@ Normal n = List (Fin n) -- The semantics of a normal form. -⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier +⟦_⟧⇓ : Normal n → Env n → Carrier ⟦ [] ⟧⇓ ρ = ε ⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ @@ -84,14 +84,14 @@ nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) where open L -- A normaliser. -normalise : ∀ {n} → Expr n → Normal n +normalise : 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) → +homomorphic : (nf₁ nf₂ : Normal n) (ρ : Env n) → ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) homomorphic [] nf₂ ρ = begin ⟦ nf₂ ⟧⇓ ρ ≈⟨ sym $ identityˡ _ ⟩ @@ -104,7 +104,7 @@ homomorphic (x ∷ nf₁) nf₂ ρ = begin -- The normaliser preserves the semantics of the expression. normalise-correct : - ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ + (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ normalise-correct (var x) ρ = begin lookup ρ x ∙ ε ≈⟨ identityʳ _ ⟩ lookup ρ x ∎ @@ -125,7 +125,7 @@ open module R = Relation.Binary.Reflection -- We can also give a sound, but not necessarily complete, procedure -- for determining if two expressions have the same semantics. -prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) where From a495a12c150ea346432064abab6c9f2cfccfb2b6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Jun 2024 13:30:10 +0100 Subject: [PATCH 05/26] refactor `Algebra.Solver.*Monoid` --- CHANGELOG.md | 11 + src/Algebra/Solver/CommutativeMonoid.agda | 192 +---------------- .../Solver/CommutativeMonoid/Normal.agda | 139 ++++++++++++ .../Solver/IdempotentCommutativeMonoid.agda | 203 +----------------- .../IdempotentCommutativeMonoid/Normal.agda | 152 +++++++++++++ src/Algebra/Solver/Monoid.agda | 132 +----------- src/Algebra/Solver/Monoid/Normal.agda | 90 ++++++++ src/Algebra/Solver/Monoid/Tactic.agda | 52 +++++ 8 files changed, 470 insertions(+), 501 deletions(-) create mode 100644 src/Algebra/Solver/CommutativeMonoid/Normal.agda create mode 100644 src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda create mode 100644 src/Algebra/Solver/Monoid/Normal.agda create mode 100644 src/Algebra/Solver/Monoid/Tactic.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f8d6de9bd..21a233438c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -132,6 +132,17 @@ New modules Algebra.Morphism.Construct.Terminal ``` +* 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 + ``` + * Pointwise and equality relations over indexed containers: ```agda Data.Container.Indexed.Relation.Binary.Pointwise diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index f95f055bd6..a1ee900be0 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -8,197 +8,21 @@ {-# 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 import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.Definitions using (DecidableEquality) -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.PropositionalEquality.Core as ≡ using (_≡_) -open import Relation.Nullary.Decidable 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 _⊕_ - -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₂ ⟧ ρ +open CommutativeMonoid M using (monoid) ------------------------------------------------------------------------ -- 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 module N = Normal M public ------------------------------------------------------------------------ --- 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 - --- 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 - ------------------------------------------------------------------------- --- 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 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. - -prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) -prove _ e₁ e₂ = from-just (prove′ e₁ e₂) +-- Tactic --- prove : ∀ n (es : Expr n × Expr n) → --- From-just (uncurry prove′ es) --- prove _ = from-just ∘ uncurry prove′ +open Tactic monoid (record { N }) public diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..f0948a6be5 --- /dev/null +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -0,0 +1,139 @@ +------------------------------------------------------------------------ +-- 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 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 ≈-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 + flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c) + flip12 a b c = begin + a ∙ (b ∙ c) ≈⟨ 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. + +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₂ ⟧ ρ + ∎ diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 435f55aad0..bf702c43b1 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -10,209 +10,20 @@ 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) - -open import Function.Base using (_∘_; _$_) - -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.Definitions using (DecidableEquality) -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.PropositionalEquality.Core as ≡ using (_≡_) -open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) -open import Relation.Nullary.Decidable using (Dec) - module Algebra.Solver.IdempotentCommutativeMonoid - {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where - -open IdempotentCommutativeMonoid 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 _⊕_ - -data Expr (n : ℕ) : Set where - var : Fin n → Expr n - id : Expr n - _⊕_ : Expr n → Expr n → Expr n + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where --- An environment contains one value for every variable. +import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal +import Algebra.Solver.Monoid.Tactic as Tactic -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 IdempotentCommutativeMonoid M using (monoid) ------------------------------------------------------------------------ -- Normal forms --- A normal form is a vector of bits (a set). - -Normal : ℕ → Set -Normal n = Vec Bool n - --- The semantics of a normal form. - -⟦_⟧⇓ : 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. -infixr 10 _•_ - -_•_ : (v w : Normal n) → Normal n -[] • [] = [] -(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w - --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ - -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) - where open Pointwise +open module N = Normal M public ------------------------------------------------------------------------ --- 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 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. - -prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) -prove _ e₁ e₂ = from-just (prove′ e₁ e₂) +-- Tactic --- prove : ∀ n (es : Expr n × Expr n) → --- From-just (uncurry prove′ es) --- prove _ = from-just ∘ uncurry prove′ +open Tactic monoid (record { N }) public diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..7315146dc7 --- /dev/null +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -0,0 +1,152 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Solver for equations in idempotent commutative monoids +-- +-- Adapted from Algebra.Solver.CommutativeMonoid +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (IdempotentCommutativeMonoid) + +module Algebra.Solver.IdempotentCommutativeMonoid.Normal + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where + +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 (ℕ) +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 IdempotentCommutativeMonoid M +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 bits (a set). + +Normal : ℕ → Set +Normal n = Vec Bool n + +-- The semantics of a normal form. + +⟦_⟧⇓ : Normal 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 (Normal n) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) + where open Pointwise using (Pointwise-≡↔≡; decidable) + +------------------------------------------------------------------------ +-- 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. +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 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) ≈⟨ 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ʳ (idem a) ⟨ + (a ∙ a) ∙ (b ∙ c) ≈⟨ assoc _ _ _ ⟩ + a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (assoc _ _ _) ⟨ + a ∙ ((a ∙ b) ∙ c) ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩ + a ∙ ((b ∙ a) ∙ c) ≈⟨ ∙-congˡ (assoc _ _ _) ⟩ + a ∙ (b ∙ (a ∙ c)) ≈⟨ assoc _ _ _ ⟨ + (a ∙ b) ∙ (a ∙ c) ∎ + +comp-correct : ∀ v w (ρ : 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. + +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₂ ⟧ ρ + ∎ diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index f1d2cce195..e08bb169f0 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -6,137 +6,27 @@ {-# 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 Relation.Binary.PropositionalEquality.Core using (_≡_; cong) -import Relation.Binary.Reflection -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec - -open Monoid M -open import Relation.Binary.Reasoning.Setoid 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 _⊕_ - -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₂ ⟧ ρ +open import Function.Base using (_∘_) ------------------------------------------------------------------------ -- Normal forms --- A normal form is a list of variables. - -Normal : ℕ → Set -Normal n = List (Fin n) - --- The semantics of a normal form. - -⟦_⟧⇓ : Normal n → Env n → Carrier -⟦ [] ⟧⇓ ρ = ε -⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ - --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ - -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) where open ListEq Fin._≟_ - --- A normaliser. - -normalise : 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 : (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. - -normalise-correct : - (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₂ ⟧ ρ ∎ +open module N = Normal M public ------------------------------------------------------------------------ --- "Tactic. - -open module R = Relation.Binary.Reflection - setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) 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′ : (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₂ ⟧⇓ ρ ∎) +-- Tactic --- This procedure can be combined with from-just. +open module T = Tactic M (record { N }) public + hiding (prove) -prove : ∀ n (es : Expr n × Expr n) → - From-just (uncurry prove′ es) +prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es) prove _ = from-just ∘ uncurry prove′ diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda new file mode 100644 index 0000000000..543c7a59bc --- /dev/null +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -0,0 +1,90 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) + +module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where + +open import Data.Fin.Base using (Fin) +import Data.Fin.Properties as Fin +open import Data.List.Base using (List; [] ; _∷_; _++_) +import Data.List.Relation.Binary.Equality.DecPropositional as ≋ +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (lookup) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Definitions using (DecidableEquality) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open Monoid M +open ≈-Reasoning setoid + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Monoid expressions + +open import Algebra.Solver.Monoid.Expression rawMonoid public + +------------------------------------------------------------------------ +-- Normal forms + +-- A normal form is a list of variables. + +Normal : ℕ → Set _ +Normal n = List (Fin n) + +-- The semantics of a normal form. + +⟦_⟧⇓ : Normal n → Env n → Carrier +⟦ [] ⟧⇓ ρ = ε +⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) + where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋) + +-- A normaliser. + +normalise : 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 : ∀ nf₁ nf₂ (ρ : Env n) → + ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) +homomorphic [] nf₂ ρ = begin + ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ + ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ +homomorphic (x ∷ nf₁) nf₂ ρ = begin + lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩ + lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ assoc _ _ _ ⟨ + lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ + +-- The normaliser preserves the semantics of the expression. + +correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ +correct (var x) ρ = begin + lookup ρ x ∙ ε ≈⟨ identityʳ _ ⟩ + lookup ρ x ∎ +correct id ρ = begin + ε ∎ +correct (e₁ ⊕ e₂) ρ = begin + ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ + ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ + diff --git a/src/Algebra/Solver/Monoid/Tactic.agda b/src/Algebra/Solver/Monoid/Tactic.agda new file mode 100644 index 0000000000..6cae90372b --- /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 c ℓ} (M : Monoid c ℓ) + (open Monoid M using (rawMonoid; setoid; _≈_)) + (open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI)) + (N : NormalAPI {a}) where + +open import Data.Maybe.Base as Maybe + using (Maybe; From-just; from-just) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +import Relation.Binary.Reflection as Reflection + +open NormalAPI N +open module R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct public + using (solve; _⊜_) + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Tactic + +-- We can also give a sound, but not necessarily complete, procedure +-- for determining if two expressions have the same semantics. + +prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) + where + open import Relation.Binary.Reasoning.Setoid 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 77f420ab04aefad8613760f7c61189b43ed381ba Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Jun 2024 14:43:34 +0100 Subject: [PATCH 06/26] regularise vocabulary: deprecations --- CHANGELOG.md | 16 +++++++++++++++ .../Solver/IdempotentCommutativeMonoid.agda | 15 ++++++++++++++ src/Algebra/Solver/Monoid.agda | 20 +++++++++++++++++++ src/Algebra/Solver/Monoid/Normal.agda | 11 +++++----- 4 files changed, 56 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 21a233438c..7bff8810b1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -69,6 +69,22 @@ Deprecated names 1×-identityʳ ↦ ×-homo-1 ``` +* In `Algebra.Solver.CommutativeMonoid`: + ```agda + normalise-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.correct + ``` + +* In `Algebra.Solver.IdempotentCommutativeMonoid`: + ```agda + 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 + ``` + * In `Algebra.Structures.IsGroup`: ```agda _-_ ↦ _//_ diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index bf702c43b1..b8586d3a9c 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -22,8 +22,23 @@ open IdempotentCommutativeMonoid M using (monoid) -- Normal forms open module N = Normal M public + renaming (correct to normalise-correct) ------------------------------------------------------------------------ -- Tactic open Tactic monoid (record { N }) public + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.1. +Please use Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index e08bb169f0..6082961a7c 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -21,6 +21,7 @@ open import Function.Base using (_∘_) -- Normal forms open module N = Normal M public + renaming (correct to normalise-correct) ------------------------------------------------------------------------ -- Tactic @@ -30,3 +31,22 @@ open module T = Tactic M (record { N }) public prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es) prove _ = from-just ∘ uncurry prove′ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +{-# WARNING_ON_USAGE homomorphic +"Warning: homomorphic was deprecated in v2.1. +Please use Algebra.Solver.Monoid.Normal.comp-correct instead." +#-} + +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.1. +Please use Algebra.Solver.Monoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 543c7a59bc..6fd4f3e839 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -65,13 +65,13 @@ normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂ -- The normaliser is homomorphic with respect to _++_/_∙_. -homomorphic : ∀ nf₁ nf₂ (ρ : Env n) → +comp-correct : ∀ nf₁ nf₂ (ρ : Env n) → ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) -homomorphic [] nf₂ ρ = begin +comp-correct [] nf₂ ρ = begin ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ -homomorphic (x ∷ nf₁) nf₂ ρ = begin - lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩ +comp-correct (x ∷ nf₁) nf₂ ρ = begin + lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (comp-correct nf₁ nf₂ ρ) ⟩ lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ assoc _ _ _ ⟨ lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ @@ -84,7 +84,6 @@ correct (var x) ρ = begin correct id ρ = begin ε ∎ correct (e₁ ⊕ e₂) ρ = begin - ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩ + ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ - From 54a53a880054197967cd48a463a0158fba319be5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Jun 2024 14:58:21 +0100 Subject: [PATCH 07/26] `variable`s for `Algebra.Solver.Ring` --- src/Algebra/Solver/Ring.agda | 80 +++++++++++++++++++----------------- 1 file changed, 42 insertions(+), 38 deletions(-) diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index 333f052113..4d31bf5442 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -58,6 +58,11 @@ infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_ infixl 7 _:+_ _:-_ _+H_ _+N_ infix 4 _≈H_ _≈N_ +private + variable + n : ℕ + + ------------------------------------------------------------------------ -- Polynomials @@ -76,16 +81,16 @@ data Polynomial (m : ℕ) : Set r₁ where -- Short-hand notation. -_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:+_ : Polynomial n → Polynomial n → Polynomial n _:+_ = op [+] -_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:*_ : Polynomial n → Polynomial n → Polynomial n _:*_ = op [*] -_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:-_ : Polynomial n → Polynomial n → Polynomial n x :- y = x :+ :- y -_:×_ : ∀ {n} → ℕ → Polynomial n → Polynomial n +_:×_ : ℕ → Polynomial n → Polynomial n zero :× p = con C.0# suc m :× p = p :+ m :× p @@ -100,7 +105,7 @@ sem [*] = _*_ Env : ℕ → Set _ Env = Vec Carrier -⟦_⟧ : ∀ {n} → Polynomial n → Env n → Carrier +⟦_⟧ : Polynomial n → Env n → Carrier ⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ ⟦ con c ⟧ ρ = ⟦ c ⟧′ ⟦ var x ⟧ ρ = lookup ρ x @@ -137,12 +142,12 @@ mutual -- degree. data HNF : ℕ → Set r₁ where - ∅ : ∀ {n} → HNF (suc n) - _*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) + ∅ : HNF (suc n) + _*x+_ : HNF (suc n) → Normal n → HNF (suc n) data Normal : ℕ → Set r₁ where con : C.Carrier → Normal zero - poly : ∀ {n} → HNF (suc n) → Normal (suc n) + poly : HNF (suc n) → Normal (suc n) -- Note that the data types above do /not/ ensure uniqueness of -- normal forms: the zero polynomial of degree one can be @@ -152,11 +157,11 @@ mutual -- Semantics. - ⟦_⟧H : ∀ {n} → HNF (suc n) → Env (suc n) → Carrier + ⟦_⟧H : HNF (suc n) → Env (suc n) → Carrier ⟦ ∅ ⟧H _ = 0# ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ - ⟦_⟧N : ∀ {n} → Normal n → Env n → Carrier + ⟦_⟧N : Normal n → Env n → Carrier ⟦ con c ⟧N _ = ⟦ c ⟧′ ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ @@ -167,12 +172,12 @@ mutual -- Equality. - data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where - ∅ : ∀ {n} → _≈H_ {suc n} ∅ ∅ + data _≈H_ : HNF n → HNF n → Set (r₁ ⊔ r₃) where + ∅ : _≈H_ {suc n} ∅ ∅ _*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} → p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂) - data _≈N_ : ∀ {n} → Normal n → Normal n → Set (r₁ ⊔ r₃) where + data _≈N_ : Normal n → Normal n → Set (r₁ ⊔ r₃) where con : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂ poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂ @@ -182,7 +187,7 @@ mutual infix 4 _≟H_ _≟N_ - _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n}) + _≟H_ : WeaklyDecidable (_≈H_ {n = n}) ∅ ≟H ∅ = just ∅ ∅ ≟H (_ *x+ _) = nothing (_ *x+ _) ≟H ∅ = nothing @@ -191,7 +196,7 @@ mutual ... | _ | nothing = nothing ... | nothing | _ = nothing - _≟N_ : ∀ {n} → WeaklyDecidable (_≈N_ {n = n}) + _≟N_ : WeaklyDecidable (_≈N_ {n = n}) con c₁ ≟N con c₂ with c₁ coeff≟ c₂ ... | just c₁≈c₂ = just (con c₁≈c₂) ... | nothing = nothing @@ -203,7 +208,7 @@ mutual -- The semantics respect the equality relations defined above. - ⟦_⟧H-cong : ∀ {n} {p₁ p₂ : HNF (suc n)} → + ⟦_⟧H-cong : {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ ⟦ ∅ ⟧H-cong _ = refl ⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) = @@ -211,9 +216,8 @@ mutual ⟨ +-cong ⟩ ⟦ c₁≈c₂ ⟧N-cong ρ - ⟦_⟧N-cong : - ∀ {n} {p₁ p₂ : Normal n} → - p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ + ⟦_⟧N-cong : {p₁ p₂ : Normal n} → + p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ ⟦ con c₁≈c₂ ⟧N-cong _ = c₁≈c₂ ⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ @@ -222,10 +226,10 @@ mutual -- Zero. -0H : ∀ {n} → HNF (suc n) +0H : HNF (suc n) 0H = ∅ -0N : ∀ {n} → Normal n +0N : Normal n 0N {zero} = con C.0# 0N {suc n} = poly 0H @@ -233,16 +237,16 @@ mutual -- One. - 1H : ∀ {n} → HNF (suc n) + 1H : HNF (suc n) 1H {n} = ∅ *x+ 1N {n} - 1N : ∀ {n} → Normal n + 1N : Normal n 1N {zero} = con C.1# 1N {suc n} = poly 1H -- A simplifying variant of _*x+_. -_*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) +_*x+HN_ : HNF (suc n) → Normal n → HNF (suc n) (p *x+ c′) *x+HN c = (p *x+ c′) *x+ c ∅ *x+HN c with c ≟N 0N ... | just c≈0 = ∅ @@ -252,49 +256,49 @@ mutual -- Addition. - _+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) + _+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) ∅ +H p = p p +H ∅ = p (p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂) - _+N_ : ∀ {n} → Normal n → Normal n → Normal n + _+N_ : Normal n → Normal n → Normal n con c₁ +N con c₂ = con (c₁ C.+ c₂) poly p₁ +N poly p₂ = poly (p₁ +H p₂) -- Multiplication. -_*x+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) +_*x+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) p₁ *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c ∅ *x+H ∅ = ∅ (p₁ *x+ c) *x+H ∅ = (p₁ *x+ c) *x+ 0N mutual - _*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n) + _*NH_ : Normal n → HNF (suc n) → HNF (suc n) c *NH ∅ = ∅ c *NH (p *x+ c′) with c ≟N 0N ... | just c≈0 = ∅ ... | nothing = (c *NH p) *x+ (c *N c′) - _*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) + _*HN_ : HNF (suc n) → Normal n → HNF (suc n) ∅ *HN c = ∅ (p *x+ c′) *HN c with c ≟N 0N ... | just c≈0 = ∅ ... | nothing = (p *HN c) *x+ (c′ *N c) - _*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) + _*H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) ∅ *H _ = ∅ (_ *x+ _) *H ∅ = ∅ (p₁ *x+ c₁) *H (p₂ *x+ c₂) = ((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂) - _*N_ : ∀ {n} → Normal n → Normal n → Normal n + _*N_ : Normal n → Normal n → Normal n con c₁ *N con c₂ = con (c₁ C.* c₂) poly p₁ *N poly p₂ = poly (p₁ *H p₂) -- Exponentiation. -_^N_ : ∀ {n} → Normal n → ℕ → Normal n +_^N_ : Normal n → ℕ → Normal n p ^N zero = 1N p ^N suc n = p *N (p ^N n) @@ -302,25 +306,25 @@ mutual -- Negation. - -H_ : ∀ {n} → HNF (suc n) → HNF (suc n) + -H_ : HNF (suc n) → HNF (suc n) -H p = (-N 1N) *NH p - -N_ : ∀ {n} → Normal n → Normal n + -N_ : Normal n → Normal n -N con c = con (C.- c) -N poly p = poly (-H p) ------------------------------------------------------------------------ -- Normalisation -normalise-con : ∀ {n} → C.Carrier → Normal n +normalise-con : C.Carrier → Normal n normalise-con {zero} c = con c normalise-con {suc n} c = poly (∅ *x+HN normalise-con c) -normalise-var : ∀ {n} → Fin n → Normal n +normalise-var : Fin n → Normal n normalise-var zero = poly ((∅ *x+ 1N) *x+ 0N) normalise-var (suc i) = poly (∅ *x+HN normalise-var i) -normalise : ∀ {n} → Polynomial n → Normal n +normalise : Polynomial n → Normal n normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂ normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂ normalise (con c) = normalise-con c @@ -330,7 +334,7 @@ normalise (:- t) = -N normalise t -- Evaluation after normalisation. -⟦_⟧↓ : ∀ {n} → Polynomial n → Env n → Carrier +⟦_⟧↓ : Polynomial n → Env n → Carrier ⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ ------------------------------------------------------------------------ From 706b3a15ead12138a723bde3fdc3f89a6e5349a5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Jun 2024 15:05:18 +0100 Subject: [PATCH 08/26] tweaks --- CHANGELOG.md | 6 ++++++ src/Algebra/Solver/CommutativeMonoid.agda | 15 +++++++++++++++ src/Algebra/Solver/Monoid.agda | 2 +- 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7bff8810b1..f736aa774e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -401,6 +401,12 @@ Additions to existing modules idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x ``` +* In `Algebra.Solver.Ring` + ```agda + Env : ℕ → Set _ + Env = Vec Carrier + ``` + * In `Algebra.Structures` ```agda record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index a1ee900be0..b583ab7df1 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -21,8 +21,23 @@ open CommutativeMonoid M using (monoid) -- Normal forms open module N = Normal M public + renaming (correct to normalise-correct) ------------------------------------------------------------------------ -- Tactic open Tactic monoid (record { N }) public + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.1. +Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 6082961a7c..690d4bac93 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -21,7 +21,7 @@ open import Function.Base using (_∘_) -- Normal forms open module N = Normal M public - renaming (correct to normalise-correct) + renaming (comp-correct to homomorphic; correct to normalise-correct) ------------------------------------------------------------------------ -- Tactic From 24d04951574cb7b6598a387bc62f15100002a9d4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Jun 2024 15:41:50 +0100 Subject: [PATCH 09/26] forgot to add `Expression` module --- src/Algebra/Solver/Monoid/Expression.agda | 69 +++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 src/Algebra/Solver/Monoid/Expression.agda diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda new file mode 100644 index 0000000000..43fc81ea21 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -0,0 +1,69 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Raw using (RawMonoid) + +module Algebra.Solver.Monoid.Expression {c ℓ} (M : RawMonoid c ℓ) where + +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (Vec; lookup) +open import Level using (suc; _⊔_) +open import Relation.Binary.Definitions using (DecidableEquality) + +open RawMonoid M + +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 _⊕_ + +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₂ ⟧ ρ + +------------------------------------------------------------------------ +-- API for normal expressions + +record NormalAPI {a} : Set (suc a ⊔ c ⊔ ℓ) where + infix 5 _≟_ + + field + +-- The type of normal forms. + Normal : ℕ → Set a +-- We can decide if two normal forms are /syntactically/ equal. + _≟_ : DecidableEquality (Normal n) +-- A normaliser. + normalise : Expr n → Normal n +-- The semantics of a normal form. + ⟦_⟧⇓ : Normal n → Env n → Carrier +-- The normaliser preserves the semantics of the expression. + correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ + From 28c1791e3ae158e085e099c324efb908b544aef3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 14 Jun 2024 12:51:40 +0100 Subject: [PATCH 10/26] refactor: use existing lemma --- CHANGELOG.md | 1 + .../Solver/CommutativeMonoid/Normal.agda | 10 ++----- .../IdempotentCommutativeMonoid/Normal.agda | 30 ++++++++++++------- 3 files changed, 23 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f736aa774e..395c6d39ce 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -76,6 +76,7 @@ Deprecated names * In `Algebra.Solver.IdempotentCommutativeMonoid`: ```agda + flip12 ↦ Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz normalise-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct ``` diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index f0948a6be5..e823a53a4b 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -12,6 +12,7 @@ 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) @@ -22,6 +23,7 @@ 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 @@ -103,16 +105,10 @@ comp-correct : ∀ v w (ρ : Env n) → 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) ≈⟨ 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 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 _ _)) ------------------------------------------------------------------------ diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 7315146dc7..141689e99c 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -13,6 +13,7 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid) module Algebra.Solver.IdempotentCommutativeMonoid.Normal {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where +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.Base using (ℕ) @@ -23,6 +24,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Nullary.Decidable as Dec open IdempotentCommutativeMonoid M +open CSProperties commutativeSemigroup using (x∙yz≈y∙xz) open ≈-Reasoning setoid private @@ -99,20 +101,11 @@ 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) ≈⟨ 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ʳ (idem a) ⟨ (a ∙ a) ∙ (b ∙ c) ≈⟨ assoc _ _ _ ⟩ - a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (assoc _ _ _) ⟨ - a ∙ ((a ∙ b) ∙ c) ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩ - a ∙ ((b ∙ a) ∙ c) ≈⟨ ∙-congˡ (assoc _ _ _) ⟩ + a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (x∙yz≈y∙xz _ _ _) ⟩ a ∙ (b ∙ (a ∙ c)) ≈⟨ assoc _ _ _ ⟨ (a ∙ b) ∙ (a ∙ c) ∎ @@ -124,7 +117,7 @@ comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = 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 _ _ _) + trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈y∙xz _ _ _) comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = comp-correct v w ρ @@ -150,3 +143,18 @@ correct (e₁ ⊕ e₂) ρ = begin ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +flip12 = x∙yz≈y∙xz +{-# WARNING_ON_USAGE flip12 +"Warning: flip12 was deprecated in v2.1. +Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead." +#-} From 7e8f2e897568d6825ed8233be8d4e6dcb708eeb9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 26 Jul 2024 15:16:53 +0100 Subject: [PATCH 11/26] fixed deprecations to `v2.2` --- src/Algebra/Solver/CommutativeMonoid.agda | 4 ++-- src/Algebra/Solver/IdempotentCommutativeMonoid.agda | 4 ++-- src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda | 4 ++-- src/Algebra/Solver/Monoid.agda | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 5d0ad1427c..4e6540d508 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -36,9 +36,9 @@ open Tactic monoid (record { N }) public -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 2.1 +-- Version 2.2 {-# WARNING_ON_USAGE normalise-correct -"Warning: normalise-correct was deprecated in v2.1. +"Warning: normalise-correct was deprecated in v2.2. Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead." #-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index b8586d3a9c..922c735f41 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -36,9 +36,9 @@ open Tactic monoid (record { N }) public -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 2.1 +-- Version 2.2 {-# WARNING_ON_USAGE normalise-correct -"Warning: normalise-correct was deprecated in v2.1. +"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 index 141689e99c..2edfef7626 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -151,10 +151,10 @@ correct (e₁ ⊕ e₂) ρ = begin -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 2.1 +-- Version 2.2 flip12 = x∙yz≈y∙xz {-# WARNING_ON_USAGE flip12 -"Warning: flip12 was deprecated in v2.1. +"Warning: flip12 was deprecated in v2.2. Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead." #-} diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index fb43106349..3708d7b5e3 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -40,14 +40,14 @@ prove _ = from-just ∘ uncurry prove′ -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 2.1 +-- Version 2.2 {-# WARNING_ON_USAGE homomorphic -"Warning: homomorphic was deprecated in v2.1. +"Warning: homomorphic was deprecated in v2.2. Please use Algebra.Solver.Monoid.Normal.comp-correct instead." #-} {-# WARNING_ON_USAGE normalise-correct -"Warning: normalise-correct was deprecated in v2.1. +"Warning: normalise-correct was deprecated in v2.2. Please use Algebra.Solver.Monoid.Normal.correct instead." #-} From f83f962d425929594823937b2390407a7f687ba0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 27 Jul 2024 09:04:51 +0100 Subject: [PATCH 12/26] v2.2 `CHANGELOG` --- CHANGELOG.md | 838 +-------------------------------------------------- 1 file changed, 2 insertions(+), 836 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 66bb4bb286..7414d9be1d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.1-dev +Version 2.2-dev =============== -The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3. +The library has been tested using Agda 2.6.4.3. Highlights ---------- @@ -9,68 +9,18 @@ Highlights Bug-fixes --------- -* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate` - was mistakenly applied to the level of the type `A` instead of the - variable `x` of type `A`. - -* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer - exports the `Setoid` module under the alias `S`. - -* Remove unbound parameter from `Data.List.Properties.length-alignWith`, - `alignWith-map` and `map-alignWith`. - Non-backwards compatible changes -------------------------------- -* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now - parametrized by _raw_ bundles rather than lawful bundles, in line with other - modules defining morphism structures. -* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now - parametrized by _raw_ bundles, and as such take a proof of transitivity. -* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now - parametrized by _raw_ bundles, and as such take a proof of reflexivity. -* The module `IO.Primitive` was moved to `IO.Primitive.Core`. -* The modules in the `Data.Word` hierarchy were moved to the `Data.Word64` - one instead. - -Other major improvements ------------------------- - Minor improvements ------------------ -* The size of the dependency graph for many modules has been - reduced. This may lead to speed ups for first-time loading of some - modules. - -* The definition of the `Pointwise` relational combinator in - `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise` - has been generalised to take heterogeneous arguments in `REL`. - -* The structures `IsSemilattice` and `IsBoundedSemilattice` in - `Algebra.Lattice.Structures` have been redefined as aliases of - `IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`. - - Deprecated modules ------------------ -* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of - `Data.List.Relation.Binary.Sublist.Propositional.Slice`. - -* The modules `Function.Endomorphism.Propositional` and - `Function.Endomorphism.Setoid` that use the old `Function` - hierarchy. Use `Function.Endo.Propositional` and - `Function.Endo.Setoid` instead. - Deprecated names ---------------- -* In `Algebra.Properties.Semiring.Mult`: - ```agda - 1×-identityʳ ↦ ×-homo-1 - ``` - * In `Algebra.Solver.CommutativeMonoid`: ```agda normalise-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.correct @@ -88,99 +38,9 @@ Deprecated names normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct ``` -* In `Algebra.Structures.IsGroup`: - ```agda - _-_ ↦ _//_ - ``` - -* In `Data.Maybe.Base`: - ```agda - decToMaybe ↦ Relation.Nullary.Decidable.Core.dec⇒maybe - ``` - -* In `Algebra.Structures.Biased`: - ```agda - IsRing* ↦ Algebra.Structures.IsRing - isRing* ↦ Algebra.Structures.isRing - ``` - -* In `Data.List.Base`: - ```agda - scanr ↦ Data.List.Scans.Base.scanr - scanl ↦ Data.List.Scans.Base.scanl - ``` - -* In `Data.List.Properties`: - ```agda - scanr-defn ↦ Data.List.Scans.Properties.scanr-defn - scanl-defn ↦ Data.List.Scans.Properties.scanl-defn - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - map-compose ↦ map-∘ - ``` - -* In `Data.Nat.Base`: the following pattern synonyms and definitions are all - deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_` - ```agda - pattern less-than-or-equal {k} eq = k , eq - pattern ≤″-offset k = k , refl - pattern <″-offset k = k , refl - s≤″s⁻¹ - ``` - -* In `Data.Nat.Divisibility.Core`: - ```agda - *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ - ``` - -* In `Data.Sum`: - ```agda - fromDec ↦ Relation.Nullary.Decidable.Core.toSum - toDec ↦ Relation.Nullary.Decidable.Core.fromSum - ``` - -* In `IO.Base`: - ```agda - untilRight ↦ untilInj₂ - ``` - -* In `Data.Float.Base`: - ```agda - toWord ↦ toWord64 - ``` - -* In `Data.Float.Properties`: - ```agda - toWord-injective ↦ toWord64-injective - ``` - New modules ----------- -* Pointwise lifting of algebraic structures `IsX` and bundles `X` from - carrier set `C` to function space `A → C`: - ``` - Algebra.Construct.Pointwise - ``` - -* Raw bundles for module-like algebraic structures: - ``` - Algebra.Module.Bundles.Raw - ``` - -* Nagata's construction of the "idealization of a module": - ```agda - Algebra.Module.Construct.Idealization - ``` - -* The unique morphism from the initial, resp. terminal, algebra: - ```agda - Algebra.Morphism.Construct.Initial - Algebra.Morphism.Construct.Terminal - ``` - * Refactoring of the `Algebra.Solver.*Monoid` implementations, via a single `Tactic` module API based on the existing `Expr`, and a common `Normal`-form API: @@ -192,705 +52,11 @@ New modules Algebra.Solver.Monoid.Tactic ``` -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* `Data.List.Relation.Binary.Sublist.Propositional.Slice` - replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*) - and adding new functions: - - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*) - - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*) - ``` - -* Prime factorisation of natural numbers. - ``` - Data.Nat.Primality.Factorisation - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation`, defining: - ```agda - _↭_ : IRel (Vector A) _ - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above: - ```agda - ↭-refl : Reflexive (Vector A) _↭_ - ↭-reflexive : xs ≡ ys → xs ↭ ys - ↭-sym : Symmetric (Vector A) _↭_ - ↭-trans : Transitive (Vector A) _↭_ - isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_ - indexedSetoid : {A : Set a} → IndexedSetoid ℕ a _ - ``` - -* The modules `Function.Endo.Propositional` and - `Function.Endo.Setoid` are new but are actually proper ports of - `Function.Endomorphism.Propositional` and - `Function.Endomorphism.Setoid`. - -* `Function.Relation.Binary.Equality` - ```agda - setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _ - ``` - and a convenient infix version - ```agda - _⇨_ = setoid - ``` - -* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: - ```agda - Induction.InfiniteDescent - ``` - -* Symmetric interior of a binary relation - ``` - Relation.Binary.Construct.Interior.Symmetric - ``` - -* Properties of `Setoid`s with decidable equality relation: - ``` - Relation.Binary.Properties.DecSetoid - ``` - -* Systematise the use of `Recomputable A = .A → A`: - ```agda - Relation.Nullary.Recomputable - ``` - with `Recomputable` exported publicly from `Relation.Nullary`. - -* New IO primitives to handle buffering - ```agda - IO.Primitive.Handle - IO.Handle - ``` - -* `System.Random` bindings: - ```agda - System.Random.Primitive - System.Random - ``` - -* Show modules: - ```agda - Data.List.Show - Data.Vec.Show - Data.Vec.Bounded.Show - ``` - -* Word64 literals and bit-based functions: - ```agda - Data.Word64.Literals - Data.Word64.Unsafe - Data.Word64.Show - ``` - -* A type of bytes: - ```agda - Data.Word8.Primitive - Data.Word8.Base - Data.Word8.Literals - Data.Word8.Show - ``` - -* Bytestrings and builders: - ```agda - Data.Bytestring.Base - Data.Bytestring.Builder.Base - Data.Bytestring.Builder.Primitive - Data.Bytestring.IO - Data.Bytestring.IO.Primitive - Data.Bytestring.Primitive - ``` - -* Decidability for the subset relation on lists: - ```agda - Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) - Data.List.Relation.Binary.Subset.DecPropositional - ``` - -* Decidability for the disjoint relation on lists: - ```agda - Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) - Data.List.Relation.Binary.Disjoint.DecPropositional - ``` - Additions to existing modules ----------------------------- -* In `Algebra.Bundles` - ```agda - record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) - record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) - ``` - and additional manifest fields for sub-bundles arising from these in: - ```agda - IdempotentCommutativeMonoid - IdempotentSemiring - ``` - - -* In `Algebra.Bundles.Raw` - ```agda - record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - ``` - -* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: - ```agda - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - +-rawGroup : RawGroup _ _ - ``` - -* In `Algebra.Construct.Terminal`: - ```agda - rawNearSemiring : RawNearSemiring c ℓ - nearSemiring : NearSemiring c ℓ - ``` - -* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. - -* In `Algebra.Module.Construct.DirectProduct`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - ``` - -* In `Algebra.Module.Construct.TensorUnit`: - ```agda - rawLeftSemimodule : RawLeftSemimodule _ c ℓ - rawLeftModule : RawLeftModule _ c ℓ - rawRightSemimodule : RawRightSemimodule _ c ℓ - rawRightModule : RawRightModule _ c ℓ - rawBisemimodule : RawBisemimodule _ _ c ℓ - rawBimodule : RawBimodule _ _ c ℓ - rawSemimodule : RawSemimodule _ c ℓ - rawModule : RawModule _ c ℓ - ``` - -* In `Algebra.Module.Construct.Zero`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R c ℓ - rawLeftModule : RawLeftModule R c ℓ - rawRightSemimodule : RawRightSemimodule R c ℓ - rawRightModule : RawRightModule R c ℓ - rawBisemimodule : RawBisemimodule R c ℓ - rawBimodule : RawBimodule R c ℓ - rawSemimodule : RawSemimodule R c ℓ - rawModule : RawModule R c ℓ - ``` - -* In `Algebra.Morphism.Structures`: - ```agda - module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where - record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - - IsSemigroupHomomorphism : (A → B) → Set _ - IsSemigroupMonomorphism : (A → B) → Set _ - IsSemigroupIsomorphism : (A → B) → Set _ - ``` -* In `Algebra.Properties.AbelianGroup`: - ``` - ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x - ``` - -* In `Algebra.Properties.Group`: - ```agda - isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ - quasigroup : Quasigroup _ _ - isLoop : IsLoop _∙_ _\\_ _//_ ε - loop : Loop _ _ - - \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ - \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ - \\-leftDivides : LeftDivides _∙_ _\\_ - //-rightDividesˡ : RightDividesˡ _∙_ _//_ - //-rightDividesʳ : RightDividesʳ _∙_ _//_ - //-rightDivides : RightDivides _∙_ _//_ - - ⁻¹-selfInverse : SelfInverse _⁻¹ - x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y - x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε - \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ - comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x - ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x - ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x - ``` - -* In `Algebra.Properties.Loop`: - ```agda - identityˡ-unique : x ∙ y ≈ y → x ≈ ε - identityʳ-unique : x ∙ y ≈ x → y ≈ ε - identity-unique : Identity x _∙_ → x ≈ ε - ``` - -* In `Algebra.Properties.Monoid.Mult`: - ```agda - ×-homo-0 : ∀ x → 0 × x ≈ 0# - ×-homo-1 : ∀ x → 1 × x ≈ x - ``` - -* In `Algebra.Properties.Semiring.Mult`: - ```agda - ×-homo-0# : ∀ x → 0 × x ≈ 0# * x - ×-homo-1# : ∀ x → 1 × x ≈ 1# * x - idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x - ``` - * In `Algebra.Solver.Ring` ```agda Env : ℕ → Set _ Env = Vec Carrier ``` - -* In `Algebra.Structures` - ```agda - record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ - record IsCommutativeBand (∙ : Op₂ A) : Set _ - record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _ - ``` - and additional manifest fields for substructures arising from these in: - ```agda - IsIdempotentCommutativeMonoid - IsIdempotentSemiring - ``` - -* In `Algebra.Structures.IsGroup`: - ```agda - infixl 6 _//_ - _//_ : Op₂ A - x // y = x ∙ (y ⁻¹) - infixr 6 _\\_ - _\\_ : Op₂ A - x \\ y = (x ⁻¹) ∙ y - ``` - -* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the - extra property as an exposed definition: - ```agda - *-cancelʳ-nonZero : AlmostRightCancellative 0# * - ``` - -* In `Data.Bool.Show`: - ```agda - showBit : Bool → Char - ``` - -* In `Data.Container.Indexed.Core`: - ```agda - Subtrees o c = (r : Response c) → X (next c r) - ``` - -* In `Data.Empty`: - ```agda - ⊥-elim-irr : .⊥ → Whatever - ``` - -* In `Data.Fin.Properties`: - ```agda - nonZeroIndex : Fin n → ℕ.NonZero n - ``` - -* In `Data.Float.Base`: - ```agda - _≤_ : Rel Float _ - ``` - -* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym - ```agda - pattern divides k eq = Data.Nat.Divisibility.divides k eq - ``` - -* In `Data.Integer.Properties`: - ```agda - ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) - sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j - i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) - ``` - -* In `Data.List.Base` redefine `inits` and `tails` in terms of: - ```agda - tail∘inits : List A → List (List A) - tail∘tails : List A → List (List A) - ``` - -* In `Data.List.Membership.Propositional.Properties.Core`: - ```agda - find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p - ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - reverse⁺ : x ∈ xs → x ∈ reverse xs - reverse⁻ : x ∈ reverse xs → x ∈ xs - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - inits : List A → List⁺ (List A) - tails : List A → List⁺ (List A) - ``` - -* In `Data.List.NonEmpty.Properties`: - ```agda - toList-inits : toList ∘ List⁺.inits ≗ List.inits - toList-tails : toList ∘ List⁺.tails ≗ List.tails - ``` - -* In `Data.List.Properties`: - ```agda - length-catMaybes : length (catMaybes xs) ≤ length xs - applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) - applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) - upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) - downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) - reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse - reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n - reverse-upTo : reverse (upTo n) ≡ downFrom n - reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n - reverse-downFrom : reverse (downFrom n) ≡ upTo n - mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) - map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) - align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) - zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) - unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) - map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) - unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip - splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n - uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons - last-map : last ∘ map f ≗ map f ∘ last - tail-map : tail ∘ map f ≗ map (map f) ∘ tail - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as - unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g - foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x - alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs - alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs - align-flip : align xs ys ≡ map swap (align ys xs) - zip-flip : zip xs ys ≡ map swap (zip ys xs) - unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f - unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip - take-take : take n (take m xs) ≡ take (n ⊓ m) xs - take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) - zip-unzip : uncurry′ zip ∘ unzip ≗ id - unzipWith-zipWith : f ∘ uncurry′ g ≗ id → - length xs ≡ length ys → - unzipWith f (zipWith g xs ys) ≡ (xs , ys) - unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) - mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys - unzipWith-++ : unzipWith f (xs ++ ys) ≡ - zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) - catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe - catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) - Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs) - mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs - mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ [] - mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs - mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ [] - ``` - -* In `Data.List.Relation.Binary.Pointwise.Base`: - ```agda - unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S) - ``` - -* In `Data.Maybe.Relation.Binary.Pointwise`: - ```agda - pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid`: - ```agda - ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs - ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs - ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → - trans p (trans q r) ≡ trans (trans p q) r) → - (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → - ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs - ``` - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs - - reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs - reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs - reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs - ``` - -* In `Data.List.Relation.Unary.All`: - ```agda - universal-U : Universal (All U) - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) - Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) - ``` - -* In `Data.List.Relation.Unary.AllPairs.Properties`: - ```agda - catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) - tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f) - ``` - -* In `Data.List.Relation.Unary.Any.Properties`: - ```agda - map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) → - (p : Any P xs) → Any.map f p ≡ Any.map g p - ``` - -* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: - ```agda - through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → - ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs - through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → - ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs - assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds → - ∃[ ys ] Appending bs cs ys × Appending as ys ds - ``` - -* In `Data.List.Relation.Ternary.Appending.Properties`: - ```agda - through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → - ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs → - ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs - through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) → - ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs → - ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs - assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds - assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds - ``` - -* In `Data.Nat.Divisibility`: - ```agda - quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient - - m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m - m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient - quotient-∣ : m ∣ n → quotient ∣ n - quotient>1 : m ∣ n → m < n → 1 < quotient - quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n - n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient - - m/n≡0⇒m⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n - productOfPrimes≢0 : All Prime as → NonZero (product as) - productOfPrimes≥1 : All Prime as → product as ≥ 1 - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - product-↭ : product Preserves _↭_ ⟶ _≡_ - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`: - ```agda - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* Added some very-dependent map and zipWith to `Data.Product`. - ```agda - map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → - (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → - ((x , y) : Σ A P) → Σ (B x) (Q y) - - map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → - (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y - - zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} - (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → - (_*_ : (x : C) → (y : R x) → S x y) → - ((a , p) : Σ A P) → ((b , q) : Σ B Q) → - S (a ∙ b) (p ∘ q) - - ``` - -* In `Data.Rational.Properties`: - ```agda - 1≢0 : 1ℚ ≢ 0ℚ - - #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) - invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q - - isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ - heytingField : HeytingField 0ℓ 0ℓ 0ℓ - ``` - -* Added new functions in `Data.String.Base`: - ```agda - map : (Char → Char) → String → String - between : String → String → String → String - ``` - -* Re-exported new types and functions in `IO`: - ```agda - BufferMode : Set - noBuffering : BufferMode - lineBuffering : BufferMode - blockBuffering : Maybe ℕ → BufferMode - Handle : Set - stdin : Handle - stdout : Handle - stderr : Handle - hSetBuffering : Handle → BufferMode → IO ⊤ - hGetBuffering : Handle → IO BufferMode - hFlush : Handle → IO ⊤ - ``` - -* Added new functions in `IO.Base`: - ```agda - whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤ - forever : IO ⊤ → IO ⊤ - ``` - -* In `IO.Primitive.Core`: - ```agda - _>>_ : IO A → IO B → IO B - ``` - -* In `Data.Word64.Base`: - ```agda - _≤_ : Rel Word64 zero - show : Word64 → String - ``` - -* Added new definition in `Relation.Binary.Construct.Closure.Transitive` - ```agda - transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_ - ``` - -* Added new definition in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - ``` - -* Added new functions in `Data.Vec.Bounded.Base`: - ```agda - isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n - toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as) - ``` - -* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can - be used infix. - -* Added new proofs in `Relation.Binary.Construct.Composition`: - ```agda - transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ - ``` - -* Added new definitions in `Relation.Binary.Definitions` - ``` - Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) - Empty _∼_ = ∀ {x y} → ¬ (x ∼ y) - ``` - -* Added new proofs in `Relation.Binary.Properties.Setoid`: - ```agda - ≉-irrefl : Irreflexive _≈_ _≉_ - ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ - ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ - ``` - -* Added new definitions in `Relation.Nullary` - ``` - Recomputable : Set _ - WeaklyDecidable : Set _ - ``` - -* Added new definition and proof in `Relation.Nullary.Decidable.Core`: - ```agda - dec⇒maybe : Dec A → Maybe A - recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q - toSum : Dec A → A ⊎ ¬ A - fromSum : A ⊎ ¬ A → Dec A - ``` - -* Added new proof in `Relation.Nullary.Decidable`: - ```agda - ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ - ``` - -* Added new definitions in `Relation.Nullary.Negation.Core`: - ```agda - contradiction-irr : .A → ¬ A → Whatever - ``` - -* Added new definitions in `Relation.Nullary.Reflects`: - ```agda - recompute : Reflects A b → Recomputable A - recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q - ``` - -* Added new definitions in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - WeaklyDecidable : Pred A ℓ → Set _ - ``` - -* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details. - - Provide a marker function, `⌞_⌟`, for user-guided anti-unification. - - Improved support for equalities between terms with instance arguments, - such as terms that contain `_/_` or `_%_`. From d75b2c932affb4b5435e2942a0d75692a8ec3250 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 28 Jul 2024 13:48:57 +0100 Subject: [PATCH 13/26] use `zipWith`! --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 5 ++--- src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda | 5 ++--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index e823a53a4b..aba3baceea 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -16,7 +16,7 @@ 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) +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) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -77,8 +77,7 @@ sg (suc i) = 0 ∷ sg i infixr 10 _•_ _•_ : (v w : Normal n) → Normal n -[] • [] = [] -(l ∷ v) • (m ∷ w) = l + m ∷ v • w +_•_ = zipWith _+_ ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 2edfef7626..a3bed7089c 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -17,7 +17,7 @@ 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.Base using (ℕ) -open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) +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) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -78,8 +78,7 @@ sg (suc i) = false ∷ sg i infixr 10 _•_ _•_ : (v w : Normal n) → Normal n -[] • [] = [] -(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w +_•_ = zipWith _∨_ ------------------------------------------------------------------------ -- Correctness of the constructions on normal forms From b876988241c78cb034b70387539c13298707389f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 09:33:47 +0100 Subject: [PATCH 14/26] remove dependency on `Data.Nat.GeneralisedArithmetic.fold` --- .../Solver/CommutativeMonoid/Normal.agda | 38 +++++++++++-------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index aba3baceea..33ae840309 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -12,10 +12,11 @@ open import Algebra.Bundles using (CommutativeMonoid) module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where +import Algebra.Definitions.RawMonoid as Definitions 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.Nat.GeneralisedArithmetic using (fold) 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) @@ -23,7 +24,9 @@ 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 Definitions rawMonoid using (_×_) +open MultProperties monoid using (×-homo-1; ×-homo-+) +open CSProperties commutativeSemigroup using (interchange) open ≈-Reasoning setoid private @@ -49,7 +52,7 @@ Normal n = Vec ℕ n ⟦_⟧⇓ : Normal n → Env n → Carrier ⟦ [] ⟧⇓ _ = ε -⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n +⟦ n ∷ v ⟧⇓ (a ∷ ρ) = (n × a) ∙ (⟦ v ⟧⇓ ρ) -- We can decide if two normal forms are /syntactically/ equal. @@ -86,29 +89,34 @@ _•_ = zipWith _+_ empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε empty-correct [] = refl -empty-correct (a ∷ ρ) = empty-correct ρ +empty-correct (a ∷ ρ) = begin + ε ∙ ⟦ empty ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ + ⟦ empty ⟧⇓ ρ ≈⟨ 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 ρ + (1 × x) ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-1 _) ⟩ + x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ + x ∙ ε ≈⟨ identityʳ _ ⟩ + x ∎ +sg-correct (suc x) (m ∷ ρ) = begin + ε ∙ ⟦ sg x ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ + ⟦ sg x ⟧⇓ ρ ≈⟨ sg-correct x ρ ⟩ + lookup ρ 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 _ _)) +comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin + ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-+ a l m) ⟩ + (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congˡ (comp-correct v w ρ) ⟩ + (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩ + ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ) ∎ ------------------------------------------------------------------------ -- Normalization From b7a819ff739b76ab68d2404c7ffce383e85fda8e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 09:37:59 +0100 Subject: [PATCH 15/26] simplify `import` dependencies --- src/Algebra/Solver/CommutativeMonoid/Normal.agda | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index 33ae840309..f4f6354459 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -12,7 +12,6 @@ open import Algebra.Bundles using (CommutativeMonoid) module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where -import Algebra.Definitions.RawMonoid as Definitions import Algebra.Properties.CommutativeSemigroup as CSProperties import Algebra.Properties.Monoid.Mult as MultProperties open import Data.Fin.Base using (Fin; zero; suc) @@ -24,8 +23,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Nullary.Decidable as Dec open CommutativeMonoid M -open Definitions rawMonoid using (_×_) -open MultProperties monoid using (×-homo-1; ×-homo-+) +open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) open CSProperties commutativeSemigroup using (interchange) open ≈-Reasoning setoid From 2940a783dfc803ffbf41bfc363e8bd6e59b35976 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 30 Jul 2024 10:29:41 +0100 Subject: [PATCH 16/26] refactor: tweaks --- .../Solver/IdempotentCommutativeMonoid/Normal.agda | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index a3bed7089c..1dfbe08e12 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -24,7 +24,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Nullary.Decidable as Dec open IdempotentCommutativeMonoid M -open CSProperties commutativeSemigroup using (x∙yz≈y∙xz) +open CSProperties commutativeSemigroup using (interchange; x∙yz≈xy∙z; x∙yz≈y∙xz) open ≈-Reasoning setoid private @@ -103,9 +103,7 @@ sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ 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) ≈⟨ assoc _ _ _ ⟩ - a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (x∙yz≈y∙xz _ _ _) ⟩ - a ∙ (b ∙ (a ∙ c)) ≈⟨ assoc _ _ _ ⟨ + (a ∙ a) ∙ (b ∙ c) ≈⟨ interchange _ _ _ _ ⟩ (a ∙ b) ∙ (a ∙ c) ∎ comp-correct : ∀ v w (ρ : Env n) → @@ -114,7 +112,7 @@ 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 _ _ _)) + trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈xy∙z _ _ _) comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) = trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈y∙xz _ _ _) comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = From ef864ee853242a6880c9f0bc377ff2356094550d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 10:25:38 +0100 Subject: [PATCH 17/26] change `Level` parameterisation of `NormalAPI` --- src/Algebra/Solver/Monoid/Expression.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda index 43fc81ea21..7b71c9e9c2 100644 --- a/src/Algebra/Solver/Monoid/Expression.agda +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -51,7 +51,7 @@ Env n = Vec Carrier n ------------------------------------------------------------------------ -- API for normal expressions -record NormalAPI {a} : Set (suc a ⊔ c ⊔ ℓ) where +record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where infix 5 _≟_ field From e35ae9f9d6e016cbdc515e2b4d501d858bd1555b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 10:27:48 +0100 Subject: [PATCH 18/26] clarify exports from `module R`? --- .../Solver/Monoid/{Tactic.agda => Solver.agda} | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) rename src/Algebra/Solver/Monoid/{Tactic.agda => Solver.agda} (84%) diff --git a/src/Algebra/Solver/Monoid/Tactic.agda b/src/Algebra/Solver/Monoid/Solver.agda similarity index 84% rename from src/Algebra/Solver/Monoid/Tactic.agda rename to src/Algebra/Solver/Monoid/Solver.agda index 6cae90372b..a692d5c7bf 100644 --- a/src/Algebra/Solver/Monoid/Tactic.agda +++ b/src/Algebra/Solver/Monoid/Solver.agda @@ -9,10 +9,10 @@ open import Algebra.Bundles using (Monoid) import Algebra.Solver.Monoid.Expression as Expression -module Algebra.Solver.Monoid.Tactic {a c ℓ} (M : Monoid c ℓ) +module Algebra.Solver.Monoid.Solver {a c ℓ} (M : Monoid c ℓ) (open Monoid M using (rawMonoid; setoid; _≈_)) (open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI)) - (N : NormalAPI {a}) where + (N : NormalAPI a) where open import Data.Maybe.Base as Maybe using (Maybe; From-just; from-just) @@ -23,16 +23,20 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) import Relation.Binary.Reflection as Reflection open NormalAPI N -open module R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct public - using (solve; _⊜_) private variable n : ℕ - + module + R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct ------------------------------------------------------------------------ --- Tactic +-- Proof procedures + +-- Re-export the existing solver machinery from `Reflection` + +open R public + using (solve; _⊜_) -- We can also give a sound, but not necessarily complete, procedure -- for determining if two expressions have the same semantics. @@ -46,7 +50,7 @@ prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (n ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ ⟦ normalise e₂ ⟧⇓ ρ ∎ --- This procedure can be combined with from-just. +-- This procedure can then 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 eb71dd0647bdde6269b029a7657aeb5b6dddf44f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 10:37:19 +0100 Subject: [PATCH 19/26] deprecations --- .../Solver/CommutativeMonoid/Normal.agda | 41 ++++++++++++++----- 1 file changed, 31 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index f4f6354459..2d75ec21fe 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -70,9 +70,9 @@ empty = replicate _ 0 -- A singleton bag. -sg : (i : Fin n) → Normal n -sg zero = 1 ∷ empty -sg (suc i) = 0 ∷ sg i +singleton : (i : Fin n) → Normal n +singleton zero = 1 ∷ empty +singleton (suc i) = 0 ∷ singleton i -- The composition of normal forms. infixr 10 _•_ @@ -94,15 +94,16 @@ empty-correct (a ∷ ρ) = begin -- The singleton bag stands for a single variable. -sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x -sg-correct zero (x ∷ ρ) = begin +singleton-correct : (x : Fin n) (ρ : Env n) → + ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x +singleton-correct zero (x ∷ ρ) = begin (1 × x) ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-1 _) ⟩ x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ x ∙ ε ≈⟨ identityʳ _ ⟩ x ∎ -sg-correct (suc x) (m ∷ ρ) = begin - ε ∙ ⟦ sg x ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ - ⟦ sg x ⟧⇓ ρ ≈⟨ sg-correct x ρ ⟩ +singleton-correct (suc x) (m ∷ ρ) = begin + ε ∙ ⟦ singleton x ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ + ⟦ singleton x ⟧⇓ ρ ≈⟨ singleton-correct x ρ ⟩ lookup ρ x ∎ -- Normal form composition corresponds to the composition of the monoid. @@ -122,14 +123,14 @@ comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin -- A normaliser. normalise : Expr n → Normal n -normalise (var x) = sg x +normalise (var x) = singleton 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 (var x) ρ = singleton-correct x ρ correct id ρ = empty-correct ρ correct (e₁ ⊕ e₂) ρ = begin ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ @@ -138,3 +139,23 @@ correct (e₁ ⊕ e₂) ρ = begin ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +sg = singleton +{-# WARNING_ON_USAGE sg +"Warning: sg was deprecated in v2.2. +Please use singleton instead." +#-} +sg-correct = singleton-correct +{-# WARNING_ON_USAGE sg-correct +"Warning: sg-correct was deprecated in v2.2. +Please use singleton-correct instead." +#-} From f218b8c3e4263c52f8c943502e8ce005afc004dd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 10:38:28 +0100 Subject: [PATCH 20/26] knock-on effects --- src/Algebra/Solver/CommutativeMonoid.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 4e6540d508..03ffeba82c 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -13,7 +13,7 @@ open import Algebra.Bundles using (CommutativeMonoid) module Algebra.Solver.CommutativeMonoid {c ℓ} (M : CommutativeMonoid c ℓ) where import Algebra.Solver.CommutativeMonoid.Normal as Normal -import Algebra.Solver.Monoid.Tactic as Tactic +import Algebra.Solver.Monoid.Solver as Solver open CommutativeMonoid M using (monoid) @@ -25,9 +25,9 @@ open module N = Normal M public renaming (correct to normalise-correct) ------------------------------------------------------------------------ --- Tactic +-- Proof procedures -open Tactic monoid (record { N }) public +open Solver monoid (record { N }) public ------------------------------------------------------------------------ From 1c02f9418191fa6c6b973b196aec9ce68a84c17f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 11:03:30 +0100 Subject: [PATCH 21/26] deprecations --- .../IdempotentCommutativeMonoid/Normal.agda | 43 ++++++++++++------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 1dfbe08e12..bb90c66c72 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -14,6 +14,7 @@ module Algebra.Solver.IdempotentCommutativeMonoid.Normal {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where import Algebra.Properties.CommutativeSemigroup as CSProperties +open import Algebra.Properties.IdempotentCommutativeMonoid M using (∙-distrˡ-∙) 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 (ℕ) @@ -24,7 +25,7 @@ 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 CSProperties commutativeSemigroup using (x∙yz≈xy∙z; x∙yz≈y∙xz) open ≈-Reasoning setoid private @@ -70,9 +71,9 @@ empty = replicate _ false -- A singleton set. -sg : (i : Fin n) → Normal n -sg zero = true ∷ empty -sg (suc i) = false ∷ sg i +singleton : (i : Fin n) → Normal n +singleton zero = true ∷ empty +singleton (suc i) = false ∷ singleton i -- The composition of normal forms. infixr 10 _•_ @@ -91,26 +92,21 @@ 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 +singleton-correct : (x : Fin n) (ρ : Env n) → + ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x +singleton-correct zero (x ∷ ρ) = begin x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ x ∙ ε ≈⟨ identityʳ _ ⟩ x ∎ -sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ +singleton-correct (suc x) (m ∷ ρ) = singleton-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) ∎ - comp-correct : ∀ v w (ρ : Env n) → ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) comp-correct [] [] ρ = sym (identityˡ _) comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _) + trans (∙-congˡ (comp-correct v w ρ)) (∙-distrˡ-∙ _ _ _) comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) = trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈xy∙z _ _ _) comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) = @@ -124,14 +120,14 @@ comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = -- A normaliser. normalise : Expr n → Normal n -normalise (var x) = sg x +normalise (var x) = singleton 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 (var x) ρ = singleton-correct x ρ correct id ρ = empty-correct ρ correct (e₁ ⊕ e₂) ρ = begin ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ @@ -155,3 +151,18 @@ 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." +#-} +sg = singleton +{-# WARNING_ON_USAGE sg +"Warning: sg was deprecated in v2.2. +Please use singleton instead." +#-} +sg-correct = singleton-correct +{-# WARNING_ON_USAGE sg-correct +"Warning: sg-correct was deprecated in v2.2. +Please use singleton-correct instead." +#-} From ec9888803979f0c6dc61df0cd9fdc4986bccb8ab Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 11:11:40 +0100 Subject: [PATCH 22/26] fixed exports of `Normal` form instantiations --- src/Algebra/Solver/CommutativeMonoid.agda | 5 ++++- src/Algebra/Solver/IdempotentCommutativeMonoid.agda | 12 ++++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 03ffeba82c..9316418660 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -17,11 +17,14 @@ import Algebra.Solver.Monoid.Solver as Solver open CommutativeMonoid M using (monoid) +private + module N = Normal M + ------------------------------------------------------------------------ -- Normal forms -open module N = Normal M public +open N public renaming (correct to normalise-correct) ------------------------------------------------------------------------ diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 922c735f41..d5cac0585f 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -14,20 +14,24 @@ module Algebra.Solver.IdempotentCommutativeMonoid {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal -import Algebra.Solver.Monoid.Tactic as Tactic +import Algebra.Solver.Monoid.Solver as Solver open IdempotentCommutativeMonoid M using (monoid) +private + module N = Normal M + + ------------------------------------------------------------------------ -- Normal forms -open module N = Normal M public +open N public renaming (correct to normalise-correct) ------------------------------------------------------------------------ --- Tactic +-- Proof procedures -open Tactic monoid (record { N }) public +open Solver monoid (record { N }) public ------------------------------------------------------------------------ From 45379e64536fcf473122a4076297bf8d0cb3a673 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 11:16:47 +0100 Subject: [PATCH 23/26] fixed exports of `Solver` --- src/Algebra/Solver/Monoid.agda | 9 ++++++--- src/Algebra/Solver/Monoid/Solver.agda | 1 + 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 3708d7b5e3..f0ee5ca799 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -11,23 +11,26 @@ open import Algebra.Bundles using (Monoid) module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where import Algebra.Solver.Monoid.Normal as Normal -import Algebra.Solver.Monoid.Tactic as Tactic +import Algebra.Solver.Monoid.Solver as Solver open import Data.Maybe.Base as Maybe using (From-just; from-just) open import Data.Product.Base using (_×_; uncurry) open import Function.Base using (_∘_) +private + module N = Normal M + ------------------------------------------------------------------------ -- Normal forms -open module N = Normal M public +open N public renaming (comp-correct to homomorphic; correct to normalise-correct) ------------------------------------------------------------------------ -- Tactic -open module T = Tactic M (record { N }) public +open Solver M (record { N }) public hiding (prove) prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es) diff --git a/src/Algebra/Solver/Monoid/Solver.agda b/src/Algebra/Solver/Monoid/Solver.agda index a692d5c7bf..a1281e9639 100644 --- a/src/Algebra/Solver/Monoid/Solver.agda +++ b/src/Algebra/Solver/Monoid/Solver.agda @@ -30,6 +30,7 @@ private module R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct + ------------------------------------------------------------------------ -- Proof procedures From e1c3ab17aa155294606a2ae6cd9118f93f4f28ac Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 11:54:02 +0100 Subject: [PATCH 24/26] fixed deprecations in `CHANGELOG` --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c1d147dcdb..5027b5e297 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,12 +27,17 @@ Deprecated names * 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`: From 07e005aeb549b0235150ea6a13c7fca3c1aba202 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 12:01:42 +0100 Subject: [PATCH 25/26] note on import strategy in `CHANGELOG` --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5027b5e297..71685bdf1b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -78,6 +78,8 @@ New modules Algebra.Solver.Monoid.Tactic ``` + 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 ----------------------------- From a0572d5968afb018e84508359aa112f1186770aa Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 Aug 2024 12:03:12 +0100 Subject: [PATCH 26/26] name of `Solver` module --- CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 71685bdf1b..ecdb495953 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -68,14 +68,14 @@ New modules ``` * Refactoring of the `Algebra.Solver.*Monoid` implementations, via - a single `Tactic` module API based on the existing `Expr`, and + 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.Tactic + 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`.