diff --git a/Class/MonadError.agda b/Class/MonadError.agda index e806a46..20f6e3a 100644 --- a/Class/MonadError.agda +++ b/Class/MonadError.agda @@ -16,6 +16,10 @@ record MonadError (E : Set e) (M : ∀ {f} → Set f → Set f) : Setω where error : E → M A catch : M A → (E → M A) → M A + instance + Alternative-M : Alternative M + Alternative-M = record { _<|>_ = λ x y → catch x (λ _ → y) } + open MonadError MonadError-TC : MonadError (List ErrorPart) TC diff --git a/Reflection/Utils/Args.agda b/Reflection/Utils/Args.agda index 4126bc3..f6f735a 100644 --- a/Reflection/Utils/Args.agda +++ b/Reflection/Utils/Args.agda @@ -4,13 +4,21 @@ module Reflection.Utils.Args where open import Meta.Prelude open import Meta.Init -open import Data.List using (map; zip) +open import Data.List using (map; zip; reverse; length) open import Data.Fin using (toℕ) +open import Data.Vec.Base using (Vec; []; _∷_) +import Data.Vec.Base as Vec +import Data.Maybe as Maybe open import Relation.Nullary using (Dec) open import Reflection.AST.Argument.Information import Reflection.AST.Argument.Visibility as Vis +takeFirst : ∀ {ℓ} {A : Set ℓ} (n : ℕ) → List A → Maybe (Vec A n) +takeFirst zero _ = just [] +takeFirst (suc _) [] = nothing +takeFirst (suc n) (x ∷ xs) = Maybe.map (x ∷_) (takeFirst n xs) + getVisibility : Arg A → Visibility getVisibility (arg (arg-info v _) _) = v @@ -33,6 +41,17 @@ vArgs = λ where (vArg x ∷ xs) → x ∷ vArgs xs (_ ∷ xs) → vArgs xs +visibleCount : Args A → ℕ +visibleCount = length ∘ vArgs + +-- Take the last `n` visible arguments of a `def`. Returns `nothing` +-- if the term isn't a `def` or has fewer than `n` visible +-- arguments. Hidden arguments and any leading visible arguments +-- beyond the last `n` are skipped. +getVisibleArgs : ∀ n → Term → Maybe (Vec Term n) +getVisibleArgs n (def _ xs) = Maybe.map Vec.reverse (takeFirst n (reverse (vArgs xs))) +getVisibleArgs _ _ = nothing + argInfo : Arg A → ArgInfo argInfo (arg i _) = i diff --git a/Reflection/Utils/Core.agda b/Reflection/Utils/Core.agda index 52c072f..f82b278 100644 --- a/Reflection/Utils/Core.agda +++ b/Reflection/Utils/Core.agda @@ -5,7 +5,13 @@ open import Meta.Prelude open import Meta.Init open import Data.Product using (map₁) -open import Data.List using (map) +open import Data.List using (map; findIndexᵇ) +import Data.List as List +import Data.Maybe as Maybe +import Data.Fin as Fin +import Reflection.AST.Name as Name +open import Reflection.AST.AlphaEquality using (_=α=_) +open import Reflection.AST.Literal using (nat) import Reflection.AST.Abstraction as Abs import Reflection.AST.Argument as Arg @@ -21,6 +27,34 @@ tyName = λ where (def n _) → just n _ → nothing +insertName : Name → List Name → List Name +insertName n [] = n ∷ [] +insertName n (m ∷ ms) = if n Name.≡ᵇ m then m ∷ ms else m ∷ insertName n ms + +-- Insert the def-name of `t` to `xs`, η-contract if required +pickDefName : Term → List Name → List Name +pickDefName (def n _) xs = insertName n xs +pickDefName (lam _ (abs _ body)) xs = pickDefName body xs +pickDefName _ xs = xs + +-- Extract a `ℕ` value from a term shaped as `lit (nat n)` or a chain +-- of `suc`/`zero` constructors. +extractNat : Term → Maybe ℕ +extractNat (lit (nat n)) = just n +extractNat (quote ℕ.zero ◆) = just 0 +extractNat (quote ℕ.suc ◆⟦ x ⟧) = Maybe.map ℕ.suc (extractNat x) +extractNat _ = nothing + +-- ** atom-table helpers (α-equality based) + +insertAtom : Term → List Term → List Term +insertAtom t [] = t ∷ [] +insertAtom t (a ∷ as) = if t =α= a then a ∷ as else a ∷ insertAtom t as + +-- Look up `t`'s index in `xs` up to α-equality +findAtomIndex : Term → List Term → Maybe ℕ +findAtomIndex t xs = Maybe.map Fin.toℕ (findIndexᵇ (t =α=_) xs) + -- ** alternative view of function types as a pair of a list of arguments and a return type TypeView = List (Abs (Arg Type)) × Type diff --git a/Reflection/Utils/Metas.agda b/Reflection/Utils/Metas.agda index 51581cb..3487c7a 100644 --- a/Reflection/Utils/Metas.agda +++ b/Reflection/Utils/Metas.agda @@ -4,7 +4,9 @@ module Reflection.Utils.Metas where open import Meta.Prelude open import Meta.Init -open import Data.List using (_++_) +import Data.Bool.ListAction as B +open import Data.List +import Reflection.AST.Meta as Meta isMeta : Term → Bool isMeta = λ where @@ -35,3 +37,16 @@ mutual [] → [] (clause _ _ t ∷ c) → findMetas t ++ findMetasCl c (absurd-clause _ _ ∷ c) → findMetasCl c + +metaId : Term → Maybe Meta +metaId (meta x _) = just x +metaId _ = nothing + +findMetaIds : Term → List Meta +findMetaIds = mapMaybe metaId ∘ findMetas + +firstMeta : Term → Maybe Meta +firstMeta = head ∘ findMetaIds + +shareMeta : List Meta → List Meta → Bool +shareMeta xs ys = B.any (λ x → B.any (Meta._≡ᵇ_ x) ys) xs diff --git a/Reflection/Utils/TCM.agda b/Reflection/Utils/TCM.agda index 6f872ef..b50162e 100644 --- a/Reflection/Utils/TCM.agda +++ b/Reflection/Utils/TCM.agda @@ -9,3 +9,65 @@ import Class.MonadReader as C import Class.MonadTC as C open import Reflection.Utils.TCI {TC} ⦃ C.Monad-TC ⦄ ⦃ C.MonadError-TC ⦄ ⦃ record { ask = C.initTCEnv ; local = λ _ x → x } ⦄ ⦃ C.MonadTC-TC ⦄ public + +open import Meta.Prelude +open import Reflection.AST.Term using (clause) +open import Reflection.AST.Definition using (function) +open import Reflection.AST.AlphaEquality using (_=α=_) +import Agda.Builtin.Reflection as B using (withReduceDefs) + +-- Depth-limited weak-head reduction that unfolds one `def` at a time. +-- +-- Each step head-reduces every argument first, then asks Agda's +-- `reduce` to unfold *only* the outer `def`. Stops at a fixed point +-- or when fuel runs out. More aggressive than `reduce` (which won't +-- chase a chain of `def x = def y = …`) but more controlled than +-- `normalise`. +-- +-- The argument pass is required to reduce record projections, so that +-- when the outer def is a projection, `reduce` can compute it cleanly +-- instead of falling back to inlining the projection's whole body. +-- +-- It's a bit awkward that we only reduce the `nm` in the case with no +-- arguments, but this is the only configuration I've found that makes +-- the ring solver work. + +mutual + headReduce : ℕ → Term → TC Term + headReduce 0 t = pure t + headReduce (suc k) (def nm []) = do + d ← getDefinition nm + case d of λ where + (function (clause [] [] body ∷ _)) → headReduce k body + _ → pure (def nm []) + headReduce (suc k) (def nm args) = do + args' ← reduceArgs k args + t' ← B.withReduceDefs (true , nm ∷ []) (reduce (def nm args')) + if t' =α= def nm args' + then pure t' -- no progress + else headReduce k t' + headReduce (suc _) t = pure t + + reduceArgs : ℕ → Args Term → TC (Args Term) + reduceArgs _ [] = pure [] + reduceArgs k (arg i t ∷ as) = do + t' ← headReduce k t + as' ← reduceArgs k as + pure (arg i t' ∷ as') + +-- Like `headReduce`, but stops at a nullary `def` whose body is not +-- itself a nullary `def`. +headReducePeel : ℕ → Term → TC Term +headReducePeel 0 t = pure t +headReducePeel (suc k) t@(def nm []) = do + d ← getDefinition nm + case d of λ where + (function (clause [] [] body@(def _ []) ∷ _)) → headReducePeel k body + _ → pure t +headReducePeel (suc k) (def nm args) = do + args' ← reduceArgs k args + t' ← B.withReduceDefs (true , nm ∷ []) (reduce (def nm args')) + if t' =α= def nm args' + then pure t' + else headReducePeel k t' +headReducePeel (suc _) t = pure t diff --git a/Tactic.agda b/Tactic.agda index c13e87a..9d2c8f9 100644 --- a/Tactic.agda +++ b/Tactic.agda @@ -22,3 +22,6 @@ open import Tactic.Derive.DecEqFast open import Tactic.Derive.Show public open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests open import Tactic.Derive.Convertible public + +open import Tactic.Solver.Ring +open import Tactic.Solver.Ring.Tests diff --git a/Tactic/Solver/Algebra.agda b/Tactic/Solver/Algebra.agda new file mode 100644 index 0000000..afeccd4 --- /dev/null +++ b/Tactic/Solver/Algebra.agda @@ -0,0 +1,335 @@ +------------------------------------------------------------------------ +-- Generic core for reflection-based algebraic-structure solvers. +-- +-- A `Theory` describes a particular algebraic structure by giving: +-- * the bundle type `R` is expected to inhabit; +-- * its operators (arities + Term patterns to detect them); +-- * an optional `LiteralMatch` for theories with literals; +-- * how to encode them into a backend polynomial AST. + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.Algebra where + +open import Agda.Builtin.Reflection using (withReduceDefs) + +open import Data.Bool +open import Data.List as List using (List; _∷_; []; _++_; replicate; null) +open import Data.Maybe as Maybe using (Maybe; just; nothing) +open import Data.Nat +open import Data.Nat.Reflection +open import Data.Product +open import Data.Unit +open import Data.Vec using (_∷_; []) + +open import Function + +open import Reflection +open import Reflection.AST.Argument +open import Reflection.AST.DeBruijn +import Reflection.AST.Name as Name +open import Reflection.AST.Term +open import Reflection.TCM.Syntax +open import Reflection.Utils.Args +open import Reflection.Utils.Core +open import Reflection.Utils.Metas +open import Reflection.Utils.TCM + +------------------------------------------------------------------------ +-- I. Reflection helpers + +-- Peels leading λ-binders before reading the head Name. +headName : Term → Maybe Name +headName (def nm _) = just nm +headName (lam _ (abs _ body)) = headName body +headName _ = nothing + +_≡ᵐ_ : Maybe Name → Maybe Name → Bool +just n ≡ᵐ just m = n Name.≡ᵇ m +nothing ≡ᵐ nothing = true +_ ≡ᵐ _ = false + +-- For wrapped numeric carriers like ℤ's `+_`: peel one `con C (n ∷ [])` layer. +peelLitCon : Name → Term → Maybe ℕ +peelLitCon C (con nm xs) = case nm Name.≡ᵇ C of λ where + false → nothing + true → case vArgs xs of λ where + (a ∷ []) → extractNat a + _ → nothing +peelLitCon _ _ = nothing + +extractCarrierNat : Maybe Name → Term → Maybe ℕ +extractCarrierNat mC t = case extractNat t of λ where + (just n) → just n + nothing → case mC of λ where + (just C) → peelLitCon C t + nothing → nothing + +------------------------------------------------------------------------ +-- II. Theory specification. +-- +-- `detect` and `encode` are separated so the macro can collect atoms +-- (which needs operator detection only) before the atom count is +-- known (which `encode` needs). + +record OperatorMatch : Set where + constructor opMatch + field + opTerm : Term + arity : ℕ + +-- For theories with literal coefficients (the ring solvers). Other +-- theories supply `nothing`. +record LiteralMatch : Set where + constructor litMatch + field + -- ℤ-style wrapper (e.g. ℤ's `+_`); `nothing` for unwrapped ℕ-style. + litCon : Maybe Name + peelSuc : Bool + +record TheoryDetect : Set where + field + -- The order chosen here is the source of truth: `opEncoders` in + -- `TheoryEncode` must use the same order. + operatorMatches : List OperatorMatch + -- Names to feed `withReduceDefs` so the operator boundary stays + -- opaque while the macro inspects the user's term. + blockedNames : List Name + literalMatch : Maybe LiteralMatch + +record TheoryEncode : Set where + field + -- Parallel to `TheoryDetect.operatorMatches`. + opEncoders : List (List Term → Term) + encodeNat : ℕ → Term + -- Maps `suc t` to the polynomial Term for `1 + t`. + sucPeel : Term → Term + encodeVar : ℕ → Term + encodeEq : Term → Term → Term + -- Body has `numAtoms` polynomial-var binders introduced. + finishSolve : (lambdaBody : Term) (atoms : List Term) → Term + +-- Operator match paired with its encoder. +record OperatorEntry : Set where + field + opTerm : Term + arity : ℕ + encode : List Term → Term + +mkOperatorEntry : OperatorMatch → (List Term → Term) → OperatorEntry +mkOperatorEntry (opMatch t a) enc = record { opTerm = t ; arity = a ; encode = enc } + +record Theory : Set₁ where + field + bundleType : Term + State : Set + detect : Term → TC (TheoryDetect × State) + -- R↓↓ = R weakened past `numPiVars + numAtoms` lambdas (used + -- inside the polynomial-λ body). + -- R↓ = R weakened past `numPiVars` (used outside, by `finishSolve`). + encode : (R↓↓ R↓ : Term) (numAtoms : ℕ) (state : State) → TheoryEncode + +------------------------------------------------------------------------ +-- III. Operator classification and conversion. + +-- Generic classifier: pick the first entry whose `opTerm` has `nm` +-- as its (lambda-peeled) head `def`. +classifyOp : ∀ {A : Set} → (A → Term) → List A → Name → Maybe A +classifyOp _ [] _ = nothing +classifyOp getTerm (a ∷ as) nm = + if just nm ≡ᵐ headName (getTerm a) + then just a + else classifyOp getTerm as nm + +-- A projected operator like `def CSR._+_ (R ⟨∷⟩ a ⟨∷⟩ b ⟨∷⟩ [])` +-- carries the bundle as a leading visible arg; this returns how many +-- such prefix args to skip before reaching the operator's last +-- `arity` visibles. +opDrop : ℕ → Args Term → ℕ +opDrop arity xs = visibleCount xs ∸ arity + +convertTerm : TheoryDetect → TheoryEncode → (Term → TC Term) → Term → TC Term +convertTerm det enc fallback = convert + where + open TheoryDetect det + open TheoryEncode enc + + ops : List OperatorEntry + ops = List.zipWith mkOperatorEntry operatorMatches opEncoders + + litCon : Maybe Name + litCon = Maybe.maybe LiteralMatch.litCon nothing literalMatch + + peelSuc-on : Bool + peelSuc-on = Maybe.maybe LiteralMatch.peelSuc false literalMatch + + mutual + convert : Term → TC Term + convert t = case (literalMatch , extractCarrierNat litCon t) of λ where + (just _ , just n) → pure (encodeNat n) + _ → convertHead t + + convertHead : Term → TC Term + convertHead t@(def nm xs) = case classifyOp OperatorEntry.opTerm ops nm of λ where + nothing → fallback t + (just e) → do + let open OperatorEntry e + args ← convertVisibleArgs (opDrop arity xs) xs + pure (encode args) + convertHead t@(con (quote suc) (arg (arg-info visible _) x ∷ [])) = + if peelSuc-on then sucPeel <$> convert x else fallback t + convertHead t = fallback t + + convertVisibleArgs : ℕ → Args Term → TC (List Term) + convertVisibleArgs _ [] = pure [] + convertVisibleArgs (suc d) (arg (arg-info visible _) _ ∷ xs) = convertVisibleArgs d xs + convertVisibleArgs 0 (arg (arg-info visible _) x ∷ xs) = do + x' ← convert x + xs' ← convertVisibleArgs 0 xs + pure (x' ∷ xs') + convertVisibleArgs d (_ ∷ xs) = convertVisibleArgs d xs + +collectAtoms : TheoryDetect → Term → List Term → TC (List Term) +collectAtoms det = collect + where + open TheoryDetect det + + litCon : Maybe Name + litCon = Maybe.maybe LiteralMatch.litCon nothing literalMatch + + peelSuc-on : Bool + peelSuc-on = Maybe.maybe LiteralMatch.peelSuc false literalMatch + + mutual + collect : Term → List Term → TC (List Term) + collect t acc = case (literalMatch , extractCarrierNat litCon t) of λ where + (just _ , just _) → pure acc + _ → collectHead t acc + + collectHead : Term → List Term → TC (List Term) + collectHead (def nm xs) acc = case classifyOp OperatorMatch.opTerm operatorMatches nm of λ where + nothing → pure (insertAtom (def nm xs) acc) + (just (opMatch _ arity)) → collectArgs (opDrop arity xs) xs acc + collectHead t@(con (quote suc) ((arg (arg-info visible _) x ∷ []))) acc = + if peelSuc-on then collect x acc else pure (insertAtom t acc) + collectHead t acc = pure (insertAtom t acc) + + collectArgs : ℕ → Args Term → List Term → TC (List Term) + collectArgs _ [] acc = pure acc + collectArgs (suc d) (arg (arg-info visible _) _ ∷ xs) acc = collectArgs d xs acc + collectArgs 0 (arg (arg-info visible _) x ∷ xs) acc = collect x acc >>= collectArgs 0 xs + collectArgs d (_ ∷ xs) acc = collectArgs d xs acc + +-- Used to seed `withReduceDefs`'s block list with the operator +-- names we'll encounter. +collectOpNames : TheoryDetect → Term → List Name → TC (List Name) +collectOpNames det = collect + where + open TheoryDetect det + + mutual + collect : Term → List Name → TC (List Name) + collect (def nm xs) acc = case classifyOp OperatorMatch.opTerm operatorMatches nm of λ where + nothing → pure acc + (just (opMatch _ arity)) → collectArgs (opDrop arity xs) xs (insertName nm acc) + collect _ acc = pure acc + + collectArgs : ℕ → Args Term → List Name → TC (List Name) + collectArgs _ [] acc = pure acc + collectArgs (suc d) (arg (arg-info visible _) _ ∷ xs) acc = collectArgs d xs acc + collectArgs 0 (arg (arg-info visible _) x ∷ xs) acc = collect x acc >>= collectArgs 0 xs + collectArgs d (_ ∷ xs) acc = collectArgs d xs acc + +------------------------------------------------------------------------ +-- IV. The generic macro core. + +malformedClosedEqError : ∀ {a} {A : Set a} → Term → TC A +malformedClosedEqError found = typeError + ( strErr "Malformed call to algebraic solver." + ∷ strErr "Expected target type to be of shape LHS ≈ RHS." + ∷ strErr "Instead: " + ∷ termErr found + ∷ []) + +-- The `nothing` branch is unreachable on well-formed input — +-- `collectAtoms` already inserted every term `convertTerm` will +-- look up — but we error loudly rather than silently emit a default. +private + atomFB : TheoryEncode → List Term → Term → TC Term + atomFB enc atoms t = do + just i ← pure (findAtomIndex t atoms) + where nothing → typeError + ( strErr "Internal error in solve-≈: atom " + ∷ termErr t + ∷ strErr " was not found in the atom list." + ∷ []) + pure (TheoryEncode.encodeVar enc i) + +-- Precondition: `R` has been type-checked against `Theory.bundleType` +-- by the caller (e.g. via `Tactic.Solver.Ring.detectSide`). +solveByTheory : (thy : Theory) → Term → Term → TC ⊤ +solveByTheory thy `R hole = do + det , state ← Theory.detect thy `R + let bundleNs = TheoryDetect.blockedNames det + + `hole₀ ← inferType hole + let _ , equation₀ = stripPis `hole₀ + opNames ← case getVisibleArgs 2 equation₀ of λ where + (just (lhs₀ ∷ rhs₀ ∷ [])) → collectOpNames det lhs₀ bundleNs >>= collectOpNames det rhs₀ + _ → pure bundleNs + + withReduceDefs (false , opNames) $ do + -- `normalise`, not `reduce`: Agda's elaborator can leave the + -- goal type wrapped in lambdas that need β-reducing first. + `hole ← normalise `hole₀ + let variablesAndTypes , equation = stripPis `hole + let sides = getVisibleArgs 2 equation + + -- Deadlock detection: if some side has a meta not shared with + -- the other side, `blockOnMeta` would retry forever (only this + -- macro could resolve it). Shared metas are fine — Agda + -- propagates constraints across `≈`. + case sides of λ where + (just (lhs ∷ rhs ∷ [])) → do + let bothStructured = not (isMeta lhs) ∧ not (isMeta rhs) + let metasL = findMetaIds lhs + let metasR = findMetaIds rhs + let anyMetas = not (null metasL ∧ null metasR) + let sharedMeta = shareMeta metasL metasR + if bothStructured ∧ anyMetas ∧ not sharedMeta + then typeError + ( strErr "solve-≈: the goal `LHS ≈ RHS` has at least one side " + ∷ strErr "containing a metavariable that could not be resolved. To run this " + ∷ strErr "solver you must add type annotations to resolve these variables." + ∷ []) + else pure tt + _ → pure tt + + case firstMeta `hole of λ where + (just m) → blockOnMeta m + nothing → pure tt + let variables = List.map proj₁ variablesAndTypes + let numPiVars = List.length variables + + just (lhs ∷ rhs ∷ []) ← pure sides + where nothing → malformedClosedEqError `hole + + atoms₀ ← collectAtoms det lhs [] + atoms ← collectAtoms det rhs atoms₀ + let numAtoms = List.length atoms + + let `R↓↓ = weaken (numPiVars + numAtoms) `R + let `R↓ = weaken numPiVars `R + let enc = Theory.encode thy `R↓↓ `R↓ numAtoms state + + `lhsExpr ← convertTerm det enc (atomFB enc atoms) lhs + `rhsExpr ← convertTerm det enc (atomFB enc atoms) rhs + + let open TheoryEncode enc + let lambdaBody = encodeEq `lhsExpr `rhsExpr + let f = prependVLams (replicate numAtoms "x") lambdaBody + let solverCall = finishSolve f atoms + + -- Re-introduce the pi-binders the user didn't pattern-bind. + let final = prependVLams variables solverCall + unify hole final diff --git a/Tactic/Solver/Ring.agda b/Tactic/Solver/Ring.agda new file mode 100644 index 0000000..b4abe59 --- /dev/null +++ b/Tactic/Solver/Ring.agda @@ -0,0 +1,393 @@ +------------------------------------------------------------------------ +-- A reflection-based ring solver. +-- +-- `solve-≈` accepts either a `CommutativeSemiring` or a +-- `CommutativeRing` and dispatches to the appropriate backend: +-- * CSR → `Algebra.Solver.Ring.NaturalCoefficients.Default R` +-- (ℕ coefficients, no negation); +-- * CR → `Tactic.Solver.Ring.IntegerCoefficients R` (ℤ +-- coefficients, real negation; recognises `_-_` and `-_`). +-- +-- Built on `Tactic.Solver.Algebra`. For a new structure (monoid, +-- lattice, …), write a fresh `Theory` and macro alongside this one. + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.Ring where + +open import Algebra using (CommutativeSemiring; CommutativeRing) + +open import Data.Bool using (Bool; true; false) +open import Data.Fin using (Fin) +open import Data.Integer using (ℤ; +_) +open import Data.List as List using (List; _∷_; []; map; foldr; length; drop; zip; filterᵇ; reverse) +open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe) +open import Data.Nat using (ℕ; suc; zero) +import Data.Vec as Vec +open import Data.Nat.Reflection +open import Data.Product using (_,_; _×_; proj₁; proj₂; uncurry) +open import Data.Unit + +open import Function + +open import Class.Functor +open import Class.Monad.Instances +open import Class.Traversable + +open import Reflection +open import Reflection.AST.Argument +import Reflection.AST.Name as Name +open import Reflection.AST.Term +open import Reflection.TCM.Syntax hiding (_<$>_) +open import Reflection.Utils.Args using (vArgs; takeFirst) +open import Reflection.Utils.Core using (extractNat; pickDefName) +open import Reflection.Utils.TCM using (headReduce; headReducePeel) + +open import Tactic.Solver.Algebra +import Tactic.Solver.Ring.IntegerCoefficients as IntC + +------------------------------------------------------------------------ +-- `Algebra.Solver.Ring.Polynomial`'s `con`, `var`, and `:-_` are +-- nested constructors inside a four-parameter module. Defining +-- top-level aliases lets the macro reflect them by name (with just +-- `R` as the visible argument) rather than reconstructing all four +-- module parameters. + +module Solver {c ℓ} (R : CommutativeSemiring c ℓ) where + open import Algebra.Solver.Ring.NaturalCoefficients.Default R public + + conP : ∀ {n} → ℕ → Polynomial n + conP = con + + varP : ∀ {n} → Fin n → Polynomial n + varP = var + +------------------------------------------------------------------------ +-- Backend reflection helpers (private). + +private + data RingSide : Set where + csr cr : RingSide + + data LitStyle : Set where + natStyle : LitStyle -- bare ℕ literals; peel `suc`. + wrapped : Name → LitStyle -- `con C ⟨ n ⟩` (e.g. ℤ's `+_`). + + -- Threaded from `detect` to `encode`. + record RingState : Set where + field + litStyle : Maybe LitStyle + +------------------------------------------------------------------------ +-- Operator-projection Terms from the user's bundle. + +private + projTerm : Name → Term → Term + projTerm nm R = def nm (2 ⋯⟅∷⟆ R ⟨∷⟩ []) + + csrAdd csrMul csrZero csrOne : Name + csrAdd = quote CommutativeSemiring._+_ + csrMul = quote CommutativeSemiring._*_ + csrZero = quote CommutativeSemiring.0# + csrOne = quote CommutativeSemiring.1# + + crAdd crMul crSub crNeg crZero crOne : Name + crAdd = quote CommutativeRing._+_ + crMul = quote CommutativeRing._*_ + crSub = quote CommutativeRing._-_ + crNeg = quote (CommutativeRing.-_) + crZero = quote CommutativeRing.0# + crOne = quote CommutativeRing.1# + + bundleTypeOf : RingSide → Term + bundleTypeOf csr = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) + bundleTypeOf cr = def (quote CommutativeRing) (2 ⋯⟨∷⟩ []) + +------------------------------------------------------------------------ +-- Polynomial-AST Term builders. Calling shape: +-- `def NAME (2 hidden + R-bundle ⟨∷⟩ numVars ⟅∷⟆ ⟨args…⟩)`, +-- pulling NAMEs from `Solver.*` for CSR and `IntC.*` for CR. + +private + defP : (R `n : Term) → Name → List (Arg Term) → Term + defP R `n nm args = + def nm (2 ⋯⟅∷⟆ R ⟨∷⟩ `n ⟅∷⟆ args) + + conName varName addName mulName eqName solveName reflName + : RingSide → Name + conName csr = quote Solver.conP ; conName cr = quote IntC.conP + varName csr = quote Solver.varP ; varName cr = quote IntC.varP + addName csr = quote Solver._:+_ ; addName cr = quote IntC._:+_ + mulName csr = quote Solver._:*_ ; mulName cr = quote IntC._:*_ + eqName csr = quote Solver._:=_ ; eqName cr = quote IntC._:=_ + solveName csr = quote Solver.solve ; solveName cr = quote IntC.solve + reflName csr = quote CommutativeSemiring.refl + reflName cr = quote CommutativeRing.refl + + `con : RingSide → (R `n : Term) → Term → Term + `con s R `n c = defP R `n (conName s) (c ⟨∷⟩ []) + + `var : RingSide → (R `n : Term) → Term → Term + `var s R `n i = defP R `n (varName s) (i ⟨∷⟩ []) + + `:+ : RingSide → (R `n : Term) → Term → Term → Term + `:+ s R `n x y = defP R `n (addName s) (x ⟨∷⟩ y ⟨∷⟩ []) + + `:* : RingSide → (R `n : Term) → Term → Term → Term + `:* s R `n x y = defP R `n (mulName s) (x ⟨∷⟩ y ⟨∷⟩ []) + + `:- : (R `n : Term) → Term → Term → Term + `:- R `n x y = defP R `n (quote IntC._:-_) (x ⟨∷⟩ y ⟨∷⟩ []) + + `:-‿ : (R `n : Term) → Term → Term + `:-‿ R `n x = defP R `n (quote IntC.negP) (x ⟨∷⟩ []) + + `:= : RingSide → (R `n : Term) → Term → Term → Term + `:= s R `n x y = defP R `n (eqName s) (x ⟨∷⟩ y ⟨∷⟩ []) + + `refl : RingSide → (R : Term) → Term + `refl s R = def (reflName s) (2 ⋯⟅∷⟆ R ⟨∷⟩ 1 ⋯⟅∷⟆ []) + +------------------------------------------------------------------------ +-- Literal-style recognition from the bundle's `0#` and `1#` Terms. + +private + detectLitStyle : Term → Term → Maybe LitStyle + detectLitStyle (con cz argsZ) (con co argsO) = + case (cz Name.≡ᵇ co) of λ where + true → case (vArgs argsZ , vArgs argsO) of λ where + ((z₀ ∷ []) , (o₀ ∷ [])) → case (extractNat z₀ , extractNat o₀) of λ where + (just 0 , just 1) → just (wrapped cz) + _ → fallthrough + _ → fallthrough + false → fallthrough + where + fallthrough : Maybe LitStyle + fallthrough = case (extractNat (con cz argsZ) , extractNat (con co argsO)) of λ where + (just 0 , just 1) → just natStyle + _ → nothing + detectLitStyle z o = case (extractNat z , extractNat o) of λ where + (just 0 , just 1) → just natStyle + _ → nothing + +------------------------------------------------------------------------ +-- Operator detection: concrete record peek + abstract-projection +-- fallback. + +private + collectDefNames : List Term → List Name + collectDefNames = List.foldr pickDefName [] + + -- A slot's role. `op` is a generic concrete operator field; + -- `derived` is additional syntax that isn't a field; `zeroLit` and + -- `oneLit` mark literals. + data SlotKind : Set where + op zeroLit oneLit derived : SlotKind + + -- An operator slot: `(projection-name , arity , kind)`. The slot + -- order is the source of truth for `operatorMatches` (and so must + -- align with `opEncoders` in `mkEncode`). + Slot : Set + Slot = Name × ℕ × SlotKind + + slotProj : Slot → Name + slotProj s = proj₁ s + + slotArity : Slot → ℕ + slotArity s = proj₁ (proj₂ s) + + slotKind : Slot → SlotKind + slotKind s = proj₂ (proj₂ s) + + slotIsConcrete : Slot → Bool + slotIsConcrete s with slotKind s + ... | derived = false + ... | _ = true + + csrSlots : List Slot + csrSlots = (csrAdd , 2 , op) + ∷ (csrMul , 2 , op) + ∷ (csrZero , 0 , zeroLit) + ∷ (csrOne , 0 , oneLit) + ∷ [] + + crSlots : List Slot + crSlots = (crAdd , 2 , op) + ∷ (crMul , 2 , op) + ∷ (crSub , 2 , derived) + ∷ (crNeg , 1 , op) + ∷ (crZero , 0 , zeroLit) + ∷ (crOne , 0 , oneLit) + ∷ [] + + slotsFor : RingSide → List Slot + slotsFor csr = csrSlots + slotsFor cr = crSlots + + mkLitMatch : Maybe LitStyle → Maybe LiteralMatch + mkLitMatch nothing = nothing + mkLitMatch (just natStyle) = just (litMatch nothing true) + mkLitMatch (just (wrapped C)) = just (litMatch (just C) false) + + -- Pull the `0` and `1` slot Terms by kind. Returns `nothing` if + -- either is missing from the slot list. + findZeroOne : List (Slot × Term) → Maybe (Term × Term) + findZeroOne = go nothing nothing + where + go : Maybe Term → Maybe Term → List (Slot × Term) → Maybe (Term × Term) + go (just z) (just o) _ = just (z , o) + go _ _ [] = nothing + go mz mo ((s , t) ∷ rest) with slotKind s + ... | zeroLit = go (just t) mo rest + ... | oneLit = go mz (just t) rest + ... | _ = go mz mo rest + + detectFor : RingSide → Term → TC (TheoryDetect × RingState) + detectFor side R = do + R' ← headReduce 16 R + let slots = slotsFor side + let concreteN = length (filterᵇ slotIsConcrete slots) + case R' of λ where + (con _ args) → case Maybe.map Vec.toList (takeFirst concreteN (drop 2 (vArgs args))) of λ where + (just rawOps) → do + concOps ← traverse ⦃ Functor-List ⦄ (headReducePeel 16) rawOps + slotted ← zipSlots slots concOps + slottedLit ← traverse ⦃ Functor-List ⦄ (λ (s , t) → (s ,_) <$> headReduce 16 t) slotted + let blockNs = collectDefNames concOps + let ls = maybe (uncurry detectLitStyle) nothing (findZeroOne slottedLit) + pure + ( record + { operatorMatches = List.map (λ (s , t) → opMatch t (slotArity s)) slotted + ; blockedNames = blockNs + ; literalMatch = mkLitMatch ls + } + , record { litStyle = ls } + ) + nothing → abstractPath slots + _ → abstractPath slots + where + zipSlots : List Slot → List Term → TC (List (Slot × Term)) + zipSlots [] _ = pure [] + zipSlots (s ∷ rest) ops = case slotKind s of λ where + derived → do + t ← normalise (projTerm (slotProj s) R) + rs ← zipSlots rest ops + pure ((s , t) ∷ rs) + _ → case ops of λ where + (t ∷ ops') → do + rs ← zipSlots rest ops' + pure ((s , t) ∷ rs) + [] → pure [] + + abstractPath : List Slot → TC (TheoryDetect × RingState) + abstractPath slots = do + ts ← traverse ⦃ Functor-List ⦄ normalise (List.map (λ s → projTerm (slotProj s) R) slots) + pure + ( record + { operatorMatches = List.map (λ (s , t) → opMatch t (slotArity s)) (zip slots ts) + ; blockedNames = [] + ; literalMatch = nothing + } + , record { litStyle = nothing } + ) + +------------------------------------------------------------------------ +-- Encoder construction. + +private + -- ℕ literal `n` rendered at the polynomial-coefficient type: + -- ℕ for CSR (`toTerm n`), ℤ for CR (wrapped with `+_`). + natLitTerm : RingSide → ℕ → Term + natLitTerm csr n = toTerm n + natLitTerm cr n = con (quote +_) (toTerm n ⟨∷⟩ []) + + mkEncode : (s : RingSide) → (R↓↓ R↓ : Term) + → (numAtoms : ℕ) → Maybe LitStyle → TheoryEncode + mkEncode s R↓↓ R↓ numAtoms litStyle = record + { opEncoders = ops s + ; encodeNat = encNat + ; sucPeel = sucPeelFn + ; encodeVar = encVar + ; encodeEq = `:= s R↓↓ `n + ; finishSolve = finish + } + where + `n = toTerm numAtoms + + opAdd : List Term → Term + opAdd (x ∷ y ∷ _) = `:+ s R↓↓ `n x y + opAdd _ = unknown + + opMul : List Term → Term + opMul (x ∷ y ∷ _) = `:* s R↓↓ `n x y + opMul _ = unknown + + opSub : List Term → Term + opSub (x ∷ y ∷ _) = `:- R↓↓ `n x y + opSub _ = unknown + + opNeg : List Term → Term + opNeg (x ∷ _) = `:-‿ R↓↓ `n x + opNeg _ = unknown + + opZero : List Term → Term + opZero _ = `con s R↓↓ `n (natLitTerm s 0) + + opOne : List Term → Term + opOne _ = `con s R↓↓ `n (natLitTerm s 1) + + -- The order here MUST match what `detectCSR`/`detectCR` emit + -- for `operatorMatches`. + ops : RingSide → List (List Term → Term) + ops csr = opAdd ∷ opMul ∷ opZero ∷ opOne ∷ [] + ops cr = opAdd ∷ opMul ∷ opSub ∷ opNeg ∷ opZero ∷ opOne ∷ [] + + encNat : ℕ → Term + encNat n = `con s R↓↓ `n (natLitTerm s n) + + sucPeelFn : Term → Term + sucPeelFn inner = + `:+ s R↓↓ `n (`con s R↓↓ `n (natLitTerm s 1)) inner + + encVar : ℕ → Term + encVar i = `var s R↓↓ `n (toFinTerm i) + + finish : Term → List Term → Term + finish lambdaBody atoms = + def (solveName s) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ `n ⟨∷⟩ lambdaBody ⟨∷⟩ `refl s R↓ ⟨∷⟩ List.map vArg atoms) + +------------------------------------------------------------------------ +-- The macro. + +private + ringTheory : RingSide → Theory + ringTheory s = record + { bundleType = bundleTypeOf s + ; State = RingState + ; detect = detectFor s + ; encode = λ R↓↓ R↓ n st → mkEncode s R↓↓ R↓ n (RingState.litStyle st) + } + + detectSide : Term → TC (RingSide × Term) + detectSide R = + ((cr ,_) <$> checkType R (bundleTypeOf cr)) + <|> ((csr ,_) <$> checkType R (bundleTypeOf csr)) + <|> typeError + ( strErr "solve-≈: the bundle argument must be a " + ∷ strErr "`CommutativeSemiring` or a `CommutativeRing`, but " + ∷ termErr R + ∷ strErr " is neither." + ∷ []) + +solve-≈-macro : Term → Term → TC ⊤ +solve-≈-macro R hole = do + -- `commitTC` locks in `detectSide`'s metavariable resolutions + -- before further work that depends on `R`'s type being settled. + -- `solveByTheory` deliberately doesn't redo the `checkType`. + side , R' ← detectSide R + commitTC + solveByTheory (ringTheory side) R' hole + +macro + solve-≈ : Term → Term → TC ⊤ + solve-≈ = solve-≈-macro diff --git a/Tactic/Solver/Ring/IntegerCoefficients.agda b/Tactic/Solver/Ring/IntegerCoefficients.agda new file mode 100644 index 0000000..56fd37a --- /dev/null +++ b/Tactic/Solver/Ring/IntegerCoefficients.agda @@ -0,0 +1,226 @@ +------------------------------------------------------------------------ +-- Instantiates `Algebra.Solver.Ring` for a `CommutativeRing` using +-- ℤ as the coefficient ring — the CR analogue of stdlib's +-- `Algebra.Solver.Ring.NaturalCoefficients`. The target ACR is +-- `fromCommutativeRing R` (real negation), so the polynomial AST's +-- `:-_` and `_:-_` carry through to genuine ring negation. + +{-# OPTIONS --without-K --safe #-} + +open import Algebra using (CommutativeRing) + +module Tactic.Solver.Ring.IntegerCoefficients + {c ℓ} (R : CommutativeRing c ℓ) where + +open import Algebra.Bundles using (RawRing) +open import Algebra.Solver.Ring.AlmostCommutativeRing + using (AlmostCommutativeRing; fromCommutativeRing ; _-Raw-AlmostCommutative⟶_) +open import Data.Fin.Base using (Fin) +open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; _⊖_; _◃_) +open import Data.Integer.Properties as ℤP + using ([1+m]⊖[1+n]≡m⊖n; +◃n≡+n; _≟_) +open import Data.Maybe.Base using (Maybe; nothing; just) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc) +import Data.Nat.Properties as ℕP +import Data.Sign.Base as Sign +open import Function.Base using (case_of_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Relation.Nullary using (yes; no) + +open CommutativeRing R +-- The TC-optimised `_×_` (= `_×′_`) is essential: its `1 ×′ x = x` +-- special case makes the polynomial-AST `con 1` evaluate to `1#` +-- (and `con 0` to `0#`). The basic `_×_` from +-- `Algebra.Properties.Monoid.Mult` reduces `1 × x` to `x + 0#`, +-- which gives the solver's emitted proofs the wrong shape. +open import Algebra.Properties.Semiring.Mult.TCOptimised semiring + using (_×_; ×-homo-+; ×1-homo-*) +open import Algebra.Properties.Monoid.Mult.TCOptimised +-monoid + using (1+×) +open import Algebra.Properties.Ring ring as RingProps + using (-‿involutive; -0#≈0#; -‿+-comm; -‿distribˡ-*; -‿distribʳ-*) +open import Relation.Binary.Reasoning.Setoid setoid + +R-acr : AlmostCommutativeRing c ℓ +R-acr = fromCommutativeRing R + +------------------------------------------------------------------------ +-- Integer scalar multiplication on the ring. + +infixl 7 _×ᶻ_ + +_×ᶻ_ : ℤ → Carrier → Carrier +(+ n) ×ᶻ x = n × x +(-[1+ n ]) ×ᶻ x = - (suc n × x) + +ℤ-rawRing : RawRing _ _ +ℤ-rawRing = record + { Carrier = ℤ + ; _≈_ = _≡_ + ; _+_ = ℤ._+_ + ; _*_ = ℤ._*_ + ; -_ = ℤ.-_ + ; 0# = + 0 + ; 1# = + 1 + } + +⟦_⟧ : ℤ → Carrier +⟦ z ⟧ = z ×ᶻ 1# + +------------------------------------------------------------------------ +-- The five homomorphism conditions. + +0-homo : ⟦ + 0 ⟧ ≈ 0# +0-homo = refl + +-- `1 ×′ x = x` definitionally (TCOptimised). +1-homo : ⟦ + 1 ⟧ ≈ 1# +1-homo = refl + +-‿homo : ∀ z → ⟦ ℤ.- z ⟧ ≈ - ⟦ z ⟧ +-‿homo (+ zero) = sym -0#≈0# +-‿homo (+ suc n) = refl -- ℤ.-(+ suc n) = -[1+ n] +-‿homo (-[1+ n ]) = sym (-‿involutive _) -- ℤ.-(-[1+ n]) = + suc n + +private + -- Cancels a shared leading `a` on the addition side. + cancel-prefix : ∀ a b c → (a + b) + - (a + c) ≈ b + - c + cancel-prefix a b c = begin + (a + b) + - (a + c) ≈⟨ +-congˡ (sym (-‿+-comm a c)) ⟩ + (a + b) + (- a + - c) ≈⟨ +-assoc a b (- a + - c) ⟩ + a + (b + (- a + - c)) ≈⟨ +-congˡ (sym (+-assoc b (- a) (- c))) ⟩ + a + ((b + - a) + - c) ≈⟨ +-congˡ (+-congʳ (+-comm b (- a))) ⟩ + a + ((- a + b) + - c) ≈⟨ +-congˡ (+-assoc (- a) b (- c)) ⟩ + a + (- a + (b + - c)) ≈⟨ sym (+-assoc a (- a) (b + - c)) ⟩ + (a + - a) + (b + - c) ≈⟨ +-congʳ (-‿inverseʳ a) ⟩ + 0# + (b + - c) ≈⟨ +-identityˡ (b + - c) ⟩ + b + - c ∎ + +-- The asymmetric ℕ-subtraction `_⊖_` is what ℤ's addition uses +-- internally for mixed-sign cases. +⊖-lemma : ∀ m n → (m ⊖ n) ×ᶻ 1# ≈ m × 1# + - (n × 1#) +⊖-lemma zero zero = begin + 0# ≈⟨ sym (+-identityʳ _) ⟩ + 0# + 0# ≈⟨ +-congˡ (sym -0#≈0#) ⟩ + 0# + - 0# ∎ +⊖-lemma (suc m) zero = begin + suc m × 1# ≈⟨ sym (+-identityʳ _) ⟩ + suc m × 1# + 0# ≈⟨ +-congˡ (sym -0#≈0#) ⟩ + suc m × 1# + - 0# ∎ +⊖-lemma zero (suc n) = begin + -(suc n × 1#) ≈⟨ sym (+-identityˡ _) ⟩ + 0# + -(suc n × 1#) ∎ +⊖-lemma (suc m) (suc n) = begin + -- `suc m ⊖ suc n ≡ m ⊖ n`, but `_⊖_` is defined via `_<ᵇ_`/`_∸_` + -- and so the equation isn't definitional — we use the stdlib + -- propositional lemma here. + (suc m ⊖ suc n) ×ᶻ 1# ≡⟨ ≡.cong (_×ᶻ 1#) ([1+m]⊖[1+n]≡m⊖n m n) ⟩ + (m ⊖ n) ×ᶻ 1# ≈⟨ ⊖-lemma m n ⟩ + m × 1# + - (n × 1#) ≈⟨ sym (cancel-prefix 1# (m × 1#) (n × 1#)) ⟩ + (1# + m × 1#) + - (1# + n × 1#) ≈⟨ sym (+-cong (1+× m 1#) (-‿cong (1+× n 1#))) ⟩ + suc m × 1# + - (suc n × 1#) ∎ + ++-homo : ∀ a b → ⟦ a ℤ.+ b ⟧ ≈ ⟦ a ⟧ + ⟦ b ⟧ ++-homo (+ m) (+ n) = ×-homo-+ 1# m n ++-homo (+ m) (-[1+ n ]) = ⊖-lemma m (suc n) ++-homo (-[1+ m ]) (+ n) = begin + (n ⊖ suc m) ×ᶻ 1# ≈⟨ ⊖-lemma n (suc m) ⟩ + n × 1# + - (suc m × 1#) ≈⟨ +-comm _ _ ⟩ + - (suc m × 1#) + n × 1# ∎ ++-homo (-[1+ m ]) (-[1+ n ]) = begin + -[1+ suc (m ℕ.+ n) ] ×ᶻ 1# ≡⟨⟩ + - (suc (suc (m ℕ.+ n)) × 1#) ≡⟨ ≡.cong (λ k → - (k × 1#)) + (≡.cong suc (≡.sym (ℕP.+-suc m n))) ⟩ + - ((suc m ℕ.+ suc n) × 1#) ≈⟨ -‿cong (×-homo-+ 1# (suc m) (suc n)) ⟩ + - (suc m × 1# + suc n × 1#) ≈⟨ sym (-‿+-comm (suc m × 1#) (suc n × 1#)) ⟩ + - (suc m × 1#) + - (suc n × 1#) ∎ + +private + -- `ℤ._*_` is defined uniformly via signs (not pattern-matched on + -- ℤ constructors), so these lemmas project the four sign-case + -- normalisations we need. + + -- `Sign.- ◃ k ≡ ℤ.- (+ k)`. + -◃≡-+ : ∀ k → Sign.- ◃ k ≡ ℤ.- (+ k) + -◃≡-+ zero = ≡.refl + -◃≡-+ (suc _) = ≡.refl + + pos*pos : ∀ m n → (+ m) ℤ.* (+ n) ≡ + (m ℕ.* n) + pos*pos m n = +◃n≡+n (m ℕ.* n) + + pos*neg : ∀ m n → (+ m) ℤ.* (-[1+ n ]) ≡ ℤ.- (+ (m ℕ.* suc n)) + pos*neg m n = -◃≡-+ (m ℕ.* suc n) + + neg*pos : ∀ m n → (-[1+ m ]) ℤ.* (+ n) ≡ ℤ.- (+ (suc m ℕ.* n)) + neg*pos m n = -◃≡-+ (suc m ℕ.* n) + + neg*neg : ∀ m n → (-[1+ m ]) ℤ.* (-[1+ n ]) ≡ + (suc m ℕ.* suc n) + neg*neg m n = +◃n≡+n (suc m ℕ.* suc n) + +*-homo : ∀ a b → ⟦ a ℤ.* b ⟧ ≈ ⟦ a ⟧ * ⟦ b ⟧ +*-homo (+ m) (+ n) = begin + ⟦ (+ m) ℤ.* (+ n) ⟧ ≡⟨ ≡.cong ⟦_⟧ (pos*pos m n) ⟩ + ⟦ + (m ℕ.* n) ⟧ ≡⟨⟩ + (m ℕ.* n) × 1# ≈⟨ ×1-homo-* m n ⟩ + (m × 1#) * (n × 1#) ∎ +*-homo (+ m) (-[1+ n ]) = begin + ⟦ (+ m) ℤ.* (-[1+ n ]) ⟧ ≡⟨ ≡.cong ⟦_⟧ (pos*neg m n) ⟩ + ⟦ ℤ.- (+ (m ℕ.* suc n)) ⟧ ≈⟨ -‿homo (+ (m ℕ.* suc n)) ⟩ + - ⟦ + (m ℕ.* suc n) ⟧ ≡⟨⟩ + - ((m ℕ.* suc n) × 1#) ≈⟨ -‿cong (×1-homo-* m (suc n)) ⟩ + - ((m × 1#) * (suc n × 1#)) ≈⟨ -‿distribʳ-* (m × 1#) (suc n × 1#) ⟩ + (m × 1#) * - (suc n × 1#) ∎ +*-homo (-[1+ m ]) (+ n) = begin + ⟦ (-[1+ m ]) ℤ.* (+ n) ⟧ ≡⟨ ≡.cong ⟦_⟧ (neg*pos m n) ⟩ + ⟦ ℤ.- (+ (suc m ℕ.* n)) ⟧ ≈⟨ -‿homo (+ (suc m ℕ.* n)) ⟩ + - ⟦ + (suc m ℕ.* n) ⟧ ≡⟨⟩ + - ((suc m ℕ.* n) × 1#) ≈⟨ -‿cong (×1-homo-* (suc m) n) ⟩ + - ((suc m × 1#) * (n × 1#)) ≈⟨ -‿distribˡ-* (suc m × 1#) (n × 1#) ⟩ + - (suc m × 1#) * (n × 1#) ∎ +*-homo (-[1+ m ]) (-[1+ n ]) = begin + ⟦ (-[1+ m ]) ℤ.* (-[1+ n ]) ⟧ ≡⟨ ≡.cong ⟦_⟧ (neg*neg m n) ⟩ + ⟦ + (suc m ℕ.* suc n) ⟧ ≡⟨⟩ + (suc m ℕ.* suc n) × 1# ≈⟨ ×1-homo-* (suc m) (suc n) ⟩ + (suc m × 1#) * (suc n × 1#) ≈⟨ sym (-‿involutive _) ⟩ + - (- ((suc m × 1#) * (suc n × 1#))) ≈⟨ -‿cong (-‿distribˡ-* (suc m × 1#) (suc n × 1#)) ⟩ + - (- (suc m × 1#) * (suc n × 1#)) ≈⟨ -‿distribʳ-* (- (suc m × 1#)) (suc n × 1#) ⟩ + - (suc m × 1#) * - (suc n × 1#) ∎ + +morphism : ℤ-rawRing -Raw-AlmostCommutative⟶ R-acr +morphism = record + { ⟦_⟧ = ⟦_⟧ + ; +-homo = +-homo + ; *-homo = *-homo + ; -‿homo = -‿homo + ; 0-homo = 0-homo + ; 1-homo = 1-homo + } + +-- A non-trivial `dec` is essential: without it the underlying solver +-- can't fold `1 *_` / `0 +_` during Horner normalisation, and even +-- `1# * a ≈ a` fails. ℤ equality is decidable, so we can always +-- return `just` on equal coefficients. +dec : ∀ m n → Maybe (m ×ᶻ 1# ≈ n ×ᶻ 1#) +dec m n = case m ≟ n of λ where + (yes m≡n) → just (reflexive (≡.cong (_×ᶻ 1#) m≡n)) + (no _) → nothing + +-- `hiding (⟦_⟧)`: `Algebra.Solver.Ring` re-exports the morphism's +-- `⟦_⟧`, which would shadow our own. +open import Algebra.Solver.Ring ℤ-rawRing R-acr morphism dec public + hiding (⟦_⟧) + +------------------------------------------------------------------------ +-- Top-level aliases so the macro can reflect `con`, `var`, `:-_` by +-- name (they're constructors nested inside `Algebra.Solver.Ring`'s +-- four-parameter module otherwise). The `def`-shaped `_:+_`, `_:*_`, +-- `_:-_`, `_:=_` don't need aliases. + +conP : ∀ {n} → ℤ → Polynomial n +conP = con + +varP : ∀ {n} → Fin n → Polynomial n +varP = var + +negP : ∀ {n} → Polynomial n → Polynomial n +negP = :-_ diff --git a/Tactic/Solver/Ring/Tests.agda b/Tactic/Solver/Ring/Tests.agda new file mode 100644 index 0000000..6cecdef --- /dev/null +++ b/Tactic/Solver/Ring/Tests.agda @@ -0,0 +1,6 @@ +module Tactic.Solver.Ring.Tests where + +open import Tactic.Solver.Ring.Tests.BundleVariants +open import Tactic.Solver.Ring.Tests.CommutativeRing +open import Tactic.Solver.Ring.Tests.Comparison +open import Tactic.Solver.Ring.Tests.Equations diff --git a/Tactic/Solver/Ring/Tests/BundleVariants.agda b/Tactic/Solver/Ring/Tests/BundleVariants.agda new file mode 100644 index 0000000..6903c56 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/BundleVariants.agda @@ -0,0 +1,210 @@ +------------------------------------------------------------------------ +-- Tests `solve-≈` against various ways a `CommutativeSemiring` can +-- be defined. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.Ring.Tests.BundleVariants where + +open import Algebra using (CommutativeSemiring) +open import Data.Integer as ℤ using (ℤ) +import Data.Integer.Properties as ℤP +open import Data.Nat as ℕ using (ℕ) +import Data.Nat.Properties as ℕP +open import Data.Sign as Sign using (Sign) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Tactic.Solver.Ring using (solve-≈) + +------------------------------------------------------------------------ +-- 1. Trivial alias. + +myZ : CommutativeSemiring _ _ +myZ = ℤP.+-*-commutativeSemiring + +module AliasZ where + open CommutativeSemiring myZ + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZ + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZ + +------------------------------------------------------------------------ +-- 2. Inline record literal with direct field values. + +myZ'' : CommutativeSemiring _ _ +myZ'' = record + { Carrier = ℤ + ; _≈_ = _≡_ + ; _+_ = ℤ._+_ + ; _*_ = ℤ._*_ + ; 0# = ℤ.+ 0 + ; 1# = ℤ.+ 1 + ; isCommutativeSemiring = ℤP.+-*-isCommutativeSemiring + } + +module InlineRecordZ where + open CommutativeSemiring myZ'' + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZ'' + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZ'' + +------------------------------------------------------------------------ +-- 3. η-expanded operators. + +myZη : CommutativeSemiring _ _ +myZη = record + { Carrier = ℤ + ; _≈_ = _≡_ + ; _+_ = λ a b → a ℤ.+ b + ; _*_ = λ a b → a ℤ.* b + ; 0# = ℤ.+ 0 + ; 1# = ℤ.+ 1 + ; isCommutativeSemiring = ℤP.+-*-isCommutativeSemiring + } + +module EtaExpandedZ where + open CommutativeSemiring myZη + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZη + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZη + +------------------------------------------------------------------------ +-- 4. ℕ analogues of the above. + +myN : CommutativeSemiring _ _ +myN = ℕP.+-*-commutativeSemiring + +module AliasN where + open CommutativeSemiring myN + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myN + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myN + +myN' : CommutativeSemiring _ _ +myN' = record + { Carrier = ℕ + ; _≈_ = _≡_ + ; _+_ = ℕ._+_ + ; _*_ = ℕ._*_ + ; 0# = 0 + ; 1# = 1 + ; isCommutativeSemiring = ℕP.+-*-isCommutativeSemiring + } + +module InlineRecordN where + open CommutativeSemiring myN' + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myN' + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myN' + +------------------------------------------------------------------------ +-- 5. Bundle defined as the result of a function. + +makeZ : ℤ → CommutativeSemiring _ _ +makeZ _ = ℤP.+-*-commutativeSemiring + +myZf : CommutativeSemiring _ _ +myZf = makeZ (ℤ.+ 0) + +module FunctionResultZ where + open CommutativeSemiring myZf + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZf + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZf + +------------------------------------------------------------------------ +-- 6. Two-level alias chain. + +myZAlias1 : CommutativeSemiring _ _ +myZAlias1 = ℤP.+-*-commutativeSemiring + +myZAlias2 : CommutativeSemiring _ _ +myZAlias2 = myZAlias1 + +module DoubleAliasZ where + open CommutativeSemiring myZAlias2 + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZAlias2 + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZAlias2 + +------------------------------------------------------------------------ +-- 7. Record update on top of an alias. + +myZUpdated : CommutativeSemiring _ _ +myZUpdated = record myZAlias1 { 0# = ℤ.+ 0 } + +module RecordUpdateOfAliasZ where + open CommutativeSemiring myZUpdated + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZUpdated + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZUpdated + +------------------------------------------------------------------------ +-- 8. Record update with η-expanded field values. + +myZUpdatedη : CommutativeSemiring _ _ +myZUpdatedη = record ℤP.+-*-commutativeSemiring + { _+_ = λ a b → a ℤ.+ b + ; _*_ = λ a b → a ℤ.* b + } + +module RecordUpdateηZ where + open CommutativeSemiring myZUpdatedη + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ myZUpdatedη + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ myZUpdatedη + +------------------------------------------------------------------------ +-- 9. Inlined operator body (KNOWN FAILURE). Instead of referring to +-- `ℤ._*_`, write its definition `sign i Sign.* sign j ◃ ∣i∣ ℕ.* +-- ∣j∣` directly in the bundle. +-- +-- We cannot tell Agda to stop reduction at a record projection +-- (this is a limitation of reflection primitives) and we have to +-- reduce enough for other use cases, so we have no way to stop +-- reduction before it expands to the RHS of the record, which is +-- too late. +-- +-- The workaround is to give the inlined formula its own top-level +-- definition. + +myZInlined : CommutativeSemiring _ _ +myZInlined = record ℤP.+-*-commutativeSemiring + { _*_ = λ i j → ℤ.sign i Sign.* ℤ.sign j ℤ.◃ ℤ.∣ i ∣ ℕ.* ℤ.∣ j ∣ + } + +module InlinedBodyZ where + open CommutativeSemiring myZInlined + + -- assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + -- assoc* = solve-≈ myZInlined + + -- comm+ : ∀ a b → (a + b) ≈ (b + a) + -- comm+ = solve-≈ myZInlined diff --git a/Tactic/Solver/Ring/Tests/CommutativeRing.agda b/Tactic/Solver/Ring/Tests/CommutativeRing.agda new file mode 100644 index 0000000..155ec98 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/CommutativeRing.agda @@ -0,0 +1,120 @@ +{-# OPTIONS --safe --without-K #-} + +module Tactic.Solver.Ring.Tests.CommutativeRing where + +open import Algebra using (CommutativeRing) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Tactic.Solver.Ring using (solve-≈) + +------------------------------------------------------------------------ +-- Concrete ℤ. + +module TestsℤCRConcrete where + open import Data.Integer using (+_) + open import Data.Integer.Properties using (+-*-commutativeRing) + open CommutativeRing +-*-commutativeRing using (_≈_; _+_; _*_; _-_; -_) + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ +-*-commutativeRing + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ +-*-commutativeRing + + distrib-test : ∀ a b c → a * (b + c) ≈ a * b + a * c + distrib-test = solve-≈ +-*-commutativeRing + + neg-comm : ∀ a b → - (a + b) ≈ - a + - b + neg-comm = solve-≈ +-*-commutativeRing + + neg-double : ∀ a → - (- a) ≈ a + neg-double = solve-≈ +-*-commutativeRing + + sub-as-add-neg : ∀ a b → a - b ≈ a + (- b) + sub-as-add-neg = solve-≈ +-*-commutativeRing + + distrib-over-sub : ∀ a b c → a * (b - c) ≈ a * b - a * c + distrib-over-sub = solve-≈ +-*-commutativeRing + + cancel-sub : ∀ a → a - a ≈ (+ 0) + cancel-sub = solve-≈ +-*-commutativeRing + + lit-add : (+ 1) + (+ 1) ≈ (+ 2) + lit-add = solve-≈ +-*-commutativeRing + + comm+-lit : ∀ a → (a + (+ 1)) ≈ ((+ 1) + a) + comm+-lit = solve-≈ +-*-commutativeRing + +------------------------------------------------------------------------ +-- Abstract `CommutativeRing`. + +module TestsAbstractCR {c ℓ} (R : CommutativeRing c ℓ) where + open CommutativeRing R + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ R + + assoc+ : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc+ = solve-≈ R + + comm* : ∀ a b → (a * b) ≈ (b * a) + comm* = solve-≈ R + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ R + + distrib-test : ∀ a b c → a * (b + c) ≈ a * b + a * c + distrib-test = solve-≈ R + + zero-add : ∀ a → 0# + a ≈ a + zero-add = solve-≈ R + + one-mul : ∀ a → 1# * a ≈ a + one-mul = solve-≈ R + + zero-mul : ∀ a → 0# * a ≈ 0# + zero-mul = solve-≈ R + + one-mul' : ∀ a → a * 1# ≈ a + one-mul' = solve-≈ R + + neg-self : ∀ a → - a ≈ - a + neg-self = solve-≈ R + + neg-zero : - 0# ≈ 0# + neg-zero = solve-≈ R + + neg-double : ∀ a → - (- a) ≈ a + neg-double = solve-≈ R + + neg-comm : ∀ a b → - (a + b) ≈ - a + - b + neg-comm = solve-≈ R + + add-inverse-right : ∀ a → a + (- a) ≈ 0# + add-inverse-right = solve-≈ R + + add-inverse-left : ∀ a → (- a) + a ≈ 0# + add-inverse-left = solve-≈ R + + sub-self : ∀ a → a - a ≈ 0# + sub-self = solve-≈ R + + sub-as-add-neg : ∀ a b → a - b ≈ a + (- b) + sub-as-add-neg = solve-≈ R + + sub-comm-via-neg : ∀ a b → a - b ≈ - (b - a) + sub-comm-via-neg = solve-≈ R + + distrib-over-sub : ∀ a b c → a * (b - c) ≈ a * b - a * c + distrib-over-sub = solve-≈ R + + binomial-neg : ∀ a b → (a - b) * (a + b) ≈ a * a - b * b + binomial-neg = solve-≈ R + + perfect-square-neg : ∀ a b → (a - b) * (a - b) ≈ (a * a - (1# + 1#) * a * b) + b * b + perfect-square-neg = solve-≈ R + + neg-distrib-mul : ∀ a b → (- a) * b ≈ - (a * b) + neg-distrib-mul = solve-≈ R + + neg-times-neg : ∀ a b → (- a) * (- b) ≈ a * b + neg-times-neg = solve-≈ R diff --git a/Tactic/Solver/Ring/Tests/Comparison.agda b/Tactic/Solver/Ring/Tests/Comparison.agda new file mode 100644 index 0000000..d735ca8 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/Comparison.agda @@ -0,0 +1,137 @@ +------------------------------------------------------------------------ +-- Side-by-side comparison of `solve-≈` against the stdlib's +-- ring-solver variants. Each feature shows a working `solve-≈` +-- test and the closest stdlib equivalent (either active or +-- commented out, with the error if uncommented). +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.Ring.Tests.Comparison where + +open import Algebra using (CommutativeSemiring) +open import Data.Nat.Properties using (+-*-commutativeSemiring) +import Data.Integer.Properties as ℤP +open import Data.List using (_∷_; []) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Tactic.Solver.Ring using (solve-≈) +import Data.Nat.Tactic.RingSolver as NatSolver +import Data.Integer.Tactic.RingSolver as ℤSolver +import Algebra.Solver.Ring.NaturalCoefficients.Default as NCD + +------------------------------------------------------------------------ +-- Feature 1. Abstract rings. +-- +-- Stdlib's reflective `solve-∀` takes a top-level `Name`; module +-- parameters can't be `quote`-d. + +module ParamRing-ours {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + comm+ : ∀ a b → a + b ≈ b + a + comm+ = solve-≈ R + +module ParamRing-stdlib {c ℓ} (R : CommutativeSemiring c ℓ) where + open NCD R + open CommutativeSemiring R + private module Eq = Setoid setoid + + -- comm+ : ∀ a b → a + b ≈ b + a + -- comm+ = RS.solve-∀ R + + -- Workaround: the non-reflective polynomial solver, with the AST + -- built by hand. + comm+-explicit : ∀ a b → a + b ≈ b + a + comm+-explicit = solve 2 (λ a b → a :+ b := b :+ a) Eq.refl + +------------------------------------------------------------------------ +-- Feature 2. Auto-quantification. +-- +-- Stdlib has two macros — `solve-∀` for `∀-`bound goals and `solve` +-- for equations with an explicit variable list — and requires the +-- user to pick the right one. `solve-≈` uses a single call shape for +-- all three forms below. + +module AutoQuant-ours {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + open import Relation.Binary.Reasoning.Setoid setoid + + -- a) Pi-bound goal, no variables bound + closed-∀ : ∀ a b → a + b ≈ b + a + closed-∀ = solve-≈ R + + -- b) Some variables bound + with-patterns : ∀ a b → a + b ≈ b + a + with-patterns a = solve-≈ R + +module AutoQuant-stdlib where + open import Data.Nat using (_+_; _*_) + + -- (a) ∀-bound: `solve-∀` works. + closed-∀ : ∀ a b → a + b ≡ b + a + closed-∀ = NatSolver.solve-∀ + + -- (b) Patterns introduced: must switch to `solve` + variable list. + with-patterns : ∀ a b → a + b ≡ b + a + with-patterns a b = NatSolver.solve (a ∷ b ∷ []) + +------------------------------------------------------------------------ +-- Feature 3. Concrete-ring bundles. +-- +-- Stdlib ships one preconfigured wrapper per carrier +-- (`Data.Nat.Tactic.RingSolver`, `Data.Integer.Tactic.RingSolver`, +-- `Data.Rational.Tactic.RingSolver`, …). `solve-≈` is a single macro +-- that handles all of them. + +module ConcreteRings-ours where + -- ℕ + module ℕcase where + open import Data.Nat using (_+_; _*_) + distrib : ∀ a b c → a * (b + c) ≡ a * b + a * c + distrib = solve-≈ +-*-commutativeSemiring + + -- ℤ + module ℤcase where + open import Data.Integer using (_+_; _*_) + open CommutativeSemiring ℤP.+-*-commutativeSemiring using (_≈_) + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ ℤP.+-*-commutativeSemiring + + -- ℤ with operators projected from the bundle. + module ℤbundle where + open CommutativeSemiring ℤP.+-*-commutativeSemiring + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ ℤP.+-*-commutativeSemiring + +module ConcreteRings-stdlib where + -- ℕ-specific wrapper + module ℕcase where + open import Data.Nat using (_+_; _*_) + distrib : ∀ a b c → a * (b + c) ≡ a * b + a * c + distrib = NatSolver.solve-∀ + + -- ℤ-specific wrapper (separate import) + module ℤcase where + open import Data.Integer using (_+_; _*_) + assoc* : ∀ a b c → ((a * b) * c) ≡ (a * (b * c)) + assoc* = ℤSolver.solve-∀ + +------------------------------------------------------------------------ +-- Feature 4. The stdlib solver just fails on some goals. +-- +-- Under certain circumstances, the stdlib solver doesn't reduce +-- enough, leading to it not being able to solve some equations. + +module CongChain-ours where + open import Data.Nat using (_+_) + open CommutativeSemiring +-*-commutativeSemiring using (_≈_; +-congˡ; +-comm; trans) + + trans-congˡ : ∀ a b c → a + (b + c) ≈ (a + c) + b + trans-congˡ a b c = trans (+-congˡ {x = a} (+-comm b c)) (solve-≈ +-*-commutativeSemiring) + + -- stdlib's `solve` fails with `a != a + c of type ℕ`. + -- trans-congˡ-stdlib : ∀ a b c → a + (b + c) ≈ (a + c) + b + -- trans-congˡ-stdlib a b c = trans (+-congˡ {x = a} (+-comm b c)) + -- (NatSolver.solve (a ∷ c ∷ b ∷ [])) diff --git a/Tactic/Solver/Ring/Tests/Equations.agda b/Tactic/Solver/Ring/Tests/Equations.agda new file mode 100644 index 0000000..2bb0a27 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/Equations.agda @@ -0,0 +1,600 @@ +{-# OPTIONS --safe --without-K #-} + +module Tactic.Solver.Ring.Tests.Equations where + +open import Algebra using (CommutativeSemiring) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Tactic.Solver.Ring using (solve-≈ ; module Solver) + +------------------------------------------------------------------------ +-- Limitations +-- +-- `solve-≈` is not going to help solving any metavariables. When it +-- is applied in any context where at least one side of the goal +-- contains an unresolved metavariable that only this solve call can +-- determine, the macro emits a friendly type error. Note: this might +-- be fixable, by making the solver aware of metas & letting it solve +-- them. This seems very tricky and not worth it - just add a type +-- annotation. +------------------------------------------------------------------------ + +module ReadableErrorMessages {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + -- meta-left : ∀ {a} → (∀ {c} → a ≈ c * a → a ≈ 0#) → a ≈ 0# + -- meta-left f = f (solve-≈ R) + + -- meta-right : ∀ {a} → (∀ {c} → c * a ≈ a → a ≈ 0#) → a ≈ 0# + -- meta-right f = f (solve-≈ R) + + -- meta-both : ∀ {a} → (∀ {c d} → c * a ≈ d * a → a ≈ 0#) → a ≈ 0# + -- meta-both f = f (solve-≈ R) + + -- meta-wrapped : (f : Carrier → Carrier) → ∀ {a} → (∀ {c} → a ≈ f c * a → a ≈ 0#) → a ≈ 0# + -- meta-wrapped _ f = f (solve-≈ R) + +module BundleOnConcreteℚ where + open import Data.Rational + open import Data.Rational.Properties + + eq : ∀ (q : ℚ) → q * 0ℚ + 0ℚ ≡ 0ℚ + eq q = solve-≈ +-*-commutativeRing + +module SucAtom where + open import Data.Nat using (_+_; _*_; suc) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + suc[n]-1+n : ∀ n → suc n ≡ 1 + n + suc[n]-1+n = solve-≈ +-*-commutativeSemiring + + suc-suc : ∀ n → suc (suc n) ≡ 2 + n + suc-suc = solve-≈ +-*-commutativeSemiring + + suc-distrib : ∀ n m → suc (n + m) ≡ suc n + m + suc-distrib = solve-≈ +-*-commutativeSemiring + + suc-times : ∀ n → 2 * suc n ≡ 2 + 2 * n + suc-times = solve-≈ +-*-commutativeSemiring + +module BundleOnConcreteℤ where + open import Data.Integer using (+_) + open import Data.Integer.Properties using (+-*-commutativeSemiring) + open CommutativeSemiring +-*-commutativeSemiring + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ +-*-commutativeSemiring + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ +-*-commutativeSemiring + + rearrange : ∀ a b c d → ((a + b) * (c + d)) ≈ (((a * c) + (a * d)) + ((b * c) + (b * d))) + rearrange = solve-≈ +-*-commutativeSemiring + + -- `+_` works with literals and variables + lit-zero+one : (+ 1) ≈ (+ 0) + (+ 1) + lit-zero+one = solve-≈ +-*-commutativeSemiring + + lit-one*one : (+ 1) ≈ (+ 1) * (+ 1) + lit-one*one = solve-≈ +-*-commutativeSemiring + + lit-two : (+ 2) ≈ (+ 1) + (+ 1) + lit-two = solve-≈ +-*-commutativeSemiring + + comm+' : ∀ a b → (a + (+ b)) ≈ ((+ b) + a) + comm+' = solve-≈ +-*-commutativeSemiring + + -- README `Tactic.RingSolver` lemmas on concrete ℤ. + readme-lemma₁ : ∀ x y → (x + y) + (+ 3) ≈ (((+ 2) + y) + x) + (+ 1) + readme-lemma₁ x y = solve-≈ +-*-commutativeSemiring + + readme-lemma₂ : ∀ x → (x * (+ 2)) + (+ 1) ≈ (x + (+ 1)) + x + readme-lemma₂ x = solve-≈ +-*-commutativeSemiring + + readme-lemma₆ : ∀ x y → x + y * (+ 1) + (+ 3) ≈ (+ 2) + y + x + (+ 1) + readme-lemma₆ x y = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- Concrete ℕ via `+-*-commutativeSemiring`. + +module TestsℕConcrete where + open import Data.Nat using (ℕ; _+_; _*_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + open CommutativeSemiring +-*-commutativeSemiring using (_≈_) + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ +-*-commutativeSemiring + + comm+-≈ : ∀ a b → (a + b) ≈ (b + a) + comm+-≈ a b = solve-≈ +-*-commutativeSemiring + + comm* : ∀ a b → (a * b) ≈ (b * a) + comm* = solve-≈ +-*-commutativeSemiring + + comm*-≈ : ∀ a b → (a * b) ≈ (b * a) + comm*-≈ a b = solve-≈ +-*-commutativeSemiring + + assoc+ : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc+ = solve-≈ +-*-commutativeSemiring + + assoc+-≈ : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc+-≈ a b c = solve-≈ +-*-commutativeSemiring + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ +-*-commutativeSemiring + + assoc*-≈ : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc*-≈ a b c = solve-≈ +-*-commutativeSemiring + + distrib-test : ∀ a b c → (a * (b + c)) ≈ ((a * b) + (a * c)) + distrib-test = solve-≈ +-*-commutativeSemiring + + distrib-test-≈ : ∀ a b c → (a * (b + c)) ≈ ((a * b) + (a * c)) + distrib-test-≈ a b c = solve-≈ +-*-commutativeSemiring + + rearrange3 : ∀ a b c → (a + (b + c)) ≈ (b + (a + c)) + rearrange3 = solve-≈ +-*-commutativeSemiring + + rearrange3-≈ : ∀ a b c → (a + (b + c)) ≈ (b + (a + c)) + rearrange3-≈ a b c = solve-≈ +-*-commutativeSemiring + + rearrange4 : ∀ a b c d → (((a + b) + c) + d) ≈ (((d + c) + b) + a) + rearrange4 = solve-≈ +-*-commutativeSemiring + + rearrange4-≈ : ∀ a b c d → (((a + b) + c) + d) ≈ (((d + c) + b) + a) + rearrange4-≈ a b c d = solve-≈ +-*-commutativeSemiring + + expand2 : ∀ a b c d → ((a + b) * (c + d)) ≈ (((a * c) + (a * d)) + ((b * c) + (b * d))) + expand2 = solve-≈ +-*-commutativeSemiring + + expand2-≈ : ∀ a b c d → ((a + b) * (c + d)) ≈ (((a * c) + (a * d)) + ((b * c) + (b * d))) + expand2-≈ a b c d = solve-≈ +-*-commutativeSemiring + + twisted : ∀ a b c → ((a * b) + (b * c)) ≈ (b * (a + c)) + twisted = solve-≈ +-*-commutativeSemiring + + twisted-≈ : ∀ a b c → ((a * b) + (b * c)) ≈ (b * (a + c)) + twisted-≈ a b c = solve-≈ +-*-commutativeSemiring + + bigComm : ∀ a b c d e → ((((a + b) + c) + d) + e) ≈ ((((e + d) + c) + b) + a) + bigComm = solve-≈ +-*-commutativeSemiring + + bigComm-≈ : ∀ a b c d e → ((((a + b) + c) + d) + e) ≈ ((((e + d) + c) + b) + a) + bigComm-≈ a b c d e = solve-≈ +-*-commutativeSemiring + + nat-lit-1 : ∀ a → (1 + a) ≈ (a + 1) + nat-lit-1 = solve-≈ +-*-commutativeSemiring + + nat-lit-1-≈ : ∀ a → (1 + a) ≈ (a + 1) + nat-lit-1-≈ a = solve-≈ +-*-commutativeSemiring + + nat-lit-2 : ∀ a → (2 + a) ≈ (a + 2) + nat-lit-2 = solve-≈ +-*-commutativeSemiring + + nat-lit-2-≈ : ∀ a → (2 + a) ≈ (a + 2) + nat-lit-2-≈ a = solve-≈ +-*-commutativeSemiring + + nat-lit-3 : ∀ a → ((3 * a) + a) ≈ ((1 + 3) * a) + nat-lit-3 = solve-≈ +-*-commutativeSemiring + + nat-lit-3-≈ : ∀ a → ((3 * a) + a) ≈ ((1 + 3) * a) + nat-lit-3-≈ a = solve-≈ +-*-commutativeSemiring + + binomial : ∀ a → ((a + 1) * (a + 1)) ≈ (((a * a) + (2 * a)) + 1) + binomial = solve-≈ +-*-commutativeSemiring + + binomial-≈ : ∀ a → ((a + 1) * (a + 1)) ≈ (((a * a) + (2 * a)) + 1) + binomial-≈ a = solve-≈ +-*-commutativeSemiring + + affine : ∀ a b → ((2 * a) + (3 * b)) ≈ ((b + a) + ((b + a) + b)) + affine = solve-≈ +-*-commutativeSemiring + + affine-≈ : ∀ a b → ((2 * a) + (3 * b)) ≈ ((b + a) + ((b + a) + b)) + affine-≈ a b = solve-≈ +-*-commutativeSemiring + + -- ℕ's bundle `_≈_` IS propositional `_≡_`, so the macro discharges + -- both forms. + prop-eq : ∀ a b → (a + b) ≡ (b + a) + prop-eq = solve-≈ +-*-commutativeSemiring + + prop-eq-≈ : ∀ a b → (a + b) ≡ (b + a) + prop-eq-≈ a b = solve-≈ +-*-commutativeSemiring + + -- Concrete ℕ version of `(m*n)*(o*p) ≈ (m*o)*(n*p)` + -- (`Data.Nat.Properties.[m*n]*[o*p]≡[m*o]*[n*p]`, proved by hand in + -- stdlib). + interchange* : ∀ m n o p → (m * n) * (o * p) ≈ (m * o) * (n * p) + interchange* m n o p = solve-≈ +-*-commutativeSemiring + + -- Homomorphism patterns from `Data.Nat.Binary.Properties` (proofs + -- that originally called `Data.Nat.Solver`). + homo+-0even : ∀ m n → 2 * (2 + (m + n)) ≈ 2 * (1 + m) + 2 * (1 + n) + homo+-0even m n = solve-≈ +-*-commutativeSemiring + + homo+-1odd : ∀ m n → 1 + (2 * (1 + (m + n))) ≈ 2 * (1 + m) + (1 + (2 * n)) + homo+-1odd m n = solve-≈ +-*-commutativeSemiring + + homo+-2even : ∀ m n → 1 + (1 + (2 * (m + n))) ≈ (1 + (2 * m)) + (1 + (2 * n)) + homo+-2even m n = solve-≈ +-*-commutativeSemiring + + homo*-evenodd : ∀ m n → 2 * (2 * (1 + (m + (n + m * n)))) ≈ (2 * (1 + m)) * (2 * (1 + n)) + homo*-evenodd m n = solve-≈ +-*-commutativeSemiring + + homo*-evenoddm : ∀ m n → 2 * ((1 + m) + (n * (2 * (1 + m)))) ≈ (2 * (1 + m)) * (1 + 2 * n) + homo*-evenoddm m n = solve-≈ +-*-commutativeSemiring + + -- Literal-rich ℕ rearrangements from `Data.Integer.Properties.NatLemmas` + -- (used by `*-distribʳ-+`'s case analysis). + natlemma-assoc₁ : ∀ m n o → (2 + n + o) * (1 + m) ≈ (1 + n) * (1 + m) + (1 + o) * (1 + m) + natlemma-assoc₁ m n o = solve-≈ +-*-commutativeSemiring + + natlemma-assoc₂ : ∀ m n o → (1 + n + (1 + o)) * (1 + m) ≈ (1 + n) * (1 + m) + (1 + o) * (1 + m) + natlemma-assoc₂ m n o = solve-≈ +-*-commutativeSemiring + + natlemma-assoc₃ : ∀ m n o → m + (n + (1 + o)) * (1 + m) ≈ (1 + n) * (1 + m) + (m + o * (1 + m)) + natlemma-assoc₃ m n o = solve-≈ +-*-commutativeSemiring + + natlemma-inner-assoc : ∀ m n o → + o + (n + m * (1 + n)) * (1 + o) + ≈ o + n * (1 + o) + m * (1 + (o + n * (1 + o))) + natlemma-inner-assoc m n o = solve-≈ +-*-commutativeSemiring + + -- README `Tactic.RingSolver` `NaturalExamples.lemma₁`. + readme-lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x + readme-lemma₁ x y = solve-≈ +-*-commutativeSemiring + + -- README skew-heap tree-size invariant. + tree-merge : ∀ a b c d → 1 + (1 + c + d + b) + a ≈ 1 + a + b + (1 + c + d) + tree-merge a b c d = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- Concrete ℤ. + +module TestsℤConcrete where + open import Data.Integer using (ℤ; _+_; _*_; -_; _-_) + open import Data.Integer.Properties using (+-*-commutativeSemiring) + open CommutativeSemiring +-*-commutativeSemiring using (_≈_) + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ +-*-commutativeSemiring + + comm+-≈ : ∀ a b → (a + b) ≈ (b + a) + comm+-≈ a b = solve-≈ +-*-commutativeSemiring + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ +-*-commutativeSemiring + + assoc*-≈ : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc*-≈ a b c = solve-≈ +-*-commutativeSemiring + + -- Negation / subtraction aren't in `CommutativeSemiring`'s + -- vocabulary, so `_-_` and `-_` get atomised whole, breaking the + -- proof. + -- + -- neg-comm : ∀ a b → (- (a + b)) ≈ ((- a) + (- b)) + -- neg-comm = solve-≈ +-*-commutativeSemiring + + -- 4-variable rearrangements over ℤ. + fourway-* : ∀ a b c d → (a * b) * (c * d) ≈ (a * c) * (b * d) + fourway-* a b c d = solve-≈ +-*-commutativeSemiring + + fourway-+ : ∀ a b c d → (a + b) + (c + d) ≈ (a + c) + (b + d) + fourway-+ a b c d = solve-≈ +-*-commutativeSemiring + + distribˡ : ∀ a b c → a * (b + c) ≈ a * b + a * c + distribˡ a b c = solve-≈ +-*-commutativeSemiring + + -- 6-variable ℤ rearrangements from `Data.Rational.Unnormalised.Properties` + -- (`+-cong`, `+-assoc-↥`, `*-distribˡ-+`-related lemmas). + ratunnorm-+-cong : ∀ ↥x ↧x ↧y ↥u ↧u ↧v → + (↥x * ↧u + ↥u * ↧x) * (↧y * ↧v) ≈ ↥x * ↧y * (↧u * ↧v) + ↥u * ↧v * (↧x * ↧y) + ratunnorm-+-cong ↥x ↧x ↧y ↥u ↧u ↧v = solve-≈ +-*-commutativeSemiring + + ratunnorm-+-assoc : ∀ ↥p ↧p ↥q ↧q ↥r ↧r → + (↥p * ↧q + ↥q * ↧p) * ↧r + ↥r * (↧p * ↧q) ≈ ↥p * (↧q * ↧r) + (↥q * ↧r + ↥r * ↧q) * ↧p + ratunnorm-+-assoc ↥p ↧p ↥q ↧q ↥r ↧r = solve-≈ +-*-commutativeSemiring + + ratunnorm-distrib : ∀ ↥p ↧p ↥q d e f → + (↥p * (↥q * f + e * d)) * (↧p * d * (↧p * f)) + ≈ (↥p * ↥q * (↧p * f) + ↥p * e * (↧p * d)) * (↧p * (d * f)) + ratunnorm-distrib ↥p ↧p ↥q d e f = solve-≈ +-*-commutativeSemiring + + -- 8-variable stress test on ℤ. + big8 : ∀ a b c d e f g h → + ((a + b) + (c + d)) * ((e + f) + (g + h)) + ≈ (((((a * e) + (a * f)) + ((a * g) + (a * h))) + + (((b * e) + (b * f)) + ((b * g) + (b * h)))) + + ((((c * e) + (c * f)) + ((c * g) + (c * h))) + + (((d * e) + (d * f)) + ((d * g) + (d * h))))) + big8 a b c d e f g h = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- Abstract parameterised `CommutativeSemiring`. + +module TestsAbstractCSR {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + private module Eq = Setoid setoid + + -- Repeated occurrences of the same variable + refl₁ : ∀ a → (a + a) ≈ (a + a) + refl₁ = solve-≈ R + + refl₁-≈ : ∀ a → (a + a) ≈ (a + a) + refl₁-≈ a = solve-≈ R + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ = solve-≈ R + + comm+-≈ : ∀ a b → (a + b) ≈ (b + a) + comm+-≈ a b = solve-≈ R + + comm* : ∀ a b → (a * b) ≈ (b * a) + comm* = solve-≈ R + + comm*-≈ : ∀ a b → (a * b) ≈ (b * a) + comm*-≈ a b = solve-≈ R + + assoc+ : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc+ = solve-≈ R + + assoc+-≈ : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc+-≈ a b c = solve-≈ R + + assoc* : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc* = solve-≈ R + + assoc*-≈ : ∀ a b c → ((a * b) * c) ≈ (a * (b * c)) + assoc*-≈ a b c = solve-≈ R + + distrib-test : ∀ a b c → (a * (b + c)) ≈ ((a * b) + (a * c)) + distrib-test = solve-≈ R + + distrib-test-≈ : ∀ a b c → (a * (b + c)) ≈ ((a * b) + (a * c)) + distrib-test-≈ a b c = solve-≈ R + + swap-mid : ∀ a b c → (a + (b + c)) ≈ (b + (a + c)) + swap-mid = solve-≈ R + + swap-mid-≈ : ∀ a b c → (a + (b + c)) ≈ (b + (a + c)) + swap-mid-≈ a b c = solve-≈ R + + deep+ : ∀ a b c d → ((a + b) + (c + d)) ≈ ((a + c) + (b + d)) + deep+ = solve-≈ R + + deep+-≈ : ∀ a b c d → ((a + b) + (c + d)) ≈ ((a + c) + (b + d)) + deep+-≈ a b c d = solve-≈ R + + deep* : ∀ a b c d → ((a * b) * (c * d)) ≈ ((a * c) * (b * d)) + deep* = solve-≈ R + + deep*-≈ : ∀ a b c d → ((a * b) * (c * d)) ≈ ((a * c) * (b * d)) + deep*-≈ a b c d = solve-≈ R + + square : ∀ a b → ((a + b) * (a + b)) ≈ (((a * a) + (a * b)) + ((b * a) + (b * b))) + square = solve-≈ R + + square-≈ : ∀ a b → ((a + b) * (a + b)) ≈ (((a * a) + (a * b)) + ((b * a) + (b * b))) + square-≈ a b = solve-≈ R + + big-expand : ∀ a b c d → ((a + b) * (c + d)) ≈ (((a * c) + (a * d)) + ((b * c) + (b * d))) + big-expand = solve-≈ R + + big-expand-≈ : ∀ a b c d → ((a + b) * (c + d)) ≈ (((a * c) + (a * d)) + ((b * c) + (b * d))) + big-expand-≈ a b c d = solve-≈ R + + -- The shape used in `Expectation.weight-sum-+`'s rearrangement. + weight-sum-style : ∀ pω fω gω wsf wsg → + (((pω * (fω + gω)) + (wsf + wsg))) + ≈ ((((pω * fω) + wsf) + ((pω * gω) + wsg))) + weight-sum-style = solve-≈ R + + weight-sum-style-≈ : ∀ pω fω gω wsf wsg → + (((pω * (fω + gω)) + (wsf + wsg))) + ≈ ((((pω * fω) + wsf) + ((pω * gω) + wsg))) + weight-sum-style-≈ pω fω gω wsf wsg = solve-≈ R + + trans-congˡ : ∀ a b c → a + (b + c) ≈ (a + c) + b + trans-congˡ a b c = Eq.trans + (+-congˡ (+-comm b c)) + (solve-≈ R) + + six-vars : ∀ a b c d e f → + ((((a + b) + c) + d) + (e + f)) + ≈ (((((f + e) + d) + c) + b) + a) + six-vars = solve-≈ R + + six-vars-≈ : ∀ a b c d e f → + ((((a + b) + c) + d) + (e + f)) + ≈ (((((f + e) + d) + c) + b) + a) + six-vars-≈ a b c d e f = solve-≈ R + + seven-vars : ∀ a b c d e f g → + ((a * (b + c)) * ((d + e) * (f + g))) + ≈ ((((a * b) + (a * c)) * ((d * f) + (d * g))) + (((a * b) + (a * c)) * ((e * f) + (e * g)))) + seven-vars = solve-≈ R + + seven-vars-≈ : ∀ a b c d e f g → + ((a * (b + c)) * ((d + e) * (f + g))) + ≈ ((((a * b) + (a * c)) * ((d * f) + (d * g))) + (((a * b) + (a * c)) * ((e * f) + (e * g)))) + seven-vars-≈ a b c d e f g = solve-≈ R + + -- 9-term distributive expansion: (a+b+c)*(d+e+f). + distrib-3-3 : ∀ a b c d e f → + (a + b + c) * (d + e + f) ≈ + ((a * d + a * e) + a * f) + + (((b * d + b * e) + b * f) + + ((c * d + c * e) + c * f)) + distrib-3-3 a b c d e f = solve-≈ R + + -- Sum of squares with cross term (binomial expansion shape). + sum-square : ∀ a b → (a + b) * (a + b) ≈ a * a + (1# + 1#) * (a * b) + b * b + sum-square a b = solve-≈ R + + -- From `Data.Integer.Properties.suc-*` (after factoring through CSR): + -- `sucℤ i * j ≡ j + i * j`, i.e. `(1# + i) * j ≈ j + i * j`. + suc-* : ∀ i j → (1# + i) * j ≈ j + i * j + suc-* i j = solve-≈ R + + -- Chain compression from `Algebra.Properties.Semiring.Exp`: + -- `y * ((x * A) * B) ≈ x * (y * (A * B))`. + exp-rearrange : ∀ x y A B → y * ((x * A) * B) ≈ x * (y * (A * B)) + exp-rearrange x y A B = solve-≈ R + + -- Representative permutation laws from + -- `Algebra.Properties.CommutativeSemigroup` (read `_∙_` as `_+_`). + perm-yxz : ∀ x y z → x + (y + z) ≈ y + (x + z) + perm-yxz x y z = solve-≈ R + + perm-zyx : ∀ x y z → (x + y) + z ≈ (z + y) + x + perm-zyx x y z = solve-≈ R + + -- Same shape against `_*_`. + perm-yxz-* : ∀ x y z → x * (y * z) ≈ y * (x * z) + perm-yxz-* x y z = solve-≈ R + + -- Semimedial and Jordan-style identities. + semimedialˡ : ∀ x y z → (x + x) + (y + z) ≈ (x + y) + (x + z) + semimedialˡ x y z = solve-≈ R + + jordan : ∀ x y → (x + y) + (x + x) ≈ x + (y + (x + x)) + jordan x y = solve-≈ R + +------------------------------------------------------------------------ +-- Constants and literal-coefficient identities. + +module Constants {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + one-mul : ∀ a → (1# * a) ≈ a + one-mul = solve-≈ R + + one-mul-≈ : ∀ a → (1# * a) ≈ a + one-mul-≈ a = solve-≈ R + + one-mul' : ∀ a → (a * 1#) ≈ a + one-mul' = solve-≈ R + + one-mul'-≈ : ∀ a → (a * 1#) ≈ a + one-mul'-≈ a = solve-≈ R + + zero-add : ∀ a → (0# + a) ≈ a + zero-add = solve-≈ R + + zero-add-≈ : ∀ a → (0# + a) ≈ a + zero-add-≈ a = solve-≈ R + + zero-add' : ∀ a → (0# + (a + 0#)) ≈ a + zero-add' = solve-≈ R + + zero-add'-≈ : ∀ a → (0# + (a + 0#)) ≈ a + zero-add'-≈ a = solve-≈ R + + nat-coeff : ∀ a → (a + a) ≈ ((1# + 1#) * a) + nat-coeff = solve-≈ R + + nat-coeff-≈ : ∀ a → (a + a) ≈ ((1# + 1#) * a) + nat-coeff-≈ a = solve-≈ R + + three-mul : ∀ a → ((a + a) + a) ≈ (((1# + 1#) + 1#) * a) + three-mul = solve-≈ R + + three-mul-≈ : ∀ a → ((a + a) + a) ≈ (((1# + 1#) + 1#) * a) + three-mul-≈ a = solve-≈ R + + expand-square-of-sum-of-ones : ∀ a → ((1# + 1#) * (a + a)) ≈ ((a + a) + (a + a)) + expand-square-of-sum-of-ones = solve-≈ R + + expand-square-of-sum-of-ones-≈ : ∀ a → ((1# + 1#) * (a + a)) ≈ ((a + a) + (a + a)) + expand-square-of-sum-of-ones-≈ a = solve-≈ R + + zero-mul : ∀ a → (0# * a) ≈ 0# + zero-mul = solve-≈ R + + zero-mul-≈ : ∀ a → (0# * a) ≈ 0# + zero-mul-≈ a = solve-≈ R + + zero-mul' : ∀ a → (a * 0#) ≈ 0# + zero-mul' = solve-≈ R + + zero-mul'-≈ : ∀ a → (a * 0#) ≈ 0# + zero-mul'-≈ a = solve-≈ R + + zero+xy : ∀ x y → 0# + x * y ≈ x * y + zero+xy x y = solve-≈ R + + with-extra-≈ : (k : Carrier) → ∀ a → ((k * a) + a) ≈ ((k + 1#) * a) + with-extra-≈ k a = solve-≈ R + +------------------------------------------------------------------------ +-- Tests with free function-typed atoms. The function variables +-- have to be introduced as patterns (since neither macro abstracts +-- over Carrier-typed function values, and `solve-≈` needs them in +-- scope to collect their applications as atoms); the Carrier-typed +-- `a` stays under the goal's pi-binder. + +module FunctionAtoms {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + fn-atoms : (f g : Carrier → Carrier) (a : Carrier) + → ((f a) + (g a)) ≈ ((g a) + (f a)) + fn-atoms f g = solve-≈ R + + -- Composite atoms aren't peered into; `f (g a)` is one atom. + nested : (f g : Carrier → Carrier) (a : Carrier) + → ((f (g a)) + a) ≈ (a + (f (g a))) + nested f g = solve-≈ R + + mixed-with-const : (a : Carrier) → (1# * a) + a ≈ (1# + 1#) * a + mixed-with-const a = solve-≈ R + + larger : (a b c d e : Carrier) + → ((a * (b + c)) + (d + e)) + ≈ (((a * b) + d) + ((a * c) + e)) + larger a b c d e = solve-≈ R + + -- Inline use within an `≈⟨ … ⟩` reasoning chain. + module InContext (k : Carrier) where + open import Relation.Binary.Reasoning.Setoid setoid + reasoning : (a b : Carrier) → (k * (a + b)) ≈ ((k * a) + (k * b)) + reasoning a b = begin + k * (a + b) ≈⟨ solve-≈ R ⟩ + (k * a) + (k * b) ∎ + + -- Composite atoms are atomised whole, so a goal that rearranges + -- their *internals* sees them as distinct variables and fails: + -- + -- opaque-internal : (f : Carrier → Carrier) (a b : Carrier) + -- → (f (a + b)) ≈ (f (b + a)) + -- opaque-internal f a b = solve-≈ R + +------------------------------------------------------------------------ +-- Stress test. + +module StressTest {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + big8 : ∀ a b c d e f g h → + (((a + b) * (c + d)) + ((e + f) * (g + h))) + ≈ (((c + d) * (a + b)) + ((g + h) * (e + f))) + big8 = solve-≈ R + + big8-≈ : ∀ a b c d e f g h → + (((a + b) * (c + d)) + ((e + f) * (g + h))) + ≈ (((c + d) * (a + b)) + ((g + h) * (e + f))) + big8-≈ a b c d e f g h = solve-≈ R + + expand8 : ∀ a b c d e f g h → + (((a + b) + (c + d)) * ((e + f) + (g + h))) + ≈ (((((a * e) + (a * f)) + ((a * g) + (a * h))) + + (((b * e) + (b * f)) + ((b * g) + (b * h)))) + + ((((c * e) + (c * f)) + ((c * g) + (c * h))) + + (((d * e) + (d * f)) + ((d * g) + (d * h))))) + expand8 = solve-≈ R + + expand8-≈ : ∀ a b c d e f g h → + (((a + b) + (c + d)) * ((e + f) + (g + h))) + ≈ (((((a * e) + (a * f)) + ((a * g) + (a * h))) + + (((b * e) + (b * f)) + ((b * g) + (b * h)))) + + ((((c * e) + (c * f)) + ((c * g) + (c * h))) + + (((d * e) + (d * f)) + ((d * g) + (d * h))))) + expand8-≈ a b c d e f g h = solve-≈ R