From d10d2826db53855e5765b5a49a74e567a7ceb2ff Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Wed, 13 May 2026 15:30:18 +0200 Subject: [PATCH 1/5] Add ring solver --- Tactic.agda | 3 + Tactic/Solver/Ring.agda | 588 ++++++++++++++++++ Tactic/Solver/Ring/Tests.agda | 5 + Tactic/Solver/Ring/Tests/BundleVariants.agda | 215 +++++++ Tactic/Solver/Ring/Tests/Comparison.agda | 137 +++++ Tactic/Solver/Ring/Tests/Equations.agda | 596 +++++++++++++++++++ 6 files changed, 1544 insertions(+) create mode 100644 Tactic/Solver/Ring.agda create mode 100644 Tactic/Solver/Ring/Tests.agda create mode 100644 Tactic/Solver/Ring/Tests/BundleVariants.agda create mode 100644 Tactic/Solver/Ring/Tests/Comparison.agda create mode 100644 Tactic/Solver/Ring/Tests/Equations.agda 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/Ring.agda b/Tactic/Solver/Ring.agda new file mode 100644 index 0000000..dbbe1f3 --- /dev/null +++ b/Tactic/Solver/Ring.agda @@ -0,0 +1,588 @@ +------------------------------------------------------------------------ +-- An improved ring solver, based on the stdlib's one +-- +-- Automatically handles variable introduction as required, properly +-- deals with most literals, has sensible defaults and a few other +-- bells and whistles. Also has an extensive test suite. + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.Ring where + +open import Algebra using (CommutativeSemiring) +open import Data.Fin.Base as Fin using (Fin; toℕ) +open import Data.Vec.Base as Vec using (Vec; _∷_; []) +open import Data.List.Base as List using (List; _∷_; []; _++_; replicate; foldr; findIndexᵇ; null) +open import Data.Bool.ListAction using (any) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) +open import Data.Nat.Base using (ℕ; suc; zero; _+_) +open import Data.Bool.Base using (Bool; if_then_else_; true; false; _∨_; _∧_; not) +open import Data.Unit.Base using (⊤; tt) +open import Data.Product.Base using (_,_; _×_; proj₁) +open import Function.Base + +open import Reflection +open import Reflection.AST.Argument +open import Reflection.AST.Term +open import Reflection.AST.AlphaEquality +open import Reflection.AST.DeBruijn using (weaken) +import Reflection.AST.Name as Name +import Reflection.AST.Meta as Meta +open import Reflection.TCM.Syntax +import Agda.Builtin.Reflection as B + using (withReduceDefs) +open import Data.Nat.Reflection +import Data.Vec.Reflection as Vec + +------------------------------------------------------------------------ +-- I. Generic reflection utilities. +-- +-- Everything in this section is independent of `CommutativeSemiring` +-- (and the polynomial layer): plain helpers for inspecting and +-- manipulating reflected `Term`s, deduplicating name/atom lists, +-- chasing metavariables, and reducing `def`-chains further than +-- Agda's primitive `reduce` does. +------------------------------------------------------------------------ + +private + ---------------------------------------------------------------------- + -- Arg/Term inspection + ---------------------------------------------------------------------- + + getVisible : Arg Term → Maybe Term + getVisible (arg (arg-info visible _) x) = just x + getVisible _ = nothing + + -- Extract the head `Name` of a term, peeling off any leading λ-binders. + 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 + + -- Try to extract a ℕ value from an iterated `suc`/`zero` + -- constructor chain (or a built-in `lit (nat n)` literal). + -- Returns `nothing` if the term is not a ℕ literal. + extractNat : Term → Maybe ℕ + extractNatArgs : Args Term → Maybe ℕ + + extractNat (lit (nat n)) = just n + extractNat (con nm xs) = + if nm Name.≡ᵇ quote zero then just 0 + else if nm Name.≡ᵇ quote suc then extractNatArgs xs + else nothing + extractNat _ = nothing + + extractNatArgs (arg (arg-info visible _) x ∷ []) = Maybe.map suc (extractNat x) + extractNatArgs (_ ∷ xs) = extractNatArgs xs + extractNatArgs [] = nothing + + -- Try `extractNat` first; if that fails and we have a wrapping + -- constructor name (e.g. ℤ's `+_ : ℕ → ℤ`), peel one layer of + -- `con C (arg ∷ [])` and try again. Used to recognise `(+ n)` + -- on ℤ as a polynomial constant. + peelLitCon : Name → Term → Maybe ℕ + peelLitCon C (con nm xs) with nm Name.≡ᵇ C + ... | false = nothing + ... | true = case List.mapMaybe getVisible 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 + + getVisibleArgs : ∀ n → Term → Maybe (Vec Term n) + getVisibleArgs n (def _ xs) = Maybe.map Vec.reverse + (List.foldl f c (List.mapMaybe getVisible xs) n) + where + f : (∀ n → Maybe (Vec Term n)) → Term → ∀ n → Maybe (Vec Term n) + f xs x zero = just [] + f xs x (suc n) = Maybe.map (x ∷_) (xs n) + + c : ∀ n → Maybe (Vec Term n) + c zero = just [] + c (suc _ ) = nothing + getVisibleArgs _ _ = nothing + + ---------------------------------------------------------------------- + -- List dedup/lookup + ---------------------------------------------------------------------- + + 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 `t` into `xs` if not already present (α-equality). + insertAtom : Term → List Term → List Term + insertAtom t [] = t ∷ [] + insertAtom t (a ∷ as) = + if t =α= a then a ∷ as else a ∷ insertAtom t as + + findAtomIndex : Term → List Term → Maybe ℕ + findAtomIndex t xs = Maybe.map Fin.toℕ (findIndexᵇ (t =α=_) xs) + + ---------------------------------------------------------------------- + -- Definition inspection + ---------------------------------------------------------------------- + + noArgBody : Definition → Maybe Term + noArgBody (function (clause [] [] body ∷ _)) = just body + noArgBody _ = nothing + + -- Pick the def-Name out of a Term, potentially under η-expansion. + pickDefName : Term → List Name → List Name + pickDefName (def n _) xs = insertName n xs + pickDefName (lam _ (abs _ body)) xs = pickDefName body xs + pickDefName _ xs = xs + +mutual + headReduce : ℕ → Term → TC Term + headReduce 0 t = pure t + headReduce (suc k) (def nm []) = do + d ← getDefinition nm + case noArgBody d of λ where + (just body) → headReduce k body + nothing → 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') + +---------------------------------------------------------------------- +-- Metavariable inspection (depth-first walk). +---------------------------------------------------------------------- + +mutual + collectMetasT : Term → List Meta → List Meta + collectMetasT (var _ xs) acc = collectMetasArgs xs acc + collectMetasT (con _ xs) acc = collectMetasArgs xs acc + collectMetasT (def _ xs) acc = collectMetasArgs xs acc + collectMetasT (lam _ (abs _ t)) acc = collectMetasT t acc + collectMetasT (pat-lam _ _) acc = acc + collectMetasT (pi (arg _ a) (abs _ b)) acc = collectMetasT b (collectMetasT a acc) + collectMetasT (agda-sort s) acc = collectMetasSort s acc + collectMetasT (lit _) acc = acc + collectMetasT (meta x _) acc = x ∷ acc + collectMetasT unknown acc = acc + + collectMetasArgs : Args Term → List Meta → List Meta + collectMetasArgs [] acc = acc + collectMetasArgs (arg _ x ∷ xs) acc = collectMetasArgs xs (collectMetasT x acc) + + collectMetasSort : Sort → List Meta → List Meta + collectMetasSort (set t) acc = collectMetasT t acc + collectMetasSort (lit _) acc = acc + collectMetasSort (prop t) acc = collectMetasT t acc + collectMetasSort (propLit _) acc = acc + collectMetasSort (inf _) acc = acc + collectMetasSort unknown acc = acc + +metasOf : Term → List Meta +metasOf t = collectMetasT t [] + +firstMeta : Term → Maybe Meta +firstMeta t = case metasOf t of λ where + [] → nothing + (m ∷ _) → just m + +-- Do two meta-lists share an element? Used to distinguish +-- "deadlock" goals (no shared meta — blocking won't propagate +-- between the equation's sides) from goals where `blockOnMeta` +-- can be expected to succeed. +shareMeta : List Meta → List Meta → Bool +shareMeta xs ys = any (λ x → any (Meta._≡ᵇ_ x) ys) xs + +bareMeta : Term → Bool +bareMeta (meta _ _) = true +bareMeta _ = false + +---------------------------------------------------------------------- +-- Append a list of Terms as visible args to an existing `def`. +---------------------------------------------------------------------- + +applyVisibleArgs : Term → List Term → Term +applyVisibleArgs (def nm xs) atoms = def nm (xs ++ foldr _⟨∷⟩_ [] atoms) +applyVisibleArgs t _ = t -- shouldn't happen for our use + +------------------------------------------------------------------------ +-- II. CommutativeSemiring-specific machinery. +------------------------------------------------------------------------ + +module Solver {c ℓ} (R : CommutativeSemiring c ℓ) where + open import Algebra.Solver.Ring.NaturalCoefficients.Default R public + + -- Constructor wrappers (using `con` directly via `quote` is + -- ambiguous because of name collisions across the imported chain). + conP : ∀ {n} → ℕ → Polynomial n + conP = con + + varP : ∀ {n} → Fin n → Polynomial n + varP = var + +`CommutativeSemiring : Term +`CommutativeSemiring = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) + +record RingOperatorTerms : Set where + constructor add⇒_mul⇒_zero⇒_one⇒_ + field + add mul zero# one# : Term + +-- Try to detect a "carrier-nat constructor": a single-argument +-- constructor `C : ℕ → Carrier` that wraps ℕ literals (e.g. ℤ's +-- `+_`). We find it by checking that `zero#` and `one#` both have +-- shape `con C (n ∷ [])` with extracted ℕ values `0` and `1`. +litConstructor : RingOperatorTerms → Maybe Name +litConstructor (add⇒ _ mul⇒ _ zero⇒ con cz argsZ one⇒ con co argsO) = + check (cz Name.≡ᵇ co) (List.mapMaybe getVisible argsZ) (List.mapMaybe getVisible argsO) + where + check : Bool → List Term → List Term → Maybe Name + check true (z₀ ∷ []) (o₀ ∷ []) with extractNat z₀ | extractNat o₀ + ... | just 0 | just 1 = just cz + ... | _ | _ = nothing + check _ _ _ = nothing +litConstructor _ = nothing + +data RingOpKind : Set where + isAdd isMul isZero isOne otherOp : RingOpKind + +-- Match a `Name` against the four operator Terms. +classifyOp : RingOperatorTerms → Name → TC RingOpKind +classifyOp ops nm = do + nameTerm ← normalise (def nm []) + let nmH = just nm + let match : Term → Bool + match t = (nameTerm =α= t) ∨ (nmH ≡ᵐ headName t) + pure (if match (RingOperatorTerms.add ops) then isAdd + else if match (RingOperatorTerms.mul ops) then isMul + else if match (RingOperatorTerms.zero# ops) then isZero + else if match (RingOperatorTerms.one# ops) then isOne + else otherOp) + +checkIsRing : Term → TC Term +checkIsRing ring = checkType ring `CommutativeSemiring + +module RingReflection (`R : Term) where + + -- `nm $ʳ args` produces `def nm (2 hidden ⊕ R ⊕ args)`, mirroring + -- the calling convention of every `Solver` re-export. + infixr 6 _$ʳ_ + _$ʳ_ : Name → Args Term → Term + nm $ʳ args = def nm (2 ⋯⟅∷⟆ `R ⟨∷⟩ args) + + -- Fallback `RingOperatorTerms` for abstract bundles (e.g. a module + -- parameter): each operator is the bundle projection applied to + -- `R`. Used when `R` is not a concrete top-level `def`, so we can't + -- `getDefinition` it to peek at the fields. + abstractRingOperatorTerms : TC RingOperatorTerms + abstractRingOperatorTerms = ⦇ + add⇒ normalise (def (quote CommutativeSemiring._+_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + mul⇒ normalise (def (quote CommutativeSemiring._*_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + zero⇒ normalise (def (quote CommutativeSemiring.0#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + one⇒ normalise (def (quote CommutativeSemiring.1#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + ⦈ + + `refl : Term + `refl = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ `R ⟨∷⟩ 1 ⋯⟅∷⟆ []) + +------------------------------------------------------------------------ +-- Reflection utilities for the polynomial layer. + +module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where + open RingReflection `R + + `numberOfVariables : Term + `numberOfVariables = toTerm numberOfVariables + + infix -1 _$ᵖ_ + _$ᵖ_ : Name → List (Arg Term) → Term + nm $ᵖ xs = def nm (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟅∷⟆ xs) + + `con : Term → Term + `con n = quote Solver.conP $ᵖ (n ⟨∷⟩ []) + + `var : Term → Term + `var i = quote Solver.varP $ᵖ (i ⟨∷⟩ []) + + `:+ : Term → Term → Term + `:+ x y = quote Solver._:+_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) + + `:* : Term → Term → Term + `:* x y = quote Solver._:*_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) + + `:= : Term → Term → Term + `:= x y = quote Solver._:=_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) + + `solver : Term → Term → Term + `solver `f `eq = def (quote Solver.solve) + (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟨∷⟩ `f ⟨∷⟩ `eq ⟨∷⟩ []) + + toVarTerm : ℕ → Term + toVarTerm i = `var (toFinTerm i) + + -- Convert raw user-Term to a Polynomial Term. + -- + -- We recognise: + -- * `_+_` / `_*_` as ring operators, including bundle-projection + -- forms used in parameterised modules; + -- * `0#` / `1#` as the polynomial constants `con 0` / `con 1`; + -- * `lit (nat n)`, `con suc^k zero`, and `con C (lit n)` for a + -- detected carrier-nat constructor `C` (e.g. ℤ's `+_`) — each + -- decoded into `con n`; + -- * `suc t` where `t` is non-literal — peeled into `con 1 :+ t`. + -- + -- For anything else we call the supplied `fallback`, which `solve-≈` + -- uses to look the term up in an atom table and emit + -- `varP (Fin i)` for the matching atom (auto-quantification). + convertTerm : RingOperatorTerms → (Term → Term) → Term → TC Term + convertTerm operatorTerms fallback = convert + where + litCon : Maybe Name + litCon = litConstructor operatorTerms + + mutual + -- Try literal recognition first; then strip a `suc` and emit + -- `con 1 :+ convert inner`; otherwise dispatch on the head. + convert : Term → TC Term + convert t with extractCarrierNat litCon t + ... | just n = pure (`con (toTerm n)) + ... | nothing = convertHead t + + convertHead : Term → TC Term + convertHead (def nm xs) = do + kind ← classifyOp operatorTerms nm + case kind of λ where + isAdd → convertOp₂ `:+ xs + isMul → convertOp₂ `:* xs + isZero → pure (`con (toTerm 0)) + isOne → pure (`con (toTerm 1)) + otherOp → pure (fallback (def nm xs)) + convertHead t@(con nm xs) with nm Name.≡ᵇ quote suc | xs + ... | true | arg (arg-info visible _) x ∷ [] = do + inner ← convert x + pure (`:+ (`con (toTerm 1)) inner) + ... | _ | _ = pure (fallback t) + convertHead t = pure (fallback t) + + convertOp₂ : (Term → Term → Term) → Args Term → TC Term + convertOp₂ mk (x ⟨∷⟩ y ⟨∷⟩ []) = do + x' ← convert x + y' ← convert y + pure (mk x' y') + convertOp₂ mk (x ∷ xs) = convertOp₂ mk xs + convertOp₂ _ _ = pure (`con (toTerm 0)) + +------------------------------------------------------------------------ + +open RingReflection +open RingSolverReflection + +-- Collect the def-Names of every recognised ring-operator occurrence +-- in the user term (used to seed the `withReduceDefs` block list). +collectOpNames : RingOperatorTerms → Term → List Name → TC (List Name) +collectOpNames operatorTerms = collect + where + mutual + collect : Term → List Name → TC (List Name) + collect (def nm xs) acc = do + kind ← classifyOp operatorTerms nm + case kind of λ where + otherOp → pure acc + isZero → pure (insertName nm acc) + isOne → pure (insertName nm acc) + isAdd → collectArgs xs (insertName nm acc) + isMul → collectArgs xs (insertName nm acc) + collect _ acc = pure acc + + collectArgs : Args Term → List Name → TC (List Name) + collectArgs [] acc = pure acc + collectArgs (arg (arg-info visible _) x ∷ xs) acc = do + acc1 ← collect x acc + collectArgs xs acc1 + collectArgs (_ ∷ xs) acc = collectArgs xs acc + +-- Walk a Term, accumulating atomic subterms into the supplied list. +-- Operators and ℕ literals are decomposed/skipped; anything else +-- becomes an atom. +collectAtoms : RingOperatorTerms → Term → List Term → TC (List Term) +collectAtoms operatorTerms = collect + where + litCon : Maybe Name + litCon = litConstructor operatorTerms + + mutual + collect : Term → List Term → TC (List Term) + collect t acc with extractCarrierNat litCon t + ... | just _ = pure acc + ... | nothing = collectHead t acc + + collectHead : Term → List Term → TC (List Term) + collectHead (def nm xs) acc = do + kind ← classifyOp operatorTerms nm + case kind of λ where + isAdd → collectOp₂ xs acc + isMul → collectOp₂ xs acc + isZero → pure acc + isOne → pure acc + otherOp → pure (insertAtom (def nm xs) acc) + collectHead t@(con nm xs) acc with nm Name.≡ᵇ quote suc | xs + ... | true | arg (arg-info visible _) x ∷ [] = collect x acc + ... | _ | _ = pure (insertAtom t acc) + collectHead t acc = pure (insertAtom t acc) + + collectOp₂ : Args Term → List Term → TC (List Term) + collectOp₂ (x ⟨∷⟩ y ⟨∷⟩ []) acc = do + acc1 ← collect x acc + collect y acc1 + collectOp₂ (x ∷ xs) acc = collectOp₂ xs acc + collectOp₂ [] acc = pure acc + +------------------------------------------------------------------------ +-- Inspect a bundle term `R` and produce its `RingOperatorTerms` +-- plus the list of underlying field-value Names to block via +-- `withReduceDefs`. + +ringOperatorTerms : Term → TC (RingOperatorTerms × List Name) +ringOperatorTerms `R = do + `R' ← headReduce 16 `R + case `R' of λ where + (con _ args) → case List.mapMaybe getVisible args of λ where + (_ ∷ _ ∷ a ∷ m ∷ z ∷ o ∷ _ ∷ []) → do + a' ← headReduce 16 a + m' ← headReduce 16 m + z' ← headReduce 16 z + o' ← headReduce 16 o + let ops = add⇒ a' mul⇒ m' zero⇒ z' one⇒ o' + pure (ops , pickDefName a' (pickDefName m' (pickDefName z' (pickDefName o' [])))) + _ → fallback + _ → fallback + where + fallback : TC (RingOperatorTerms × List Name) + fallback = do + ops ← RingReflection.abstractRingOperatorTerms `R + pure (ops , []) + +------------------------------------------------------------------------ +-- `solve-≈`: closed-equation form with auto-quantification. + +malformedClosedEqError : ∀ {a} {A : Set a} → Term → TC A +malformedClosedEqError found = typeError + ( strErr "Malformed call to solve-≈." + ∷ strErr "Expected target type to be of shape LHS ≈ RHS." + ∷ strErr "Instead: " + ∷ termErr found + ∷ []) + +-- Atom-lookup fallback: given a Term, return its polynomial-var +-- form if it appears in the atoms list, else `con 0`. +atomFallback : Term → ℕ → List Term → Term → Term +atomFallback `R↑ numAtoms atoms t with findAtomIndex t atoms +... | just i = toVarTerm `R↑ numAtoms i +... | nothing = `con `R↑ numAtoms (toTerm 0) + +solve-≈-macro : Term → Term → TC ⊤ +solve-≈-macro `R hole = do + `R' ← checkIsRing `R + commitTC + operatorTerms , bundleNs ← ringOperatorTerms `R' + + `hole₀ ← inferType hole + let _ , equation₀ = stripPis `hole₀ + opNamesFromGoal ← case getVisibleArgs 2 equation₀ of λ where + (just (lhs₀ ∷ rhs₀ ∷ [])) → do + ns ← collectOpNames operatorTerms lhs₀ [] + collectOpNames operatorTerms rhs₀ ns + _ → pure [] + let opNames = bundleNs ++ opNamesFromGoal + + B.withReduceDefs (false , opNames) $ do + -- Use `normalise` (not `reduce`) here: Agda's elaborator can + -- leave the goal type wrapped in lambdas; `normalise` β-reduces + -- those away. + `hole ← normalise `hole₀ + + -- Detect the deadlock: the goal contains metavariables that + -- only this macro could resolve, so `blockOnMeta` would retry + -- forever. We flag this when both sides have structure (so + -- neither is a bare meta `blockOnMeta` could fill in via sibling + -- constraints), some side has metas, AND no meta is shared + -- across the equation. + -- + -- A meta shared between LHS and RHS can be resolved by Agda + -- propagating constraints across the equation, so we defer those + -- to `blockOnMeta` instead of erroring. + let _ , equationProbe = stripPis `hole + case getVisibleArgs 2 equationProbe of λ where + (just (lhs₀ ∷ rhs₀ ∷ [])) → do + let bothStructured = not (bareMeta lhs₀) ∧ not (bareMeta rhs₀) + let metasL = metasOf lhs₀ + let metasR = metasOf rhs₀ + let anyMetas = not (null metasL ∧ null metasR) + let sharedMeta = shareMeta metasL metasR + case bothStructured ∧ anyMetas ∧ not sharedMeta of λ where + true → typeError + ( strErr "solve-≈: the goal `LHS ≈ RHS` has at least one side " + ∷ strErr "containing an metavariable that could not be resolved. To run this " + ∷ strErr "solver you must add type annotations to resolve these variables." + ∷ []) + false → pure tt + _ → pure tt + + -- Block on any unresolved meta in the goal type so Agda's + -- elaborator has a chance to resolve it via adjacent constraints. + case firstMeta `hole of λ where + (just m) → blockOnMeta m + nothing → pure tt + let variablesAndTypes , equation = stripPis `hole + let variables = List.map proj₁ variablesAndTypes + let numPiVars = List.length variables + + just (lhs ∷ rhs ∷ []) ← pure (getVisibleArgs 2 equation) + where nothing → malformedClosedEqError `hole + + -- Pass 1: collect atoms from LHS, then from RHS (preserving order). + atoms₀ ← collectAtoms operatorTerms lhs [] + atoms ← collectAtoms operatorTerms rhs atoms₀ + let numAtoms = List.length atoms + + -- Pass 2: convert with an atom-lookup fallback. The polynomial + -- body lives at depth `numPiVars + numAtoms` relative to the + -- macro's call-site (the wrapper lambdas re-introducing the + -- pi-binders, then the polynomial-lambda's binders inside). + let `R↓↓ = weaken (numPiVars + numAtoms) `R + `lhsExpr ← convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) lhs + `rhsExpr ← convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) rhs + + -- Build the lambda body and the `solve R N f refl atoms` term. + -- At the wrapper-lambda level, depth is `numPiVars`; we use + -- `R↓ = weaken numPiVars R` for `solver`/`refl`. + let `R↓ = weaken numPiVars `R + let lambdaBody = `:= `R↓↓ numAtoms `lhsExpr `rhsExpr + let f = prependVLams (replicate numAtoms "x") lambdaBody + let bare = `solver `R↓ numAtoms f (`refl `R↓) + let solverCall = applyVisibleArgs bare atoms + + -- Wrap with the pi-binders that the user didn't introduce as patterns + unify hole (prependVLams variables solverCall) + +macro + solve-≈ : Term → Term → TC ⊤ + solve-≈ = solve-≈-macro diff --git a/Tactic/Solver/Ring/Tests.agda b/Tactic/Solver/Ring/Tests.agda new file mode 100644 index 0000000..20444bf --- /dev/null +++ b/Tactic/Solver/Ring/Tests.agda @@ -0,0 +1,5 @@ +module Tactic.Solver.Ring.Tests where + +open import Tactic.Solver.Ring.Tests.Equations +open import Tactic.Solver.Ring.Tests.BundleVariants +open import Tactic.Solver.Ring.Tests.Comparison diff --git a/Tactic/Solver/Ring/Tests/BundleVariants.agda b/Tactic/Solver/Ring/Tests/BundleVariants.agda new file mode 100644 index 0000000..8245464 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/BundleVariants.agda @@ -0,0 +1,215 @@ +------------------------------------------------------------------------ +-- 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.Base as ℤB +open import Data.Integer.Properties as ℤP + using (+-*-commutativeSemiring) +open import Data.Nat as ℕ using (ℕ) +import Data.Nat.Base as ℕB +open import Data.Nat.Properties as ℕP +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 = ℤ + ; _≈_ = _≡_ + ; _+_ = ℤB._+_ + ; _*_ = ℤB._*_ + ; 0# = ℤB.+ 0 + ; 1# = ℤB.+ 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.+ b + ; _*_ = λ a b → a ℤB.* b + ; 0# = ℤB.+ 0 + ; 1# = ℤB.+ 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 = ℕ + ; _≈_ = _≡_ + ; _+_ = ℕB._+_ + ; _*_ = ℕB._*_ + ; 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 (ℤB.+ 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# = ℤB.+ 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.+ b + ; _*_ = λ a b → a ℤB.* 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 +-- `ℤB._*_`, 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. + +open import Data.Sign.Base as Sign using (Sign) + +myZInlined : CommutativeSemiring _ _ +myZInlined = record ℤP.+-*-commutativeSemiring + { _*_ = λ i j → ℤB.sign i Sign.* ℤB.sign j ℤB.◃ ℤB.∣ i ∣ ℕB.* ℤB.∣ 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/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..ab69b34 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/Equations.agda @@ -0,0 +1,596 @@ +{-# 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 +-- +-- 1. `solve-≈` currently only speaks the language of semirings, so +-- there's no negation. +-- +-- 2. `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 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 From 92ba06af08efb2f7245bdbfecd7223c66c230f5e Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Mon, 18 May 2026 20:25:24 +0200 Subject: [PATCH 2/5] Tactic.Solver.Ring: simplify and reorganise --- Reflection/Utils/Args.agda | 19 +- Reflection/Utils/Core.agda | 36 +++- Reflection/Utils/Metas.agda | 14 +- Reflection/Utils/TCM.agda | 45 ++++ Tactic/Solver/Ring.agda | 404 ++++++++++-------------------------- 5 files changed, 216 insertions(+), 302 deletions(-) diff --git a/Reflection/Utils/Args.agda b/Reflection/Utils/Args.agda index 4126bc3..31800b1 100644 --- a/Reflection/Utils/Args.agda +++ b/Reflection/Utils/Args.agda @@ -4,8 +4,11 @@ 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) 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 @@ -33,6 +36,20 @@ vArgs = λ where (vArg x ∷ xs) → x ∷ vArgs xs (_ ∷ xs) → vArgs xs +private + 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) + +-- 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..7d9e6fe 100644 --- a/Reflection/Utils/Metas.agda +++ b/Reflection/Utils/Metas.agda @@ -4,7 +4,7 @@ module Reflection.Utils.Metas where open import Meta.Prelude open import Meta.Init -open import Data.List using (_++_) +open import Data.List using (_++_; mapMaybe) isMeta : Term → Bool isMeta = λ where @@ -35,3 +35,15 @@ 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 t = case findMetaIds t of λ where + [] → nothing + (m ∷ _) → just m diff --git a/Reflection/Utils/TCM.agda b/Reflection/Utils/TCM.agda index 6f872ef..6d64989 100644 --- a/Reflection/Utils/TCM.agda +++ b/Reflection/Utils/TCM.agda @@ -9,3 +9,48 @@ 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') diff --git a/Tactic/Solver/Ring.agda b/Tactic/Solver/Ring.agda index dbbe1f3..35a1139 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring.agda @@ -10,13 +10,13 @@ module Tactic.Solver.Ring where open import Algebra using (CommutativeSemiring) -open import Data.Fin.Base as Fin using (Fin; toℕ) +open import Data.Fin.Base using (Fin) open import Data.Vec.Base as Vec using (Vec; _∷_; []) -open import Data.List.Base as List using (List; _∷_; []; _++_; replicate; foldr; findIndexᵇ; null) +open import Data.List.Base as List using (List; _∷_; []; _++_; replicate; foldr; null) open import Data.Bool.ListAction using (any) open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) open import Data.Nat.Base using (ℕ; suc; zero; _+_) -open import Data.Bool.Base using (Bool; if_then_else_; true; false; _∨_; _∧_; not) +open import Data.Bool.Base using (Bool; if_then_else_; true; false; _∧_; not) open import Data.Unit.Base using (⊤; tt) open import Data.Product.Base using (_,_; _×_; proj₁) open import Function.Base @@ -32,55 +32,12 @@ open import Reflection.TCM.Syntax import Agda.Builtin.Reflection as B using (withReduceDefs) open import Data.Nat.Reflection -import Data.Vec.Reflection as Vec - ------------------------------------------------------------------------- --- I. Generic reflection utilities. --- --- Everything in this section is independent of `CommutativeSemiring` --- (and the polynomial layer): plain helpers for inspecting and --- manipulating reflected `Term`s, deduplicating name/atom lists, --- chasing metavariables, and reducing `def`-chains further than --- Agda's primitive `reduce` does. ------------------------------------------------------------------------- +open import Reflection.Utils.Args using (getVisibleArgs; vArgs) +open import Reflection.Utils.Core using (extractNat; pickDefName; insertName; insertAtom; findAtomIndex) +open import Reflection.Utils.Metas using (isMeta; firstMeta; findMetaIds) +open import Reflection.Utils.TCM using (headReduce) private - ---------------------------------------------------------------------- - -- Arg/Term inspection - ---------------------------------------------------------------------- - - getVisible : Arg Term → Maybe Term - getVisible (arg (arg-info visible _) x) = just x - getVisible _ = nothing - - -- Extract the head `Name` of a term, peeling off any leading λ-binders. - 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 - - -- Try to extract a ℕ value from an iterated `suc`/`zero` - -- constructor chain (or a built-in `lit (nat n)` literal). - -- Returns `nothing` if the term is not a ℕ literal. - extractNat : Term → Maybe ℕ - extractNatArgs : Args Term → Maybe ℕ - - extractNat (lit (nat n)) = just n - extractNat (con nm xs) = - if nm Name.≡ᵇ quote zero then just 0 - else if nm Name.≡ᵇ quote suc then extractNatArgs xs - else nothing - extractNat _ = nothing - - extractNatArgs (arg (arg-info visible _) x ∷ []) = Maybe.map suc (extractNat x) - extractNatArgs (_ ∷ xs) = extractNatArgs xs - extractNatArgs [] = nothing - -- Try `extractNat` first; if that fails and we have a wrapping -- constructor name (e.g. ℤ's `+_ : ℕ → ℤ`), peel one layer of -- `con C (arg ∷ [])` and try again. Used to recognise `(+ n)` @@ -88,143 +45,19 @@ private peelLitCon : Name → Term → Maybe ℕ peelLitCon C (con nm xs) with nm Name.≡ᵇ C ... | false = nothing - ... | true = case List.mapMaybe getVisible xs of λ where + ... | 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 - - getVisibleArgs : ∀ n → Term → Maybe (Vec Term n) - getVisibleArgs n (def _ xs) = Maybe.map Vec.reverse - (List.foldl f c (List.mapMaybe getVisible xs) n) - where - f : (∀ n → Maybe (Vec Term n)) → Term → ∀ n → Maybe (Vec Term n) - f xs x zero = just [] - f xs x (suc n) = Maybe.map (x ∷_) (xs n) - - c : ∀ n → Maybe (Vec Term n) - c zero = just [] - c (suc _ ) = nothing - getVisibleArgs _ _ = nothing - - ---------------------------------------------------------------------- - -- List dedup/lookup - ---------------------------------------------------------------------- - - 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 `t` into `xs` if not already present (α-equality). - insertAtom : Term → List Term → List Term - insertAtom t [] = t ∷ [] - insertAtom t (a ∷ as) = - if t =α= a then a ∷ as else a ∷ insertAtom t as - - findAtomIndex : Term → List Term → Maybe ℕ - findAtomIndex t xs = Maybe.map Fin.toℕ (findIndexᵇ (t =α=_) xs) - - ---------------------------------------------------------------------- - -- Definition inspection - ---------------------------------------------------------------------- - - noArgBody : Definition → Maybe Term - noArgBody (function (clause [] [] body ∷ _)) = just body - noArgBody _ = nothing - - -- Pick the def-Name out of a Term, potentially under η-expansion. - pickDefName : Term → List Name → List Name - pickDefName (def n _) xs = insertName n xs - pickDefName (lam _ (abs _ body)) xs = pickDefName body xs - pickDefName _ xs = xs - -mutual - headReduce : ℕ → Term → TC Term - headReduce 0 t = pure t - headReduce (suc k) (def nm []) = do - d ← getDefinition nm - case noArgBody d of λ where - (just body) → headReduce k body - nothing → 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') - ----------------------------------------------------------------------- --- Metavariable inspection (depth-first walk). ----------------------------------------------------------------------- - -mutual - collectMetasT : Term → List Meta → List Meta - collectMetasT (var _ xs) acc = collectMetasArgs xs acc - collectMetasT (con _ xs) acc = collectMetasArgs xs acc - collectMetasT (def _ xs) acc = collectMetasArgs xs acc - collectMetasT (lam _ (abs _ t)) acc = collectMetasT t acc - collectMetasT (pat-lam _ _) acc = acc - collectMetasT (pi (arg _ a) (abs _ b)) acc = collectMetasT b (collectMetasT a acc) - collectMetasT (agda-sort s) acc = collectMetasSort s acc - collectMetasT (lit _) acc = acc - collectMetasT (meta x _) acc = x ∷ acc - collectMetasT unknown acc = acc - - collectMetasArgs : Args Term → List Meta → List Meta - collectMetasArgs [] acc = acc - collectMetasArgs (arg _ x ∷ xs) acc = collectMetasArgs xs (collectMetasT x acc) - - collectMetasSort : Sort → List Meta → List Meta - collectMetasSort (set t) acc = collectMetasT t acc - collectMetasSort (lit _) acc = acc - collectMetasSort (prop t) acc = collectMetasT t acc - collectMetasSort (propLit _) acc = acc - collectMetasSort (inf _) acc = acc - collectMetasSort unknown acc = acc - -metasOf : Term → List Meta -metasOf t = collectMetasT t [] - -firstMeta : Term → Maybe Meta -firstMeta t = case metasOf t of λ where - [] → nothing - (m ∷ _) → just m - --- Do two meta-lists share an element? Used to distinguish --- "deadlock" goals (no shared meta — blocking won't propagate --- between the equation's sides) from goals where `blockOnMeta` --- can be expected to succeed. -shareMeta : List Meta → List Meta → Bool -shareMeta xs ys = any (λ x → any (Meta._≡ᵇ_ x) ys) xs - -bareMeta : Term → Bool -bareMeta (meta _ _) = true -bareMeta _ = false - ----------------------------------------------------------------------- --- Append a list of Terms as visible args to an existing `def`. ----------------------------------------------------------------------- - -applyVisibleArgs : Term → List Term → Term -applyVisibleArgs (def nm xs) atoms = def nm (xs ++ foldr _⟨∷⟩_ [] atoms) -applyVisibleArgs t _ = t -- shouldn't happen for our use + extractCarrierNat nothing t = extractNat t + extractCarrierNat (just C) t with extractNat t + ... | just n = just n + ... | nothing = peelLitCon C t ------------------------------------------------------------------------ --- II. CommutativeSemiring-specific machinery. +-- CommutativeSemiring-specific machinery. ------------------------------------------------------------------------ module Solver {c ℓ} (R : CommutativeSemiring c ℓ) where @@ -252,7 +85,7 @@ record RingOperatorTerms : Set where -- shape `con C (n ∷ [])` with extracted ℕ values `0` and `1`. litConstructor : RingOperatorTerms → Maybe Name litConstructor (add⇒ _ mul⇒ _ zero⇒ con cz argsZ one⇒ con co argsO) = - check (cz Name.≡ᵇ co) (List.mapMaybe getVisible argsZ) (List.mapMaybe getVisible argsO) + check (cz Name.≡ᵇ co) (vArgs argsZ) (vArgs argsO) where check : Bool → List Term → List Term → Maybe Name check true (z₀ ∷ []) (o₀ ∷ []) with extractNat z₀ | extractNat o₀ @@ -264,50 +97,43 @@ litConstructor _ = nothing data RingOpKind : Set where isAdd isMul isZero isOne otherOp : RingOpKind --- Match a `Name` against the four operator Terms. -classifyOp : RingOperatorTerms → Name → TC RingOpKind -classifyOp ops nm = do - nameTerm ← normalise (def nm []) - let nmH = just nm - let match : Term → Bool - match t = (nameTerm =α= t) ∨ (nmH ≡ᵐ headName t) - pure (if match (RingOperatorTerms.add ops) then isAdd - else if match (RingOperatorTerms.mul ops) then isMul - else if match (RingOperatorTerms.zero# ops) then isZero - else if match (RingOperatorTerms.one# ops) then isOne - else otherOp) +-- Match a `Name` against the four operator Terms. Peels leading +-- λ-binders so η-expanded operators match too. +classifyOp : RingOperatorTerms → Name → RingOpKind +classifyOp (add⇒ a mul⇒ m zero⇒ z one⇒ o) nm = + if match a then isAdd + else if match m then isMul + else if match z then isZero + else if match o then isOne + else otherOp + where + match : Term → Bool + match (def nm' _) = nm' Name.≡ᵇ nm + match (lam _ (abs _ body)) = match body + match _ = false checkIsRing : Term → TC Term checkIsRing ring = checkType ring `CommutativeSemiring -module RingReflection (`R : Term) where - - -- `nm $ʳ args` produces `def nm (2 hidden ⊕ R ⊕ args)`, mirroring - -- the calling convention of every `Solver` re-export. - infixr 6 _$ʳ_ - _$ʳ_ : Name → Args Term → Term - nm $ʳ args = def nm (2 ⋯⟅∷⟆ `R ⟨∷⟩ args) - - -- Fallback `RingOperatorTerms` for abstract bundles (e.g. a module - -- parameter): each operator is the bundle projection applied to - -- `R`. Used when `R` is not a concrete top-level `def`, so we can't - -- `getDefinition` it to peek at the fields. - abstractRingOperatorTerms : TC RingOperatorTerms - abstractRingOperatorTerms = ⦇ - add⇒ normalise (def (quote CommutativeSemiring._+_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - mul⇒ normalise (def (quote CommutativeSemiring._*_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - zero⇒ normalise (def (quote CommutativeSemiring.0#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - one⇒ normalise (def (quote CommutativeSemiring.1#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - ⦈ - - `refl : Term - `refl = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ `R ⟨∷⟩ 1 ⋯⟅∷⟆ []) +-- Fallback `RingOperatorTerms` for abstract bundles (e.g. a module +-- parameter): each operator is the bundle projection applied to +-- `R`. Used when `R` is not a concrete top-level `def`, so we can't +-- `getDefinition` it to peek at the fields. +abstractRingOperatorTerms : Term → TC RingOperatorTerms +abstractRingOperatorTerms `R = ⦇ + add⇒ normalise (def (quote CommutativeSemiring._+_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + mul⇒ normalise (def (quote CommutativeSemiring._*_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + zero⇒ normalise (def (quote CommutativeSemiring.0#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + one⇒ normalise (def (quote CommutativeSemiring.1#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) + ⦈ + +`refl : Term → Term +`refl `R = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ `R ⟨∷⟩ 1 ⋯⟅∷⟆ []) ------------------------------------------------------------------------ -- Reflection utilities for the polynomial layer. module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where - open RingReflection `R `numberOfVariables : Term `numberOfVariables = toTerm numberOfVariables @@ -331,9 +157,9 @@ module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where `:= : Term → Term → Term `:= x y = quote Solver._:=_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) - `solver : Term → Term → Term - `solver `f `eq = def (quote Solver.solve) - (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟨∷⟩ `f ⟨∷⟩ `eq ⟨∷⟩ []) + `solver : Term → Term → List Term → Term + `solver `f `eq atoms = def (quote Solver.solve) + (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟨∷⟩ `f ⟨∷⟩ `eq ⟨∷⟩ foldr _⟨∷⟩_ [] atoms) toVarTerm : ℕ → Term toVarTerm i = `var (toFinTerm i) @@ -352,7 +178,7 @@ module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where -- For anything else we call the supplied `fallback`, which `solve-≈` -- uses to look the term up in an atom table and emit -- `varP (Fin i)` for the matching atom (auto-quantification). - convertTerm : RingOperatorTerms → (Term → Term) → Term → TC Term + convertTerm : RingOperatorTerms → (Term → Term) → Term → Term convertTerm operatorTerms fallback = convert where litCon : Maybe Name @@ -361,99 +187,83 @@ module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where mutual -- Try literal recognition first; then strip a `suc` and emit -- `con 1 :+ convert inner`; otherwise dispatch on the head. - convert : Term → TC Term + convert : Term → Term convert t with extractCarrierNat litCon t - ... | just n = pure (`con (toTerm n)) + ... | just n = `con (toTerm n) ... | nothing = convertHead t - convertHead : Term → TC Term - convertHead (def nm xs) = do - kind ← classifyOp operatorTerms nm - case kind of λ where - isAdd → convertOp₂ `:+ xs - isMul → convertOp₂ `:* xs - isZero → pure (`con (toTerm 0)) - isOne → pure (`con (toTerm 1)) - otherOp → pure (fallback (def nm xs)) + convertHead : Term → Term + convertHead (def nm xs) = case classifyOp operatorTerms nm of λ where + isAdd → convertOp₂ `:+ xs + isMul → convertOp₂ `:* xs + isZero → `con (toTerm 0) + isOne → `con (toTerm 1) + otherOp → fallback (def nm xs) convertHead t@(con nm xs) with nm Name.≡ᵇ quote suc | xs - ... | true | arg (arg-info visible _) x ∷ [] = do - inner ← convert x - pure (`:+ (`con (toTerm 1)) inner) - ... | _ | _ = pure (fallback t) - convertHead t = pure (fallback t) - - convertOp₂ : (Term → Term → Term) → Args Term → TC Term - convertOp₂ mk (x ⟨∷⟩ y ⟨∷⟩ []) = do - x' ← convert x - y' ← convert y - pure (mk x' y') + ... | true | arg (arg-info visible _) x ∷ [] = `:+ (`con (toTerm 1)) (convert x) + ... | _ | _ = fallback t + convertHead t = fallback t + + convertOp₂ : (Term → Term → Term) → Args Term → Term + convertOp₂ mk (x ⟨∷⟩ y ⟨∷⟩ []) = mk (convert x) (convert y) convertOp₂ mk (x ∷ xs) = convertOp₂ mk xs - convertOp₂ _ _ = pure (`con (toTerm 0)) + convertOp₂ _ _ = `con (toTerm 0) ------------------------------------------------------------------------ -open RingReflection open RingSolverReflection -- Collect the def-Names of every recognised ring-operator occurrence -- in the user term (used to seed the `withReduceDefs` block list). -collectOpNames : RingOperatorTerms → Term → List Name → TC (List Name) +collectOpNames : RingOperatorTerms → Term → List Name → List Name collectOpNames operatorTerms = collect where mutual - collect : Term → List Name → TC (List Name) - collect (def nm xs) acc = do - kind ← classifyOp operatorTerms nm - case kind of λ where - otherOp → pure acc - isZero → pure (insertName nm acc) - isOne → pure (insertName nm acc) - isAdd → collectArgs xs (insertName nm acc) - isMul → collectArgs xs (insertName nm acc) - collect _ acc = pure acc - - collectArgs : Args Term → List Name → TC (List Name) - collectArgs [] acc = pure acc - collectArgs (arg (arg-info visible _) x ∷ xs) acc = do - acc1 ← collect x acc - collectArgs xs acc1 + collect : Term → List Name → List Name + collect (def nm xs) acc = case classifyOp operatorTerms nm of λ where + otherOp → acc + isZero → insertName nm acc + isOne → insertName nm acc + isAdd → collectArgs xs (insertName nm acc) + isMul → collectArgs xs (insertName nm acc) + collect _ acc = acc + + collectArgs : Args Term → List Name → List Name + collectArgs [] acc = acc + collectArgs (arg (arg-info visible _) x ∷ xs) acc = collectArgs xs (collect x acc) collectArgs (_ ∷ xs) acc = collectArgs xs acc -- Walk a Term, accumulating atomic subterms into the supplied list. -- Operators and ℕ literals are decomposed/skipped; anything else -- becomes an atom. -collectAtoms : RingOperatorTerms → Term → List Term → TC (List Term) +collectAtoms : RingOperatorTerms → Term → List Term → List Term collectAtoms operatorTerms = collect where litCon : Maybe Name litCon = litConstructor operatorTerms mutual - collect : Term → List Term → TC (List Term) + collect : Term → List Term → List Term collect t acc with extractCarrierNat litCon t - ... | just _ = pure acc + ... | just _ = acc ... | nothing = collectHead t acc - collectHead : Term → List Term → TC (List Term) - collectHead (def nm xs) acc = do - kind ← classifyOp operatorTerms nm - case kind of λ where - isAdd → collectOp₂ xs acc - isMul → collectOp₂ xs acc - isZero → pure acc - isOne → pure acc - otherOp → pure (insertAtom (def nm xs) acc) + collectHead : Term → List Term → List Term + collectHead (def nm xs) acc = case classifyOp operatorTerms nm of λ where + isAdd → collectOp₂ xs acc + isMul → collectOp₂ xs acc + isZero → acc + isOne → acc + otherOp → insertAtom (def nm xs) acc collectHead t@(con nm xs) acc with nm Name.≡ᵇ quote suc | xs ... | true | arg (arg-info visible _) x ∷ [] = collect x acc - ... | _ | _ = pure (insertAtom t acc) - collectHead t acc = pure (insertAtom t acc) + ... | _ | _ = insertAtom t acc + collectHead t acc = insertAtom t acc - collectOp₂ : Args Term → List Term → TC (List Term) - collectOp₂ (x ⟨∷⟩ y ⟨∷⟩ []) acc = do - acc1 ← collect x acc - collect y acc1 + collectOp₂ : Args Term → List Term → List Term + collectOp₂ (x ⟨∷⟩ y ⟨∷⟩ []) acc = collect y (collect x acc) collectOp₂ (x ∷ xs) acc = collectOp₂ xs acc - collectOp₂ [] acc = pure acc + collectOp₂ [] acc = acc ------------------------------------------------------------------------ -- Inspect a bundle term `R` and produce its `RingOperatorTerms` @@ -464,20 +274,20 @@ ringOperatorTerms : Term → TC (RingOperatorTerms × List Name) ringOperatorTerms `R = do `R' ← headReduce 16 `R case `R' of λ where - (con _ args) → case List.mapMaybe getVisible args of λ where + (con _ args) → case vArgs args of λ where (_ ∷ _ ∷ a ∷ m ∷ z ∷ o ∷ _ ∷ []) → do a' ← headReduce 16 a m' ← headReduce 16 m z' ← headReduce 16 z o' ← headReduce 16 o let ops = add⇒ a' mul⇒ m' zero⇒ z' one⇒ o' - pure (ops , pickDefName a' (pickDefName m' (pickDefName z' (pickDefName o' [])))) + pure (ops , foldr pickDefName [] (a' ∷ m' ∷ z' ∷ o' ∷ [])) _ → fallback _ → fallback where fallback : TC (RingOperatorTerms × List Name) fallback = do - ops ← RingReflection.abstractRingOperatorTerms `R + ops ← abstractRingOperatorTerms `R pure (ops , []) ------------------------------------------------------------------------ @@ -506,11 +316,9 @@ solve-≈-macro `R hole = do `hole₀ ← inferType hole let _ , equation₀ = stripPis `hole₀ - opNamesFromGoal ← case getVisibleArgs 2 equation₀ of λ where - (just (lhs₀ ∷ rhs₀ ∷ [])) → do - ns ← collectOpNames operatorTerms lhs₀ [] - collectOpNames operatorTerms rhs₀ ns - _ → pure [] + let opNamesFromGoal = case getVisibleArgs 2 equation₀ of λ where + (just (lhs₀ ∷ rhs₀ ∷ [])) → collectOpNames operatorTerms rhs₀ (collectOpNames operatorTerms lhs₀ []) + _ → [] let opNames = bundleNs ++ opNamesFromGoal B.withReduceDefs (false , opNames) $ do @@ -532,11 +340,11 @@ solve-≈-macro `R hole = do let _ , equationProbe = stripPis `hole case getVisibleArgs 2 equationProbe of λ where (just (lhs₀ ∷ rhs₀ ∷ [])) → do - let bothStructured = not (bareMeta lhs₀) ∧ not (bareMeta rhs₀) - let metasL = metasOf lhs₀ - let metasR = metasOf rhs₀ + 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 + let sharedMeta = any (λ x → any (Meta._≡ᵇ_ x) metasR) metasL case bothStructured ∧ anyMetas ∧ not sharedMeta of λ where true → typeError ( strErr "solve-≈: the goal `LHS ≈ RHS` has at least one side " @@ -556,11 +364,10 @@ solve-≈-macro `R hole = do let numPiVars = List.length variables just (lhs ∷ rhs ∷ []) ← pure (getVisibleArgs 2 equation) - where nothing → malformedClosedEqError `hole + where _ → malformedClosedEqError `hole -- Pass 1: collect atoms from LHS, then from RHS (preserving order). - atoms₀ ← collectAtoms operatorTerms lhs [] - atoms ← collectAtoms operatorTerms rhs atoms₀ + let atoms = collectAtoms operatorTerms rhs (collectAtoms operatorTerms lhs []) let numAtoms = List.length atoms -- Pass 2: convert with an atom-lookup fallback. The polynomial @@ -568,8 +375,8 @@ solve-≈-macro `R hole = do -- macro's call-site (the wrapper lambdas re-introducing the -- pi-binders, then the polynomial-lambda's binders inside). let `R↓↓ = weaken (numPiVars + numAtoms) `R - `lhsExpr ← convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) lhs - `rhsExpr ← convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) rhs + let `lhsExpr = convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) lhs + let `rhsExpr = convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) rhs -- Build the lambda body and the `solve R N f refl atoms` term. -- At the wrapper-lambda level, depth is `numPiVars`; we use @@ -577,8 +384,7 @@ solve-≈-macro `R hole = do let `R↓ = weaken numPiVars `R let lambdaBody = `:= `R↓↓ numAtoms `lhsExpr `rhsExpr let f = prependVLams (replicate numAtoms "x") lambdaBody - let bare = `solver `R↓ numAtoms f (`refl `R↓) - let solverCall = applyVisibleArgs bare atoms + let solverCall = `solver `R↓ numAtoms f (`refl `R↓) atoms -- Wrap with the pi-binders that the user didn't introduce as patterns unify hole (prependVLams variables solverCall) From 146293ef83698487956952a2a0536d75bc63787c Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Fri, 22 May 2026 12:18:59 +0200 Subject: [PATCH 3/5] Tactic.Solver.Ring: refactor onto a generic Theory abstraction Extracts the structure-independent parts of the ring solver (atom collection, two-pass polynomial-AST conversion, deadlock detection, auto-quantification, reflection plumbing) into a new generic core `Tactic.Solver.Algebra`, parameterised by a `Theory` record that describes a particular algebraic structure. The ring solver is now an instantiation of this core for `CommutativeSemiring` against stdlib's `Algebra.Solver.Ring.NaturalCoefficients.Default`. --- Reflection/Utils/Args.agda | 14 +- Reflection/Utils/Metas.agda | 11 +- Tactic/Solver/Algebra.agda | 335 ++++++++++ Tactic/Solver/Ring.agda | 624 ++++++++----------- Tactic/Solver/Ring/Tests/BundleVariants.agda | 49 +- 5 files changed, 644 insertions(+), 389 deletions(-) create mode 100644 Tactic/Solver/Algebra.agda diff --git a/Reflection/Utils/Args.agda b/Reflection/Utils/Args.agda index 31800b1..f6f735a 100644 --- a/Reflection/Utils/Args.agda +++ b/Reflection/Utils/Args.agda @@ -4,7 +4,7 @@ module Reflection.Utils.Args where open import Meta.Prelude open import Meta.Init -open import Data.List using (map; zip; reverse) +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 @@ -14,6 +14,11 @@ 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 @@ -36,11 +41,8 @@ vArgs = λ where (vArg x ∷ xs) → x ∷ vArgs xs (_ ∷ xs) → vArgs xs -private - 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) +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 diff --git a/Reflection/Utils/Metas.agda b/Reflection/Utils/Metas.agda index 7d9e6fe..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 (_++_; mapMaybe) +import Data.Bool.ListAction as B +open import Data.List +import Reflection.AST.Meta as Meta isMeta : Term → Bool isMeta = λ where @@ -44,6 +46,7 @@ findMetaIds : Term → List Meta findMetaIds = mapMaybe metaId ∘ findMetas firstMeta : Term → Maybe Meta -firstMeta t = case findMetaIds t of λ where - [] → nothing - (m ∷ _) → just m +firstMeta = head ∘ findMetaIds + +shareMeta : List Meta → List Meta → Bool +shareMeta xs ys = B.any (λ x → B.any (Meta._≡ᵇ_ x) ys) xs 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 index 35a1139..7e32745 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring.agda @@ -1,393 +1,313 @@ ------------------------------------------------------------------------ --- An improved ring solver, based on the stdlib's one +-- A reflection-based ring solver for `CommutativeSemiring`. -- --- Automatically handles variable introduction as required, properly --- deals with most literals, has sensible defaults and a few other --- bells and whistles. Also has an extensive test suite. +-- `solve-≈` instantiates `Algebra.Solver.Ring.NaturalCoefficients.Default R` +-- (ℕ coefficients, no negation) by reflecting the user's bundle into +-- the polynomial AST and discharging the resulting equation. +-- +-- 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) -open import Data.Fin.Base using (Fin) -open import Data.Vec.Base as Vec using (Vec; _∷_; []) -open import Data.List.Base as List using (List; _∷_; []; _++_; replicate; foldr; null) -open import Data.Bool.ListAction using (any) -open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) -open import Data.Nat.Base using (ℕ; suc; zero; _+_) -open import Data.Bool.Base using (Bool; if_then_else_; true; false; _∧_; not) -open import Data.Unit.Base using (⊤; tt) -open import Data.Product.Base using (_,_; _×_; proj₁) -open import Function.Base + +open import Data.Bool using (Bool; true; false) +open import Data.Fin using (Fin) +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 -open import Reflection.AST.Term -open import Reflection.AST.AlphaEquality -open import Reflection.AST.DeBruijn using (weaken) import Reflection.AST.Name as Name -import Reflection.AST.Meta as Meta -open import Reflection.TCM.Syntax -import Agda.Builtin.Reflection as B - using (withReduceDefs) -open import Data.Nat.Reflection -open import Reflection.Utils.Args using (getVisibleArgs; vArgs) -open import Reflection.Utils.Core using (extractNat; pickDefName; insertName; insertAtom; findAtomIndex) -open import Reflection.Utils.Metas using (isMeta; firstMeta; findMetaIds) -open import Reflection.Utils.TCM using (headReduce) +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) -private - -- Try `extractNat` first; if that fails and we have a wrapping - -- constructor name (e.g. ℤ's `+_ : ℕ → ℤ`), peel one layer of - -- `con C (arg ∷ [])` and try again. Used to recognise `(+ n)` - -- on ℤ as a polynomial constant. - peelLitCon : Name → Term → Maybe ℕ - peelLitCon C (con nm xs) with nm Name.≡ᵇ C - ... | false = nothing - ... | true = case vArgs xs of λ where - (a ∷ []) → extractNat a - _ → nothing - peelLitCon _ _ = nothing - - extractCarrierNat : Maybe Name → Term → Maybe ℕ - extractCarrierNat nothing t = extractNat t - extractCarrierNat (just C) t with extractNat t - ... | just n = just n - ... | nothing = peelLitCon C t +open import Tactic.Solver.Algebra ------------------------------------------------------------------------ --- CommutativeSemiring-specific machinery. ------------------------------------------------------------------------- +-- `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 - -- Constructor wrappers (using `con` directly via `quote` is - -- ambiguous because of name collisions across the imported chain). conP : ∀ {n} → ℕ → Polynomial n conP = con varP : ∀ {n} → Fin n → Polynomial n varP = var -`CommutativeSemiring : Term -`CommutativeSemiring = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) - -record RingOperatorTerms : Set where - constructor add⇒_mul⇒_zero⇒_one⇒_ - field - add mul zero# one# : Term - --- Try to detect a "carrier-nat constructor": a single-argument --- constructor `C : ℕ → Carrier` that wraps ℕ literals (e.g. ℤ's --- `+_`). We find it by checking that `zero#` and `one#` both have --- shape `con C (n ∷ [])` with extracted ℕ values `0` and `1`. -litConstructor : RingOperatorTerms → Maybe Name -litConstructor (add⇒ _ mul⇒ _ zero⇒ con cz argsZ one⇒ con co argsO) = - check (cz Name.≡ᵇ co) (vArgs argsZ) (vArgs argsO) - where - check : Bool → List Term → List Term → Maybe Name - check true (z₀ ∷ []) (o₀ ∷ []) with extractNat z₀ | extractNat o₀ - ... | just 0 | just 1 = just cz - ... | _ | _ = nothing - check _ _ _ = nothing -litConstructor _ = nothing - -data RingOpKind : Set where - isAdd isMul isZero isOne otherOp : RingOpKind - --- Match a `Name` against the four operator Terms. Peels leading --- λ-binders so η-expanded operators match too. -classifyOp : RingOperatorTerms → Name → RingOpKind -classifyOp (add⇒ a mul⇒ m zero⇒ z one⇒ o) nm = - if match a then isAdd - else if match m then isMul - else if match z then isZero - else if match o then isOne - else otherOp - where - match : Term → Bool - match (def nm' _) = nm' Name.≡ᵇ nm - match (lam _ (abs _ body)) = match body - match _ = false - -checkIsRing : Term → TC Term -checkIsRing ring = checkType ring `CommutativeSemiring - --- Fallback `RingOperatorTerms` for abstract bundles (e.g. a module --- parameter): each operator is the bundle projection applied to --- `R`. Used when `R` is not a concrete top-level `def`, so we can't --- `getDefinition` it to peek at the fields. -abstractRingOperatorTerms : Term → TC RingOperatorTerms -abstractRingOperatorTerms `R = ⦇ - add⇒ normalise (def (quote CommutativeSemiring._+_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - mul⇒ normalise (def (quote CommutativeSemiring._*_) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - zero⇒ normalise (def (quote CommutativeSemiring.0#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - one⇒ normalise (def (quote CommutativeSemiring.1#) (2 ⋯⟅∷⟆ `R ⟨∷⟩ [])) - ⦈ - -`refl : Term → Term -`refl `R = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ `R ⟨∷⟩ 1 ⋯⟅∷⟆ []) +------------------------------------------------------------------------ +-- Backend reflection helpers (private). + +private + 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# + + `CommutativeSemiring : Term + `CommutativeSemiring = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) + +------------------------------------------------------------------------ +-- Polynomial-AST Term builders. Calling shape: +-- `def NAME (2 hidden + R-bundle ⟨∷⟩ numVars ⟅∷⟆ ⟨args…⟩)`, +-- pulling NAMEs from `Solver.*`. + +private + defP : (R `n : Term) → Name → List (Arg Term) → Term + defP R `n nm args = + def nm (2 ⋯⟅∷⟆ R ⟨∷⟩ `n ⟅∷⟆ args) + + `con : (R `n : Term) → Term → Term + `con R `n c = defP R `n (quote Solver.conP) (c ⟨∷⟩ []) + + `var : (R `n : Term) → Term → Term + `var R `n i = defP R `n (quote Solver.varP) (i ⟨∷⟩ []) + + `:+ : (R `n : Term) → Term → Term → Term + `:+ R `n x y = defP R `n (quote Solver._:+_) (x ⟨∷⟩ y ⟨∷⟩ []) + + `:* : (R `n : Term) → Term → Term → Term + `:* R `n x y = defP R `n (quote Solver._:*_) (x ⟨∷⟩ y ⟨∷⟩ []) + + `:= : (R `n : Term) → Term → Term → Term + `:= R `n x y = defP R `n (quote Solver._:=_) (x ⟨∷⟩ y ⟨∷⟩ []) + + `refl : (R : Term) → Term + `refl R = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ R ⟨∷⟩ 1 ⋯⟅∷⟆ []) ------------------------------------------------------------------------ --- Reflection utilities for the polynomial layer. - -module RingSolverReflection (`R : Term) (numberOfVariables : ℕ) where - - `numberOfVariables : Term - `numberOfVariables = toTerm numberOfVariables - - infix -1 _$ᵖ_ - _$ᵖ_ : Name → List (Arg Term) → Term - nm $ᵖ xs = def nm (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟅∷⟆ xs) - - `con : Term → Term - `con n = quote Solver.conP $ᵖ (n ⟨∷⟩ []) - - `var : Term → Term - `var i = quote Solver.varP $ᵖ (i ⟨∷⟩ []) - - `:+ : Term → Term → Term - `:+ x y = quote Solver._:+_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) - - `:* : Term → Term → Term - `:* x y = quote Solver._:*_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) - - `:= : Term → Term → Term - `:= x y = quote Solver._:=_ $ᵖ (x ⟨∷⟩ y ⟨∷⟩ []) - - `solver : Term → Term → List Term → Term - `solver `f `eq atoms = def (quote Solver.solve) - (2 ⋯⟅∷⟆ `R ⟨∷⟩ `numberOfVariables ⟨∷⟩ `f ⟨∷⟩ `eq ⟨∷⟩ foldr _⟨∷⟩_ [] atoms) - - toVarTerm : ℕ → Term - toVarTerm i = `var (toFinTerm i) - - -- Convert raw user-Term to a Polynomial Term. - -- - -- We recognise: - -- * `_+_` / `_*_` as ring operators, including bundle-projection - -- forms used in parameterised modules; - -- * `0#` / `1#` as the polynomial constants `con 0` / `con 1`; - -- * `lit (nat n)`, `con suc^k zero`, and `con C (lit n)` for a - -- detected carrier-nat constructor `C` (e.g. ℤ's `+_`) — each - -- decoded into `con n`; - -- * `suc t` where `t` is non-literal — peeled into `con 1 :+ t`. - -- - -- For anything else we call the supplied `fallback`, which `solve-≈` - -- uses to look the term up in an atom table and emit - -- `varP (Fin i)` for the matching atom (auto-quantification). - convertTerm : RingOperatorTerms → (Term → Term) → Term → Term - convertTerm operatorTerms fallback = convert +-- 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 - litCon : Maybe Name - litCon = litConstructor operatorTerms - - mutual - -- Try literal recognition first; then strip a `suc` and emit - -- `con 1 :+ convert inner`; otherwise dispatch on the head. - convert : Term → Term - convert t with extractCarrierNat litCon t - ... | just n = `con (toTerm n) - ... | nothing = convertHead t - - convertHead : Term → Term - convertHead (def nm xs) = case classifyOp operatorTerms nm of λ where - isAdd → convertOp₂ `:+ xs - isMul → convertOp₂ `:* xs - isZero → `con (toTerm 0) - isOne → `con (toTerm 1) - otherOp → fallback (def nm xs) - convertHead t@(con nm xs) with nm Name.≡ᵇ quote suc | xs - ... | true | arg (arg-info visible _) x ∷ [] = `:+ (`con (toTerm 1)) (convert x) - ... | _ | _ = fallback t - convertHead t = fallback t - - convertOp₂ : (Term → Term → Term) → Args Term → Term - convertOp₂ mk (x ⟨∷⟩ y ⟨∷⟩ []) = mk (convert x) (convert y) - convertOp₂ mk (x ∷ xs) = convertOp₂ mk xs - convertOp₂ _ _ = `con (toTerm 0) + 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. -open RingSolverReflection - --- Collect the def-Names of every recognised ring-operator occurrence --- in the user term (used to seed the `withReduceDefs` block list). -collectOpNames : RingOperatorTerms → Term → List Name → List Name -collectOpNames operatorTerms = collect - where - mutual - collect : Term → List Name → List Name - collect (def nm xs) acc = case classifyOp operatorTerms nm of λ where - otherOp → acc - isZero → insertName nm acc - isOne → insertName nm acc - isAdd → collectArgs xs (insertName nm acc) - isMul → collectArgs xs (insertName nm acc) - collect _ acc = acc - - collectArgs : Args Term → List Name → List Name - collectArgs [] acc = acc - collectArgs (arg (arg-info visible _) x ∷ xs) acc = collectArgs xs (collect x acc) - collectArgs (_ ∷ xs) acc = collectArgs xs acc - --- Walk a Term, accumulating atomic subterms into the supplied list. --- Operators and ℕ literals are decomposed/skipped; anything else --- becomes an atom. -collectAtoms : RingOperatorTerms → Term → List Term → List Term -collectAtoms operatorTerms = collect - where - litCon : Maybe Name - litCon = litConstructor operatorTerms - - mutual - collect : Term → List Term → List Term - collect t acc with extractCarrierNat litCon t - ... | just _ = acc - ... | nothing = collectHead t acc - - collectHead : Term → List Term → List Term - collectHead (def nm xs) acc = case classifyOp operatorTerms nm of λ where - isAdd → collectOp₂ xs acc - isMul → collectOp₂ xs acc - isZero → acc - isOne → acc - otherOp → insertAtom (def nm xs) acc - collectHead t@(con nm xs) acc with nm Name.≡ᵇ quote suc | xs - ... | true | arg (arg-info visible _) x ∷ [] = collect x acc - ... | _ | _ = insertAtom t acc - collectHead t acc = insertAtom t acc - - collectOp₂ : Args Term → List Term → List Term - collectOp₂ (x ⟨∷⟩ y ⟨∷⟩ []) acc = collect y (collect x acc) - collectOp₂ (x ∷ xs) acc = collectOp₂ xs acc - collectOp₂ [] acc = acc +private + collectDefNames : List Term → List Name + collectDefNames = List.foldr pickDefName [] + + -- A slot's role. `op` is a generic concrete operator field; + -- `zeroLit` and `oneLit` mark literals. (`derived` exists for + -- structures with non-field operators; CSR has none.) + 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) + ∷ [] + + 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 + + detectCSR : Term → TC (TheoryDetect × RingState) + detectCSR R = do + R' ← headReduce 16 R + let slots = csrSlots + 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 ⦄ (headReduce 16) rawOps + slotted ← zipSlots slots concOps + let blockNs = collectDefNames concOps + let ls = maybe (uncurry detectLitStyle) nothing (findZeroOne slotted) + 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 } + ) ------------------------------------------------------------------------ --- Inspect a bundle term `R` and produce its `RingOperatorTerms` --- plus the list of underlying field-value Names to block via --- `withReduceDefs`. - -ringOperatorTerms : Term → TC (RingOperatorTerms × List Name) -ringOperatorTerms `R = do - `R' ← headReduce 16 `R - case `R' of λ where - (con _ args) → case vArgs args of λ where - (_ ∷ _ ∷ a ∷ m ∷ z ∷ o ∷ _ ∷ []) → do - a' ← headReduce 16 a - m' ← headReduce 16 m - z' ← headReduce 16 z - o' ← headReduce 16 o - let ops = add⇒ a' mul⇒ m' zero⇒ z' one⇒ o' - pure (ops , foldr pickDefName [] (a' ∷ m' ∷ z' ∷ o' ∷ [])) - _ → fallback - _ → fallback - where - fallback : TC (RingOperatorTerms × List Name) - fallback = do - ops ← abstractRingOperatorTerms `R - pure (ops , []) +-- Encoder construction. + +private + mkEncode : (R↓↓ R↓ : Term) + → (numAtoms : ℕ) → Maybe LitStyle → TheoryEncode + mkEncode R↓↓ R↓ numAtoms litStyle = record + { opEncoders = opAdd ∷ opMul ∷ opZero ∷ opOne ∷ [] + ; encodeNat = encNat + ; sucPeel = sucPeelFn + ; encodeVar = encVar + ; encodeEq = `:= R↓↓ `n + ; finishSolve = finish + } + where + `n = toTerm numAtoms + + opAdd : List Term → Term + opAdd (x ∷ y ∷ _) = `:+ R↓↓ `n x y + opAdd _ = unknown + + opMul : List Term → Term + opMul (x ∷ y ∷ _) = `:* R↓↓ `n x y + opMul _ = unknown + + opZero : List Term → Term + opZero _ = `con R↓↓ `n (toTerm 0) + + opOne : List Term → Term + opOne _ = `con R↓↓ `n (toTerm 1) + + encNat : ℕ → Term + encNat n = `con R↓↓ `n (toTerm n) + + sucPeelFn : Term → Term + sucPeelFn inner = + `:+ R↓↓ `n (`con R↓↓ `n (toTerm 1)) inner + + encVar : ℕ → Term + encVar i = `var R↓↓ `n (toFinTerm i) + + finish : Term → List Term → Term + finish lambdaBody atoms = + def (quote Solver.solve) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ `n ⟨∷⟩ lambdaBody ⟨∷⟩ `refl R↓ ⟨∷⟩ List.map vArg atoms) ------------------------------------------------------------------------ --- `solve-≈`: closed-equation form with auto-quantification. - -malformedClosedEqError : ∀ {a} {A : Set a} → Term → TC A -malformedClosedEqError found = typeError - ( strErr "Malformed call to solve-≈." - ∷ strErr "Expected target type to be of shape LHS ≈ RHS." - ∷ strErr "Instead: " - ∷ termErr found - ∷ []) - --- Atom-lookup fallback: given a Term, return its polynomial-var --- form if it appears in the atoms list, else `con 0`. -atomFallback : Term → ℕ → List Term → Term → Term -atomFallback `R↑ numAtoms atoms t with findAtomIndex t atoms -... | just i = toVarTerm `R↑ numAtoms i -... | nothing = `con `R↑ numAtoms (toTerm 0) +-- The macro. + +private + csrTheory : Theory + csrTheory = record + { bundleType = `CommutativeSemiring + ; State = RingState + ; detect = detectCSR + ; encode = λ R↓↓ R↓ n st → mkEncode R↓↓ R↓ n (RingState.litStyle st) + } solve-≈-macro : Term → Term → TC ⊤ -solve-≈-macro `R hole = do - `R' ← checkIsRing `R +solve-≈-macro R hole = do + -- `commitTC` locks in `checkType`'s metavariable resolutions + -- before further work that depends on `R`'s type being settled. + -- `solveByTheory` deliberately doesn't redo the `checkType`. + R' ← checkType R `CommutativeSemiring commitTC - operatorTerms , bundleNs ← ringOperatorTerms `R' - - `hole₀ ← inferType hole - let _ , equation₀ = stripPis `hole₀ - let opNamesFromGoal = case getVisibleArgs 2 equation₀ of λ where - (just (lhs₀ ∷ rhs₀ ∷ [])) → collectOpNames operatorTerms rhs₀ (collectOpNames operatorTerms lhs₀ []) - _ → [] - let opNames = bundleNs ++ opNamesFromGoal - - B.withReduceDefs (false , opNames) $ do - -- Use `normalise` (not `reduce`) here: Agda's elaborator can - -- leave the goal type wrapped in lambdas; `normalise` β-reduces - -- those away. - `hole ← normalise `hole₀ - - -- Detect the deadlock: the goal contains metavariables that - -- only this macro could resolve, so `blockOnMeta` would retry - -- forever. We flag this when both sides have structure (so - -- neither is a bare meta `blockOnMeta` could fill in via sibling - -- constraints), some side has metas, AND no meta is shared - -- across the equation. - -- - -- A meta shared between LHS and RHS can be resolved by Agda - -- propagating constraints across the equation, so we defer those - -- to `blockOnMeta` instead of erroring. - let _ , equationProbe = stripPis `hole - case getVisibleArgs 2 equationProbe 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 = any (λ x → any (Meta._≡ᵇ_ x) metasR) metasL - case bothStructured ∧ anyMetas ∧ not sharedMeta of λ where - true → typeError - ( strErr "solve-≈: the goal `LHS ≈ RHS` has at least one side " - ∷ strErr "containing an metavariable that could not be resolved. To run this " - ∷ strErr "solver you must add type annotations to resolve these variables." - ∷ []) - false → pure tt - _ → pure tt - - -- Block on any unresolved meta in the goal type so Agda's - -- elaborator has a chance to resolve it via adjacent constraints. - case firstMeta `hole of λ where - (just m) → blockOnMeta m - nothing → pure tt - let variablesAndTypes , equation = stripPis `hole - let variables = List.map proj₁ variablesAndTypes - let numPiVars = List.length variables - - just (lhs ∷ rhs ∷ []) ← pure (getVisibleArgs 2 equation) - where _ → malformedClosedEqError `hole - - -- Pass 1: collect atoms from LHS, then from RHS (preserving order). - let atoms = collectAtoms operatorTerms rhs (collectAtoms operatorTerms lhs []) - let numAtoms = List.length atoms - - -- Pass 2: convert with an atom-lookup fallback. The polynomial - -- body lives at depth `numPiVars + numAtoms` relative to the - -- macro's call-site (the wrapper lambdas re-introducing the - -- pi-binders, then the polynomial-lambda's binders inside). - let `R↓↓ = weaken (numPiVars + numAtoms) `R - let `lhsExpr = convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) lhs - let `rhsExpr = convertTerm `R↓↓ numAtoms operatorTerms (atomFallback `R↓↓ numAtoms atoms) rhs - - -- Build the lambda body and the `solve R N f refl atoms` term. - -- At the wrapper-lambda level, depth is `numPiVars`; we use - -- `R↓ = weaken numPiVars R` for `solver`/`refl`. - let `R↓ = weaken numPiVars `R - let lambdaBody = `:= `R↓↓ numAtoms `lhsExpr `rhsExpr - let f = prependVLams (replicate numAtoms "x") lambdaBody - let solverCall = `solver `R↓ numAtoms f (`refl `R↓) atoms - - -- Wrap with the pi-binders that the user didn't introduce as patterns - unify hole (prependVLams variables solverCall) + solveByTheory csrTheory R' hole macro solve-≈ : Term → Term → TC ⊤ diff --git a/Tactic/Solver/Ring/Tests/BundleVariants.agda b/Tactic/Solver/Ring/Tests/BundleVariants.agda index 8245464..6903c56 100644 --- a/Tactic/Solver/Ring/Tests/BundleVariants.agda +++ b/Tactic/Solver/Ring/Tests/BundleVariants.agda @@ -8,15 +8,12 @@ module Tactic.Solver.Ring.Tests.BundleVariants where open import Algebra using (CommutativeSemiring) -open import Data.Integer as ℤ using (ℤ) -import Data.Integer.Base as ℤB -open import Data.Integer.Properties as ℤP - using (+-*-commutativeSemiring) -open import Data.Nat as ℕ using (ℕ) -import Data.Nat.Base as ℕB -open import Data.Nat.Properties as ℕP -open import Relation.Binary.PropositionalEquality - using (_≡_) +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-≈) ------------------------------------------------------------------------ @@ -41,10 +38,10 @@ myZ'' : CommutativeSemiring _ _ myZ'' = record { Carrier = ℤ ; _≈_ = _≡_ - ; _+_ = ℤB._+_ - ; _*_ = ℤB._*_ - ; 0# = ℤB.+ 0 - ; 1# = ℤB.+ 1 + ; _+_ = ℤ._+_ + ; _*_ = ℤ._*_ + ; 0# = ℤ.+ 0 + ; 1# = ℤ.+ 1 ; isCommutativeSemiring = ℤP.+-*-isCommutativeSemiring } @@ -64,10 +61,10 @@ myZη : CommutativeSemiring _ _ myZη = record { Carrier = ℤ ; _≈_ = _≡_ - ; _+_ = λ a b → a ℤB.+ b - ; _*_ = λ a b → a ℤB.* b - ; 0# = ℤB.+ 0 - ; 1# = ℤB.+ 1 + ; _+_ = λ a b → a ℤ.+ b + ; _*_ = λ a b → a ℤ.* b + ; 0# = ℤ.+ 0 + ; 1# = ℤ.+ 1 ; isCommutativeSemiring = ℤP.+-*-isCommutativeSemiring } @@ -99,8 +96,8 @@ myN' : CommutativeSemiring _ _ myN' = record { Carrier = ℕ ; _≈_ = _≡_ - ; _+_ = ℕB._+_ - ; _*_ = ℕB._*_ + ; _+_ = ℕ._+_ + ; _*_ = ℕ._*_ ; 0# = 0 ; 1# = 1 ; isCommutativeSemiring = ℕP.+-*-isCommutativeSemiring @@ -122,7 +119,7 @@ makeZ : ℤ → CommutativeSemiring _ _ makeZ _ = ℤP.+-*-commutativeSemiring myZf : CommutativeSemiring _ _ -myZf = makeZ (ℤB.+ 0) +myZf = makeZ (ℤ.+ 0) module FunctionResultZ where open CommutativeSemiring myZf @@ -155,7 +152,7 @@ module DoubleAliasZ where -- 7. Record update on top of an alias. myZUpdated : CommutativeSemiring _ _ -myZUpdated = record myZAlias1 { 0# = ℤB.+ 0 } +myZUpdated = record myZAlias1 { 0# = ℤ.+ 0 } module RecordUpdateOfAliasZ where open CommutativeSemiring myZUpdated @@ -171,8 +168,8 @@ module RecordUpdateOfAliasZ where myZUpdatedη : CommutativeSemiring _ _ myZUpdatedη = record ℤP.+-*-commutativeSemiring - { _+_ = λ a b → a ℤB.+ b - ; _*_ = λ a b → a ℤB.* b + { _+_ = λ a b → a ℤ.+ b + ; _*_ = λ a b → a ℤ.* b } module RecordUpdateηZ where @@ -186,7 +183,7 @@ module RecordUpdateηZ where ------------------------------------------------------------------------ -- 9. Inlined operator body (KNOWN FAILURE). Instead of referring to --- `ℤB._*_`, write its definition `sign i Sign.* sign j ◃ ∣i∣ ℕ.* +-- `ℤ._*_`, 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 @@ -198,11 +195,9 @@ module RecordUpdateηZ where -- The workaround is to give the inlined formula its own top-level -- definition. -open import Data.Sign.Base as Sign using (Sign) - myZInlined : CommutativeSemiring _ _ myZInlined = record ℤP.+-*-commutativeSemiring - { _*_ = λ i j → ℤB.sign i Sign.* ℤB.sign j ℤB.◃ ℤB.∣ i ∣ ℕB.* ℤB.∣ j ∣ + { _*_ = λ i j → ℤ.sign i Sign.* ℤ.sign j ℤ.◃ ℤ.∣ i ∣ ℕ.* ℤ.∣ j ∣ } module InlinedBodyZ where From fa180a56d09446fb8e1e44dad5b5a57cc674e66b Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Fri, 22 May 2026 12:19:20 +0200 Subject: [PATCH 4/5] Tactic.Solver.Ring: handle CommutativeRing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a `CommutativeRing` side to `solve-≈`, alongside the existing `CommutativeSemiring` support. This comes at no extra cost at the call site, and we automatically detect what ring is being used. --- Class/MonadError.agda | 4 + Tactic/Solver/Ring.agda | 168 +++++++++---- Tactic/Solver/Ring/IntegerCoefficients.agda | 226 ++++++++++++++++++ Tactic/Solver/Ring/Tests.agda | 3 +- Tactic/Solver/Ring/Tests/CommutativeRing.agda | 120 ++++++++++ Tactic/Solver/Ring/Tests/Equations.agda | 7 +- 6 files changed, 477 insertions(+), 51 deletions(-) create mode 100644 Tactic/Solver/Ring/IntegerCoefficients.agda create mode 100644 Tactic/Solver/Ring/Tests/CommutativeRing.agda 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/Tactic/Solver/Ring.agda b/Tactic/Solver/Ring.agda index 7e32745..2881234 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring.agda @@ -1,9 +1,12 @@ ------------------------------------------------------------------------ --- A reflection-based ring solver for `CommutativeSemiring`. +-- A reflection-based ring solver. -- --- `solve-≈` instantiates `Algebra.Solver.Ring.NaturalCoefficients.Default R` --- (ℕ coefficients, no negation) by reflecting the user's bundle into --- the polynomial AST and discharging the resulting equation. +-- `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. @@ -12,10 +15,11 @@ module Tactic.Solver.Ring where -open import Algebra using (CommutativeSemiring) +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) @@ -40,6 +44,7 @@ open import Reflection.Utils.Core using (extractNat; pickDefName) open import Reflection.Utils.TCM using (headReduce) open import Tactic.Solver.Algebra +import Tactic.Solver.Ring.IntegerCoefficients as IntC ------------------------------------------------------------------------ -- `Algebra.Solver.Ring.Polynomial`'s `con`, `var`, and `:-_` are @@ -61,6 +66,9 @@ module Solver {c ℓ} (R : CommutativeSemiring c ℓ) where -- 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 `+_`). @@ -83,36 +91,62 @@ private csrZero = quote CommutativeSemiring.0# csrOne = quote CommutativeSemiring.1# - `CommutativeSemiring : Term - `CommutativeSemiring = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) + 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.*`. +-- 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) - `con : (R `n : Term) → Term → Term - `con R `n c = defP R `n (quote Solver.conP) (c ⟨∷⟩ []) + 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 : (R `n : Term) → Term → Term - `var R `n i = defP R `n (quote Solver.varP) (i ⟨∷⟩ []) + `var : RingSide → (R `n : Term) → Term → Term + `var s R `n i = defP R `n (varName s) (i ⟨∷⟩ []) - `:+ : (R `n : Term) → Term → Term → Term - `:+ R `n x y = defP R `n (quote Solver._:+_) (x ⟨∷⟩ y ⟨∷⟩ []) + `:+ : RingSide → (R `n : Term) → Term → Term → Term + `:+ s R `n x y = defP R `n (addName s) (x ⟨∷⟩ y ⟨∷⟩ []) - `:* : (R `n : Term) → Term → Term → Term - `:* R `n x y = defP R `n (quote Solver._:*_) (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 Solver._:=_) (x ⟨∷⟩ y ⟨∷⟩ []) + `:- : (R `n : Term) → Term → Term → Term + `:- R `n x y = defP R `n (quote IntC._:-_) (x ⟨∷⟩ y ⟨∷⟩ []) - `refl : (R : Term) → Term - `refl R = def (quote CommutativeSemiring.refl) (2 ⋯⟅∷⟆ R ⟨∷⟩ 1 ⋯⟅∷⟆ []) + `:-‿ : (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. @@ -145,8 +179,8 @@ private collectDefNames = List.foldr pickDefName [] -- A slot's role. `op` is a generic concrete operator field; - -- `zeroLit` and `oneLit` mark literals. (`derived` exists for - -- structures with non-field operators; CSR has none.) + -- `derived` is additional syntax that isn't a field; `zeroLit` and + -- `oneLit` mark literals. data SlotKind : Set where op zeroLit oneLit derived : SlotKind @@ -177,6 +211,19 @@ private ∷ (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) @@ -195,10 +242,10 @@ private ... | oneLit = go mz (just t) rest ... | _ = go mz mo rest - detectCSR : Term → TC (TheoryDetect × RingState) - detectCSR R = do + detectFor : RingSide → Term → TC (TheoryDetect × RingState) + detectFor side R = do R' ← headReduce 16 R - let slots = csrSlots + 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 @@ -247,67 +294,98 @@ private -- Encoder construction. private - mkEncode : (R↓↓ R↓ : Term) + -- ℕ 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 R↓↓ R↓ numAtoms litStyle = record - { opEncoders = opAdd ∷ opMul ∷ opZero ∷ opOne ∷ [] + mkEncode s R↓↓ R↓ numAtoms litStyle = record + { opEncoders = ops s ; encodeNat = encNat ; sucPeel = sucPeelFn ; encodeVar = encVar - ; encodeEq = `:= R↓↓ `n + ; encodeEq = `:= s R↓↓ `n ; finishSolve = finish } where `n = toTerm numAtoms opAdd : List Term → Term - opAdd (x ∷ y ∷ _) = `:+ R↓↓ `n x y + opAdd (x ∷ y ∷ _) = `:+ s R↓↓ `n x y opAdd _ = unknown opMul : List Term → Term - opMul (x ∷ y ∷ _) = `:* R↓↓ `n x y + 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 R↓↓ `n (toTerm 0) + opZero _ = `con s R↓↓ `n (natLitTerm s 0) opOne : List Term → Term - opOne _ = `con R↓↓ `n (toTerm 1) + 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 R↓↓ `n (toTerm n) + encNat n = `con s R↓↓ `n (natLitTerm s n) sucPeelFn : Term → Term sucPeelFn inner = - `:+ R↓↓ `n (`con R↓↓ `n (toTerm 1)) inner + `:+ s R↓↓ `n (`con s R↓↓ `n (natLitTerm s 1)) inner encVar : ℕ → Term - encVar i = `var R↓↓ `n (toFinTerm i) + encVar i = `var s R↓↓ `n (toFinTerm i) finish : Term → List Term → Term finish lambdaBody atoms = - def (quote Solver.solve) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ `n ⟨∷⟩ lambdaBody ⟨∷⟩ `refl R↓ ⟨∷⟩ List.map vArg atoms) + def (solveName s) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ `n ⟨∷⟩ lambdaBody ⟨∷⟩ `refl s R↓ ⟨∷⟩ List.map vArg atoms) ------------------------------------------------------------------------ -- The macro. private - csrTheory : Theory - csrTheory = record - { bundleType = `CommutativeSemiring + ringTheory : RingSide → Theory + ringTheory s = record + { bundleType = bundleTypeOf s ; State = RingState - ; detect = detectCSR - ; encode = λ R↓↓ R↓ n st → mkEncode R↓↓ R↓ n (RingState.litStyle st) + ; 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 `checkType`'s metavariable resolutions + -- `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`. - R' ← checkType R `CommutativeSemiring + side , R' ← detectSide R commitTC - solveByTheory csrTheory R' hole + solveByTheory (ringTheory side) R' hole macro solve-≈ : Term → Term → TC ⊤ 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 index 20444bf..6cecdef 100644 --- a/Tactic/Solver/Ring/Tests.agda +++ b/Tactic/Solver/Ring/Tests.agda @@ -1,5 +1,6 @@ module Tactic.Solver.Ring.Tests where -open import Tactic.Solver.Ring.Tests.Equations 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/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/Equations.agda b/Tactic/Solver/Ring/Tests/Equations.agda index ab69b34..246d249 100644 --- a/Tactic/Solver/Ring/Tests/Equations.agda +++ b/Tactic/Solver/Ring/Tests/Equations.agda @@ -10,11 +10,8 @@ open import Tactic.Solver.Ring using (solve-≈ ; module Solver) ------------------------------------------------------------------------ -- Limitations -- --- 1. `solve-≈` currently only speaks the language of semirings, so --- there's no negation. --- --- 2. `solve-≈` is not going to help solving any metavariables. When --- it is applied in any context where at least one side of the goal +-- `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 From 9035c0e00c23a9a7756d7782af7372e6b7c8b66e Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Fri, 22 May 2026 13:03:15 +0200 Subject: [PATCH 5/5] Fix one more edge case I dislike this fix, but I can't think of anything better right now --- Reflection/Utils/TCM.agda | 17 +++++++++++++++++ Tactic/Solver/Ring.agda | 7 ++++--- Tactic/Solver/Ring/Tests/Equations.agda | 7 +++++++ 3 files changed, 28 insertions(+), 3 deletions(-) diff --git a/Reflection/Utils/TCM.agda b/Reflection/Utils/TCM.agda index 6d64989..b50162e 100644 --- a/Reflection/Utils/TCM.agda +++ b/Reflection/Utils/TCM.agda @@ -54,3 +54,20 @@ mutual 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/Solver/Ring.agda b/Tactic/Solver/Ring.agda index 2881234..b4abe59 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring.agda @@ -41,7 +41,7 @@ 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) +open import Reflection.Utils.TCM using (headReduce; headReducePeel) open import Tactic.Solver.Algebra import Tactic.Solver.Ring.IntegerCoefficients as IntC @@ -250,10 +250,11 @@ private 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 ⦄ (headReduce 16) rawOps + 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 slotted) + let ls = maybe (uncurry detectLitStyle) nothing (findZeroOne slottedLit) pure ( record { operatorMatches = List.map (λ (s , t) → opMatch t (slotArity s)) slotted diff --git a/Tactic/Solver/Ring/Tests/Equations.agda b/Tactic/Solver/Ring/Tests/Equations.agda index 246d249..2bb0a27 100644 --- a/Tactic/Solver/Ring/Tests/Equations.agda +++ b/Tactic/Solver/Ring/Tests/Equations.agda @@ -34,6 +34,13 @@ module ReadableErrorMessages {c ℓ} (R : CommutativeSemiring c ℓ) where -- 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)