------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver that uses reflection to automatically obtain and solve
-- equations over rings.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Tactic.RingSolver where
open import Algebra
open import Data.Fin.Base as Fin using (Fin)
open import Data.Vec.Base as Vec using (Vec; _∷_; [])
open import Data.List.Base as List using (List; _∷_; [])
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; fromMaybe)
open import Data.Nat.Base using (ℕ; suc; zero; _<ᵇ_)
open import Data.Bool.Base using (Bool; if_then_else_; true; false)
open import Data.Unit.Base using (⊤)
open import Data.String.Base as String using (String; _++_; parens)
open import Data.Product.Base using (_,_; proj₁)
open import Function.Base
open import Reflection
open import Reflection.AST.Argument
open import Reflection.AST.Term as Term
open import Reflection.AST.AlphaEquality
open import Reflection.AST.Name as Name
open import Reflection.TCM.Syntax
open import Data.Nat.Reflection
open import Data.List.Reflection
import Data.Vec.Reflection as Vec
open import Tactic.RingSolver.NonReflective renaming (solve to solver)
open import Tactic.RingSolver.Core.AlmostCommutativeRing
open import Tactic.RingSolver.Core.NatSet as NatSet
open AlmostCommutativeRing
------------------------------------------------------------------------
-- Utilities
private
VarMap : Set
VarMap = ℕ → Maybe Term
getVisible : Arg Term → Maybe Term
getVisible (arg (arg-info visible _) x) = just x
getVisible _ = 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
curriedTerm : NatSet → Term
curriedTerm = List.foldr go Vec.`[] ∘ NatSet.toList
where
go : ℕ → Term → Term
go x xs = var x [] Vec.`∷ xs
------------------------------------------------------------------------
-- Reflection utilities for rings
`AlmostCommutativeRing : Term
`AlmostCommutativeRing = def (quote AlmostCommutativeRing) (2 ⋯⟨∷⟩ [])
record RingOperatorTerms : Set where
constructor add⇒_mul⇒_pow⇒_neg⇒_sub⇒_
field
add mul pow neg sub : Term
checkIsRing : Term → TC Term
checkIsRing ring = checkType ring `AlmostCommutativeRing
module RingReflection (`ring : Term) where
-- Takes the name of a function that takes the ring as it's first
-- explicit argument and the terms of it's arguments and inserts
-- the required ring arguments
-- e.g. "_+_" $ʳ xs = "_+_ {_} {_} ring xs"
infixr 6 _$ʳ_
_$ʳ_ : Name → Args Term → Term
nm $ʳ args = def nm (2 ⋯⟅∷⟆ `ring ⟨∷⟩ args)
`Carrier : Term
`Carrier = quote Carrier $ʳ []
`refl : Term
`refl = quote refl $ʳ (1 ⋯⟅∷⟆ [])
`sym : Term → Term
`sym x≈y = quote sym $ʳ (2 ⋯⟅∷⟆ x≈y ⟨∷⟩ [])
`trans : Term → Term → Term
`trans x≈y y≈z = quote trans $ʳ (3 ⋯⟅∷⟆ x≈y ⟨∷⟩ y≈z ⟨∷⟩ [])
-- Normalises each of the fields of the ring operator so we can
-- compare the result against the normalised definitions we come
-- across when converting the term passed to the macro.
getRingOperatorTerms : TC RingOperatorTerms
getRingOperatorTerms = ⦇
add⇒ normalise (quote _+_ $ʳ [])
mul⇒ normalise (quote _*_ $ʳ [])
pow⇒ normalise (quote _^_ $ʳ [])
neg⇒ normalise (quote (-_) $ʳ [])
sub⇒ normalise (quote _-_ $ʳ [])
⦈
------------------------------------------------------------------------
-- Reflection utilities for ring solver
module RingSolverReflection (ring : Term) (numberOfVariables : ℕ) where
open RingReflection ring
`numberOfVariables : Term
`numberOfVariables = toTerm numberOfVariables
-- This function applies the hidden arguments that the constructors
-- that Expr needs. The first is the universe level, the second is the
-- type it contains, and the third is the number of variables it's
-- indexed by. All three of these could likely be inferred, but to
-- make things easier we supply the third because we know it.
infix -1 _$ᵉ_
_$ᵉ_ : Name → List (Arg Term) → Term
e $ᵉ xs = con e (1 ⋯⟅∷⟆ `Carrier ⟅∷⟆ `numberOfVariables ⟅∷⟆ xs)
-- A constant expression.
`Κ : Term → Term
`Κ x = quote Κ $ᵉ (x ⟨∷⟩ [])
`I : Term → Term
`I x = quote Ι $ᵉ (x ⟨∷⟩ [])
infixl 6 _`⊜_
_`⊜_ : Term → Term → Term
x `⊜ y = quote _⊜_ $ʳ (`numberOfVariables ⟅∷⟆ x ⟨∷⟩ y ⟨∷⟩ [])
`correct : Term → Term → Term
`correct x ρ = quote Ops.correct $ʳ (1 ⋯⟅∷⟆ x ⟨∷⟩ ρ ⟨∷⟩ [])
`solver : Term → Term → Term
`solver `f `eq = quote solver $ʳ (`numberOfVariables ⟨∷⟩ `f ⟨∷⟩ `eq ⟨∷⟩ [])
-- Converts the raw terms provided by the macro into the `Expr`s
-- used internally by the solver.
--
-- When trying to figure out the shape of an expression, one of
-- the difficult tasks is recognizing where constants in the
-- underlying ring are used. If we were only dealing with ℕ, we
-- might look for its constructors: however, we want to deal with
-- arbitrary types which implement AlmostCommutativeRing. If the
-- Term type contained type information we might be able to
-- recognize it there, but it doesn't.
--
-- We're in luck, though, because all other cases in the following
-- function *are* recognizable. As a result, the "catch-all" case
-- will just assume that it has a constant expression.
convertTerm : RingOperatorTerms → VarMap → Term → TC Term
convertTerm operatorTerms varMap = convert
where
open RingOperatorTerms operatorTerms
mutual
convert : Term → TC Term
-- First try and match directly against the fields
convert (def (quote _+_) xs) = convertOp₂ (quote _⊕_) xs
convert (def (quote _*_) xs) = convertOp₂ (quote _⊗_) xs
convert (def (quote -_) xs) = convertOp₁ (quote ⊝_) xs
convert (def (quote _^_) xs) = convertExp xs
convert (def (quote _-_) xs) = convertSub xs
-- Other definitions the underlying implementation of the ring's fields
convert (def nm xs) = convertUnknownName nm xs
-- Variables
convert v@(var x _) = pure $ fromMaybe (`Κ v) (varMap x)
-- Special case to recognise "suc" for naturals
convert (`suc x) = convertSuc x
-- Otherwise we're forced to treat it as a constant
convert t = pure $ `Κ t
-- Application of a ring operator often doesn't have a type as
-- simple as "Carrier → Carrier → Carrier": there may be hidden
-- arguments, etc. Here, we do our best to handle those cases,
-- by just taking the last two explicit arguments.
convertOp₂ : Name → Args Term → TC Term
convertOp₂ nm (x ⟨∷⟩ y ⟨∷⟩ []) = do
x' ← convert x
y' ← convert y
pure (nm $ᵉ (x' ⟨∷⟩ y' ⟨∷⟩ []))
convertOp₂ nm (x ∷ xs) = convertOp₂ nm xs
convertOp₂ _ _ = pure unknown
convertOp₁ : Name → Args Term → TC Term
convertOp₁ nm (x ⟨∷⟩ []) = do
x' ← convert x
pure (nm $ᵉ (x' ⟨∷⟩ []))
convertOp₁ nm (x ∷ xs) = convertOp₁ nm xs
convertOp₁ _ _ = pure unknown
convertExp : Args Term → TC Term
convertExp (x ⟨∷⟩ y ⟨∷⟩ []) = do
x' ← convert x
pure (quote _⊛_ $ᵉ (x' ⟨∷⟩ y ⟨∷⟩ []))
convertExp (x ∷ xs) = convertExp xs
convertExp _ = pure unknown
convertSub : Args Term → TC Term
convertSub (x ⟨∷⟩ y ⟨∷⟩ []) = do
x' ← convert x
-y' ← convertOp₁ (quote (⊝_)) (y ⟨∷⟩ [])
pure (quote _⊕_ $ᵉ x' ⟨∷⟩ -y' ⟨∷⟩ [])
convertSub (x ∷ xs) = convertSub xs
convertSub _ = pure unknown
convertUnknownName : Name → Args Term → TC Term
convertUnknownName nm xs = do
nameTerm ← normalise (def nm [])
if (nameTerm =α= add) then convertOp₂ (quote _⊕_) xs else
if (nameTerm =α= mul) then convertOp₂ (quote _⊗_) xs else
if (nameTerm =α= neg) then convertOp₁ (quote ⊝_) xs else
if (nameTerm =α= pow) then convertExp xs else
if (nameTerm =α= sub) then convertSub xs else
pure (`Κ (def nm xs))
convertSuc : Term → TC Term
convertSuc x = do x' ← convert x; pure (quote _⊕_ $ᵉ (`Κ (toTerm 1) ⟨∷⟩ x' ⟨∷⟩ []))
------------------------------------------------------------------------
-- Macros
------------------------------------------------------------------------
-- Quantified macro
open RingReflection
open RingSolverReflection
malformedForallTypeError : ∀ {a} {A : Set a} → Term → TC A
malformedForallTypeError found = typeError
( strErr "Malformed call to solve."
∷ strErr "Expected target type to be like: ∀ x y → x + y ≈ y + x."
∷ strErr "Instead: "
∷ termErr found
∷ [])
quantifiedVarMap : ℕ → VarMap
quantifiedVarMap numVars i =
if i <ᵇ numVars
then just (var i [])
else nothing
constructCallToSolver : Term → RingOperatorTerms → List String → Term → Term → TC Term
constructCallToSolver `ring opNames variables `lhs `rhs = do
`lhsExpr ← conv `lhs
`rhsExpr ← conv `rhs
pure $ `solver `ring numVars
(prependVLams variables (_`⊜_ `ring numVars `lhsExpr `rhsExpr))
(prependHLams variables (`refl `ring))
where
numVars : ℕ
numVars = List.length variables
conv : Term → TC Term
conv = convertTerm `ring numVars opNames (quantifiedVarMap numVars)
-- This is the main macro which solves for equations in which the
-- variables are universally quantified over:
--
-- lemma : ∀ x y → x + y ≈ y + x
-- lemma = solve-∀ ring
--
-- where ring is your implementation of AlmostCommutativeRing.
-- (Find some example implementations in
-- Polynomial.Solver.Ring.AlmostCommutativeRing.Instances).
solve-∀-macro : Name → Term → TC ⊤
solve-∀-macro ring hole = do
`ring ← checkIsRing (def ring [])
commitTC
operatorTerms ← getRingOperatorTerms `ring
-- Obtain and sanitise the goal type
`hole ← inferType hole >>= reduce
let variablesAndTypes , equation = stripPis `hole
let variables = List.map proj₁ variablesAndTypes
just (lhs ∷ rhs ∷ []) ← pure (getVisibleArgs 2 equation)
where nothing → malformedForallTypeError `hole
solverCall ← constructCallToSolver `ring operatorTerms variables lhs rhs
unify hole solverCall
macro
solve-∀ : Name → Term → TC ⊤
solve-∀ = solve-∀-macro
------------------------------------------------------------------------
-- Unquantified macro
malformedArgumentListError : ∀ {a} {A : Set a} → Term → TC A
malformedArgumentListError found = typeError
( strErr "Malformed call to solve."
∷ strErr "First argument should be a list of free variables."
∷ strErr "Instead: "
∷ termErr found
∷ [])
malformedGoalError : ∀ {a} {A : Set a} → Term → TC A
malformedGoalError found = typeError
( strErr "Malformed call to solve."
∷ strErr "Goal type should be of the form: LHS ≈ RHS"
∷ strErr "Instead: "
∷ termErr found
∷ [])
checkIsListOfVariables : Term → Term → TC Term
checkIsListOfVariables `ring `xs = checkType `xs (`List (`Carrier `ring)) >>= normalise
-- Extracts the deBruijn indices from a list of variables
getVariableIndices : Term → Maybe NatSet
getVariableIndices = go []
where
go : NatSet → Term → Maybe NatSet
go t (var i [] `∷` xs) = go (insert i t) xs
go t `[]` = just t
go _ _ = nothing
constructSolution : Term → RingOperatorTerms → NatSet → Term → Term → TC Term
constructSolution `ring opTerms variables `lhs `rhs = do
`lhsExpr ← conv `lhs
`rhsExpr ← conv `rhs
pure $ `trans `ring (`sym `ring `lhsExpr) `rhsExpr
where
numVars = List.length variables
varMap : VarMap
varMap i = Maybe.map (λ x → `I `ring numVars (toFinTerm x)) (lookup variables i)
ρ : Term
ρ = curriedTerm variables
conv = λ t → do
t' ← convertTerm `ring numVars opTerms varMap t
pure $ `correct `ring numVars t' ρ
-- Use this macro when you want to solve something *under* a lambda.
-- For example: say you have a long proof, and you just want the solver
-- to deal with an intermediate step. Call it like so:
--
-- lemma₃ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
-- lemma₃ x y = begin
-- x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩
-- y * 1 + x + 3 ≈⟨ solve (x ∷ y ∷ []) Int.ring ⟩
-- 3 + y + x ≡⟨ refl ⟩
-- 2 + 1 + y + x ∎
--
-- The first argument is the free variables, and the second is the
-- ring implementation (as before).
solve-macro : Term → Name → Term → TC ⊤
solve-macro variables ring hole = do
`ring ← checkIsRing (def ring [])
commitTC
operatorTerms ← getRingOperatorTerms `ring
-- Obtain and sanitise the list of variables
listOfVariables′ ← checkIsListOfVariables `ring variables
commitTC
just variableIndices ← pure (getVariableIndices listOfVariables′)
where nothing → malformedArgumentListError listOfVariables′
-- Obtain and santise the goal type
hole′ ← inferType hole >>= reduce
just (lhs ∷ rhs ∷ []) ← pure (getVisibleArgs 2 hole′)
where nothing → malformedGoalError hole′
solution ← constructSolution `ring operatorTerms variableIndices lhs rhs
unify hole solution
macro
solve : Term → Name → Term → TC ⊤
solve = solve-macro
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4