-- ------------------------------------------------------------------------------------------------------
-- | ███████╗ ██████╗ ██╗ ██╗ ██╗██╗███╗ ██╗ ██████╗ ██████╗ ██╗███╗ ██╗ ██████╗ ███████╗ |
-- | ██╔════╝██╔═══██╗██║ ██║ ██║██║████╗ ██║██╔════╝ ██╔══██╗██║████╗ ██║██╔════╝ ██╔════╝ |
-- | ███████╗██║ ██║██║ ██║ ██║██║██╔██╗ ██║██║ ███╗ ██████╔╝██║██╔██╗ ██║██║ ███╗███████╗ |
-- | ╚════██║██║ ██║██║ ╚██╗ ██╔╝██║██║╚██╗██║██║ ██║ ██╔══██╗██║██║╚██╗██║██║ ██║╚════██║ |
-- | ███████║╚██████╔╝███████╗ ╚████╔╝ ██║██║ ╚████║╚██████╔╝ ██║ ██║██║██║ ╚████║╚██████╔╝███████║ |
-- | ╚══════╝ ╚═════╝ ╚══════╝ ╚═══╝ ╚═╝╚═╝ ╚═══╝ ╚═════╝ ╚═╝ ╚═╝╚═╝╚═╝ ╚═══╝ ╚═════╝ ╚══════╝ |
-- | |
-- | ██╗███╗ ██╗ █████╗ ██████╗ ██████╗ █████╗ |
-- | ██║████╗ ██║ ██╔══██╗██╔════╝ ██╔══██╗██╔══██╗ |
-- | ██║██╔██╗ ██║ ███████║██║ ███╗██║ ██║███████║ |
-- | ██║██║╚██╗██║ ██╔══██║██║ ██║██║ ██║██╔══██║ |
-- | ██║██║ ╚████║ ██║ ██║╚██████╔╝██████╔╝██║ ██║ |
-- | ╚═╝╚═╝ ╚═══╝ ╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝ |
-- ------------------------------------------------------------------------------------------------------
--
-- Donnacha Oisín Kidney
-- 17 April 2019
--
-- Compiled with Agda version 2.6.1, and standard library commit 84d7962cfd90379a6d1d5ef2cdd9d3ae411ee603
-- This contains the worked-through source code for:
--
-- "Automatically And Efficiently Illustrating Polynomial Equalities in Agda"
--
-- We present a new library which automates the construction of equivalence
-- proofs between polynomials over commutative rings and semirings in the
-- programming language Agda. It is asymptotically faster than Agda's existing
-- solver. We use Agda's reflection machinery to provide a simple interface to
-- the solver, and demonstrate an interesting use of the constructed relations:
-- step-by-step solutions.
--
-- Which is (at time of writing) a work-in-progress.
--
-- This code is available on github:
-- https://github.com/oisdk/agda-ring-solver
--
-- As is the paper:
-- https://github.com/oisdk/agda-ring-solver-report
module README where
--------------------------------------------------------------------------------
-- There are 3 main contributions in this library: --
-- --
-- * A solver for polynomials over "almost commutative rings". --
-- Agda already has one these in the standard library, but this one --
-- is much more efficient. "Almost commutative rings" encapsulates a --
-- bunch of things, including ℕ. --
-- --
-- * A reflection-based interface. --
-- Not many people used the old solver, mainly (I think) because the --
-- interface was difficult and irritating. This library provides a --
-- super-simple interface using reflection. --
-- --
-- * An implementation of "step-by-step solutions". --
-- I don't know a huge amount about computer algebra systems, but I --
-- have used Wolfram Alpha countless times (especially when I was in --
-- school) to help with basic maths. I was able to get this solver to --
-- produce step-by-step solutions, and learned something about the --
-- theory behind them along the way. --
--------------------------------------------------------------------------------
--
-- ██████╗ ███████╗███╗ ██╗ ██████╗██╗ ██╗███╗ ███╗ █████╗ ██████╗ ██╗ ██╗███████╗
-- ██╔══██╗██╔════╝████╗ ██║██╔════╝██║ ██║████╗ ████║██╔══██╗██╔══██╗██║ ██╔╝██╔════╝
-- ██████╔╝█████╗ ██╔██╗ ██║██║ ███████║██╔████╔██║███████║██████╔╝█████╔╝ ███████╗ ███████╗
-- ██╔══██╗██╔══╝ ██║╚██╗██║██║ ██╔══██║██║╚██╔╝██║██╔══██║██╔══██╗██╔═██╗ ╚════██║ ╚════██║
-- ██████╔╝███████╗██║ ╚████║╚██████╗██║ ██║██║ ╚═╝ ██║██║ ██║██║ ██║██║ ██╗███████║ ██║
-- ╚═════╝ ╚══════╝╚═╝ ╚═══╝ ╚═════╝╚═╝ ╚═╝╚═╝ ╚═╝╚═╝ ╚═╝╚═╝ ╚═╝╚═╝ ╚═╝╚══════╝ ██║
-- ██║
-- ███████╗██╗ ██╗ █████╗ ███╗ ███╗██████╗ ██╗ ███████╗███████╗ ██║
-- ██╔════╝╚██╗██╔╝██╔══██╗████╗ ████║██╔══██╗██║ ██╔════╝██╔════╝ ██║
-- █████╗ ╚███╔╝ ███████║██╔████╔██║██████╔╝██║ █████╗ ███████╗ ████████████████████╗ ██║
-- ██╔══╝ ██╔██╗ ██╔══██║██║╚██╔╝██║██╔═══╝ ██║ ██╔══╝ ╚════██║ ╚═════════════════██║ ██║
-- ███████╗██╔╝ ██╗██║ ██║██║ ╚═╝ ██║██║ ███████╗███████╗███████║ ██║ ██║
-- ╚══════╝╚═╝ ╚═╝╚═╝ ╚═╝╚═╝ ╚═╝╚═╝ ╚══════╝╚══════╝╚══════╝ ██║ ██║
-- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- You can ignore this bit! We're just overloading the literals Agda uses for -- ██║ ██║
-- numbers This bit isn't necessary if you're just using Nats, or if you -- ██║ ██║
-- construct your type directly. We only really do it here so that we can use -- ██║ ██║
-- different numeric types in the same file. -- ██║ ██║
-- ██║ ██║
open import Agda.Builtin.FromNat -- ██║ ██║
open import Data.Nat using (ℕ) -- ██║ ██║
open import Data.Integer using (ℤ) -- ██║ ██║
-- ██║ ██║
instance -- ██║ ██║
numberNat : Number ℕ -- ██║ ██║
numberNat = Data.Nat.Literals.number -- ██║ ██║
where import Data.Nat.Literals -- ██║ ██║
-- ██║ ██║
instance -- ██║ ██║
numberInt : Number ℤ -- ██║ ██║
numberInt = Data.Integer.Literals.number -- ██║ ██║
where import Data.Integer.Literals -- ██║ ██║
-- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- Imports! -- ██║ ██║
-- ██║ ██║
open import Polynomial.Simple.AlmostCommutativeRing -- ██║ ██║
open import Polynomial.Simple.AlmostCommutativeRing.Instances -- ██║ ██║
open import Polynomial.Simple.Reflection -- ██║ ██║
open import Data.List as List using (List; _∷_; []) -- ██║ ██║
open import Function -- ██║ ██║
open import Relation.Binary.PropositionalEquality as ≡ using (subst; _≡_) -- ██║ ██║
open import Data.Bool as Bool using (Bool; true; false; if_then_else_) -- ██║ ██║
open import Data.Unit using (⊤; tt) -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
-- 8888888888',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888' -- ██║ ██║
-- ,8',8888888888888 -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
module IntExamples where -- ██║ ██║
open AlmostCommutativeRing Int.ring -- ██║ ██║
-- Everything is automatic: you just ask Agda to solve it and it does! -- ██╗ ██║ ██║
lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1 -- ████║ ██║ ██║
lemma₁ = solve Int.ring -- ██████████║ ██║
-- ████╔═██║ ██║
lemma₂ : ∀ x y → (x + y) ^ 2 ≈ x ^ 2 + 2 * x * y + y ^ 2 -- ██║ ██║ ██║
lemma₂ = solve Int.ring -- ╚═╝ ██║ ██║
-- ██║ ██║
open import Relation.Binary.Reasoning.Inference setoid -- ██║ ██║
-- ██║ ██║
-- It can interact with manual proofs as well. -- ██║ ██║
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 ≈⟨ solveOver (x ∷ y ∷ []) Int.ring ⟩ -- ██║ ██║
3 + y + x ≡⟨⟩ -- ██║ ██║
2 + 1 + y + x ∎ -- ██║ ██║
-- ██║ ██║
open Int.Reflection -- ██║ ██║
-- ██║ ██║
-- There's a shorthand included for Int and Nat. -- ██║ ██║
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 ≈⟨ ∀⟨ x ∷ y ∷ [] ⟩ ⟩ -- ██║ ██║
3 + y + x ≡⟨⟩ -- ██║ ██║
2 + 1 + y + x ∎ -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
-- b. 8 -- ██║ ██║
-- 888o. 8 -- ██║ ██║
-- Y88888o. 8 -- ██║ ██║
-- .`Y888888o. 8 -- ██║ ██║
-- 8o. `Y888888o. 8 -- ██║ ██║
-- 8`Y8o. `Y88888o8 -- ██║ ██║
-- 8 `Y8o. `Y8888 -- ██║ ██║
-- 8 `Y8o. `Y8 -- ██║ ██║
-- 8 `Y8o.` -- ██║ ██║
-- 8 `Yo -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
module NatExamples where -- ██║ ██║
open AlmostCommutativeRing Nat.ring -- ██╗ ██║ ██║
-- The solver is flexible enough to work with Nats (even though it asks -- ████║ ██║ ██║
-- for rings!) -- ██████████║ ██║
lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x -- ████╔═██║ ██║
lemma₁ = solve Nat.ring -- ██║ ██║ ██║
-- -- ╚═╝ ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
-- ##### # # ####### ##### # # ### # # ##### -- ██║ ██║
-- # # # # # # # # # # ## # # # -- ██║ ██║
-- # # # # # # # # # # # # -- ██║ ██║
-- # ####### ##### # ### # # # # # #### -- ██║ ██║
-- # # # # # # # # # # # # # -- ██║ ██║
-- # # # # # # # # # # # ## # # -- ██║ ██║
-- ##### # # ####### ##### # # ### # # ##### -- ██║ ██║
-- -- ██║ ██║
-- ### # # # # # ###### ### # # # ####### ##### -- ██║ ██║
-- # ## # # # # # # # # # # ## # # # # -- ██║ ██║
-- # # # # # # # # # # # # # # # # # # -- ██║ ██║
-- # # # # # # # # ###### # # # # # # # ##### -- ██║ ██║
-- # # # # # # ####### # # # ####### # # # # # -- ██║ ██║
-- # # ## # # # # # # # # # # ## # # # -- ██║ ██║
-- ### # # # # # # # ### # # # # # ##### -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- The solver makes it easy to prove invariants, without having to rewrite -- ██║ ██║
-- proof code every time something changes in the data structure. -- ██║ ██║
-- -- ██║ ██║
module _ {a} {A : Set a} (_≤_ : A → A → Bool) where -- ██║ ██║
-- A Skew Heap, indexed by its size. -- ██║ ██║
data Tree : ℕ → Set a where -- ██║ ██║
leaf : Tree 0 -- ██║ ██║
node : ∀ {n m} → A → Tree n → Tree m → Tree (n + m + 1) -- ██║ ██║
-- ██║ ██║
-- A substitution operator, to clean things up. -- ██║ ██║
_⇒_ : ∀ {n} → Tree n → ∀ {m} → n ≈ m → Tree m -- ██║ ██║
x ⇒ n≈m = subst Tree n≈m x -- ██║ ██║
-- ██║ ██║
open Nat.Reflection -- ██║ ██║
-- ██║ ██║
-- _∪_ : ∀ {n m} → Tree n → Tree m → Tree (n + m) -- ██║ ██║
-- leaf ∪ ys = ys -- ██║ ██║
-- node {a} {b} x xl xr ∪ leaf = -- ██║ ██║
-- node x xl xr ⇒ ∀⟨ a ∷ b ∷ [] ⟩ -- ██╗ ██║ ██║
-- node {a} {b} x xl xr ∪ node {c} {d} y yl yr = if x ≤ y -- ████║ ██║ ██║
-- then node x (node y yl yr ∪ xr) xl -- ██████████║ ██║
-- ⇒ ∀⟨ a ∷ b ∷ c ∷ d ∷ [] ⟩ -- ████╔═██║ ██║
-- else (node y (node x xl xr ∪ yr) yl -- ██║ ██║ ██║
-- ⇒ ∀⟨ a ∷ b ∷ c ∷ d ∷ [] ⟩) -- ╚═╝ ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- -- ██║ ██║
-- 8888888 8888888888 8 8888 8 8 8888888888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 888888888888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888888888888 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 8888 -- ██║ ██║
-- 8 8888 8 8888 8 8 888888888888 -- ██║ ██║
-- -- ██║ ██║
-- ,o888888o. 8 8888 8 888888888o. -- ██║ ██║
-- . 8888 `88. 8 8888 8 8888 `^888. -- ██║ ██║
-- ,8 8888 `8b 8 8888 8 8888 `88. -- ██║ ██║
-- 88 8888 `8b 8 8888 8 8888 `88 -- ██║ ██║
-- 88 8888 88 8 8888 8 8888 88 -- ██║ ██║
-- 88 8888 88 8 8888 8 8888 88 -- ██║ ██║
-- 88 8888 ,8P 8 8888 8 8888 ,88 -- ██║ ██║
-- `8 8888 ,8P 8 8888 8 8888 ,88' -- ██║ ██║
-- ` 8888 ,88' 8 8888 8 8888 ,o88P' -- ██║ ██║
-- `8888888P' 8 888888888888 8 888888888P' -- ██║ ██║
-- -- ██║ ██║
-- `8.`888b ,8' .8. `8.`8888. ,8' -- ██║ ██║
-- `8.`888b ,8' .888. `8.`8888. ,8' -- ██║ ██║
-- `8.`888b ,8' :88888. `8.`8888. ,8' -- ██║ ██║
-- `8.`888b .b ,8' . `88888. `8.`8888.,8' -- ██║ ██║
-- `8.`888b 88b ,8' .8. `88888. `8.`88888' -- ██║ ██║
-- `8.`888b .`888b,8' .8`8. `88888. `8. 8888 -- ██║ ██║
-- `8.`888b8.`8888' .8' `8. `88888. `8 8888 -- ██║ ██║
-- `8.`888`8.`88' .8' `8. `88888. 8 8888 -- ██║ ██║
-- `8.`8' `8,`' .888888888. `88888. 8 8888 -- ██║ ██║
-- `8.` `8' .8' `8. `88888. 8 8888 -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- Previously, you had to construct the expression you wanted to solve twice: -- ██║ ██║
-- once in the type signature, and again using the special solver syntax. -- ██║ ██║
-- -- ██║ ██║
-- This is difficult to learn, and error-prone: if I change an x + y -- ██║ ██║
-- somewhere to a y + x, I *also* have to change the proofs now! The -- ██║ ██║
-- reflection-based solver will automatically construct the new proof. -- ██║ ██║
-- -- ██║ ██║
module OldSolver where -- ██║ ██║
open import Data.Nat -- ██║ ██║
open import Data.Nat.Solver using (module +-*-Solver) -- ██║ ██║
open +-*-Solver -- ██║ ██║
-- ██╗ ██║ ██║
--lemma : ∀ x y → x + y * 1 + 3 ≡ 2 + 1 + y + x -- ████║ ██║ ██║
--lemma = +-*-Solver.solve 2 -- ██████████║ ██║
-- (λ x y → x :+ y :* con 1 :+ con 3 := con 2 :+ con 1 :+ y :+ x) ≡.refl -- ████╔═██║ ██║
-- -- ██║ ██║ ██║
-------------------------------------------------------------------------------- ╚═╝ ██║ ██║
-- -- ██║ ██║
-- d888888o. 8888888 8888888888 8 8888888888 8 888888888o -- ██║ ██║
-- .`8888:' `88. 8 8888 8 8888 8 8888 `88. -- ██║ ██║
-- 8.`8888. Y8 8 8888 8 8888 8 8888 `88 -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 8888 ,88 -- ██║ ██║
-- `8.`8888. 8 8888 8 888888888888 8 8888. ,88' -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 888888888P' -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 8888 -- ██║ ██║
-- 8b `8.`8888. 8 8888 8 8888 8 8888 -- ██║ ██║
-- `8b. ;8.`8888 8 8888 8 8888 8 8888 -- ██║ ██║
-- `Y8888P ,88P' 8 8888 8 888888888888 8 8888 -- ██║ ██║
-- -- ██║ ██║
-- 8 888888888o `8.`8888. ,8' -- ██║ ██║
-- 8 8888 `88. `8.`8888. ,8' -- ██║ ██║
-- 8 8888 `88 `8.`8888. ,8' -- ██║ ██║
-- 8 8888 ,88 `8.`8888.,8' -- ██║ ██║
-- 8 8888. ,88' `8.`88888' -- ██║ ██║
-- 8 8888888888 `8. 8888 -- ██║ ██║
-- 8 8888 `88. `8 8888 -- ██║ ██║
-- 8 8888 88 8 8888 -- ██║ ██║
-- 8 8888 ,88' 8 8888 -- ██║ ██║
-- 8 888888888P 8 8888 -- ██║ ██║
-- -- ██║ ██║
-- d888888o. 8888888 8888888888 8 8888888888 8 888888888o -- ██║ ██║
-- .`8888:' `88. 8 8888 8 8888 8 8888 `88. -- ██║ ██║
-- 8.`8888. Y8 8 8888 8 8888 8 8888 `88 -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 8888 ,88 -- ██║ ██║
-- `8.`8888. 8 8888 8 888888888888 8 8888. ,88' -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 888888888P' -- ██║ ██║
-- `8.`8888. 8 8888 8 8888 8 8888 -- ██║ ██║
-- 8b `8.`8888. 8 8888 8 8888 8 8888 -- ██║ ██║
-- `8b. ;8.`8888 8 8888 8 8888 8 8888 -- ██║ ██║
-- `Y8888P ,88P' 8 8888 8 888888888888 8 8888 -- ██║ ██║
-- -- ██║ ██║
-------------------------------------------------------------------------------- ██║ ██║
-- Don't understand why something works? Wanna get it explained to you? Now -- ██║ ██║
-- you can! The solver can generate step-by-step, human-readable solutions -- ██║ ██║
-- for learning purposes. -- ██║ ██║
-- -- ██║ ██║
module TracedExamples where -- ██║ ██║
import Data.Nat.Show -- ██║ ██║
open import EqBool -- ██║ ██║
open import Relation.Traced Nat.ring Data.Nat.Show.show public -- ██║ ██║
open AlmostCommutativeRing tracedRing -- ██║ ██║
-- ██║ ██║
lemma : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x -- ██║ ██║
lemma = solve tracedRing -- ██║ ██║
-- ██╗██║ ██║
explained -- ████║██║ ██║
: showProof (lemma "x" "y") ≡ "x + y + 3" -- █████████║ ██║
∷ " ={ +-comm(x, y + 3) }" -- ████╔══╝ ██║
∷ "y + 3 + x" -- ██║ ██║
∷ " ={ +-comm(y, 3) }" -- ╚═╝ ██║
∷ "3 + y + x" -- ██║
∷ [] -- ██║
explained = ≡.refl -- ██║
-------------------------------------------------------------------------------- ██║
-- -- ██║
-- The new solver uses a sparse representation, which is much faster than the -- ██║
-- dense one the old solver used. The following graph shows the time (in -- ██║
-- seconds) to prove that: -- ██║
-- -- ██║
-- (1 + x₁¹ + x₂² + x₃³ + x₄⁴ + x₅⁵)ᵈ -- ██║
-- -- ██║
-- is equal to its expanded form. (to run the benchmarks yourself, run the -- ██║
-- run_benchmarks.py file. You'll need python 3 and sympy.) -- ██║
-- -- ██║
-- 540 | * = old * -- ██║
-- 525 | + = new * -- ██║
-- 510 | * -- ██║
-- 495 | * -- ██║
-- 480 | * -- ██║
-- 465 | * -- ██║
-- 450 | * -- ██║
-- 435 | * -- ██║
-- 420 | * -- ██║
-- 405 | * -- ██║
-- 390 | * -- ██║
-- 375 | * -- ██║
-- 360 | * -- ██║
-- 345 | * -- ██║
-- 330 | * -- ██║
-- 315 | * -- ██║
-- 300 | * -- ██║
-- 285 | * -- ██║
-- 270 | * -- ██║
-- 255 | * -- ██║
-- 240 | * -- ██╗██║
-- 225 | * -- ████║██║
-- 210 | * -- █████████║
-- 195 | * -- ████╔══╝
-- 180 | * -- ██║
-- 165 | * -- ╚═╝
-- 150 | * --
-- 135 | * --
-- 120 | * --
-- 105 | * --
-- 90 | * --
-- 75 | * --
-- 60 | ** --
-- 45 | ** --
-- 30 | ** +++++ --
-- 15 | ***** +++++++++ --
-- 0 | *****************************************+++++++++ --
-- ------------------------------------------------------------------ --
-- d = 1 2 3 4 5 6 7 8 --
--------------------------------------------------------------------------------
--
-- * How does it work? Why is it fast?
-- The solver works by converting expressions to "Horner Normal Form".
-- This representation is special: x + y is represented in the same way
-- as y + x. This is what lets us check that two expressions are equal.
-- The implementation here is *sparse*, also, which is why it's faster
-- than the old implementation.
--
-- Want to learn more? Then this is the place for you:
import Polynomial.NormalForm
--
-- * Prove it!
-- The type of proofs we need are *homomorphisms*. They basically mean
-- that the operations on the normal form correspond to the operations
-- on expressions. Also, we don't use propositional equality: we use
-- any equivalence relation the user supplies.
--
-- Don't believe me? Check it out:
import Polynomial.Homomorphism
--
-- * How do I use it?
-- Copy the examples above! For the full solver, check out:
import Polynomial.Solver
--
-- * Wait! Don't!
-- The "full" solver lets you use different types for the coefficient
-- and carrier. You probably don't want that, unless you need the extra
-- efficiency. You'll want the *simple* solver:
import Polynomial.Simple.Solver
--
-- * Is that all?
-- No! As it happens, even the simple solver is complicated to use.
-- You'll *actually* want to use the reflection-based interface:
import Polynomial.Simple.Reflection
--
-- * And what about the step-by-step stuff?
-- That all uses the same underlying solver as the other stuff, with a
-- special *relation*. You can check that out here:
import Relation.Traced