------------------------------------------------------------------------
-- The Agda standard library
--
-- An implementation of the ring solver that requires you to manually
-- pass the equation you wish to solve.
------------------------------------------------------------------------
-- You'll probably want to use `Tactic.RingSolver` instead which uses
-- reflection to automatically extract the equation.
{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.AlmostCommutativeRing
module Tactic.RingSolver.NonReflective
{ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
(let open AlmostCommutativeRing ring)
where
open import Algebra.Morphism
open import Function.Base using (id; _⟨_⟩_)
open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
open import Data.Maybe.Base
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
open import Data.Vec.Base using (Vec)
open import Data.Vec.N-ary
open import Tactic.RingSolver.Core.Polynomial.Parameters
open import Tactic.RingSolver.Core.Expression public
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring
module Ops where
zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
zero-homo x _ with just p ← 0≟ x = p
homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
homo = record
{ from = record
{ rawRing = AlmostCommutativeRing.rawRing ring
; isZero = λ x → is-just (0≟ x)
}
; to = record
{ isAlmostCommutativeRing = record
{ isCommutativeSemiring = isCommutativeSemiring
; -‿cong = -‿cong
; -‿*-distribˡ = -‿*-distribˡ
; -‿+-comm = -‿+-comm
}
}
; morphism = -raw-almostCommutative⟶ ring
; Zero-C⟶Zero-R = zero-homo
}
open Eval rawRing id public
open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
norm : ∀ {n} → Expr Carrier n → Poly n
norm (Κ x) = κ x
norm (Ι x) = ι x
norm (x ⊕ y) = norm x ⊞ norm y
norm (x ⊗ y) = norm x ⊠ norm y
norm (⊝ x) = ⊟ norm x
norm (x ⊛ i) = norm x ⊡ i
⟦_⇓⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
⟦ expr ⇓⟧ = ⟦ norm expr ⟧ₚ where
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
renaming (⟦_⟧ to ⟦_⟧ₚ)
correct : ∀ {n} (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
correct {n = n} = go
where
open import Tactic.RingSolver.Core.Polynomial.Homomorphism homo
go : ∀ (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
go (Κ x) ρ = κ-hom x ρ
go (Ι x) ρ = ι-hom x ρ
go (x ⊕ y) ρ = ⊞-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ +-cong ⟩ go y ρ)
go (x ⊗ y) ρ = ⊠-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ *-cong ⟩ go y ρ)
go (⊝ x) ρ = ⊟-hom (norm x) ρ ⟨ trans ⟩ -‿cong (go x ρ)
go (x ⊛ i) ρ = ⊡-hom (norm x) i ρ ⟨ trans ⟩ ^-congˡ i (go x ρ)
open import Relation.Binary.Reflection setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public
solve : ∀ (n : ℕ) →
(f : N-ary n (Expr Carrier n) (Expr Carrier n × Expr Carrier n)) →
Eqʰ n _≈_ (curryⁿ (Ops.⟦_⇓⟧ (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⇓⟧ (proj₂ (Ops.close n f)))) →
Eq n _≈_ (curryⁿ (Ops.⟦_⟧ (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⟧ (proj₂ (Ops.close n f))))
solve = Ops.solve
{-# INLINE solve #-}
infixl 6 _⊜_
_⊜_ : ∀ {n : ℕ} →
Expr Carrier n →
Expr Carrier n →
Expr Carrier n × Expr Carrier n
_⊜_ = _,_
{-# INLINE _⊜_ #-}
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