Skip to content

Ring.lagda.md

Latest commit

 

History

History
104 lines (75 loc) · 3.02 KB

Ring.lagda.md

File metadata and controls

104 lines (75 loc) · 3.02 KB
Raw

Ring solver

solve-≈ proves equalities that hold in any commutative semiring or commutative ring. It is a practical, reflection-based frontend to the standard library's Algebra.Solver.Ring.

This file is literate Agda. The implementation lives in Tactic.Solver.Ring.Core; here we only define the macro, so that jumping to its definition lands on this documentation.

The solver handles both CommutativeSemiring and CommutativeRing, see below.

{-# OPTIONS --without-K --safe #-}
module Tactic.Solver.Ring where

open import Algebra using (CommutativeSemiring; CommutativeRing)
open import Reflection using (Term; TC)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality using (_≡_)

open import Tactic.Solver.Ring.Core using (solve-≈-macro)

macro
  solve-≈ : Term → Term → TC ⊤
  solve-≈ = solve-≈-macro

Examples

A first example: ℕ

Pass the bundle whose operations appear in the goal; ∀-bound variables are handled.

module ℕ-example where
  open import Data.Nat using (ℕ; _+_; _*_)
  open import Data.Nat.Properties using (+-*-commutativeSemiring)

  distrib : ∀ a b c → (a + b) * c ≡ (c * a) + (c * b)
  distrib a b = solve-≈ +-*-commutativeSemiring

Rings: subtraction and negation

A CommutativeRing bundle additionally lets the goal use _-_ and -_.

module ℤ-example where
  open import Data.Integer using (ℤ; _+_; _*_; _-_; -_)
  open import Data.Integer.Properties using (+-*-commutativeRing)

  difference-of-squares : ∀ a b → (a - b) * (a + b) ≡ a * a - b * b
  difference-of-squares a b = solve-≈ +-*-commutativeRing

  negation : ∀ a b → - (a + b) ≡ - a - b
  negation a b = solve-≈ +-*-commutativeRing

Literals

Each carrier's numeric literals are recognised as ring constants — 0/1 on ℕ, + n on ℤ, 0ℚ/1ℚ on ℚ.

module ℚ-example where
  open import Data.Rational using (ℚ; 0ℚ; 1ℚ; _+_; _*_)
  import Data.Rational.Properties as ℚP

  unit : ∀ q → q * 1ℚ ≡ q
  unit q = solve-≈ ℚP.+-*-commutativeRing

  zero : ∀ q → (q + 0ℚ) * 1ℚ ≡ q
  zero q = solve-≈ ℚP.+-*-commutativeRing

Abstract bundles

The carrier need not be concrete; under an abstract bundle, state the goal with its _≈_.

module abstract-example {c ℓ} (R : CommutativeSemiring c ℓ) where
  open CommutativeSemiring R

  rearrange : ∀ a b c d → ((a + b) + (c + d)) ≈ ((d + c) + (b + a))
  rearrange a b c d = solve-≈ R

Scope and limitations

  • The goal's relation may be the bundle's _≈_, or propositional _≡_ when that is the bundle's equality (as for ℕ/ℤ/ℚ).
  • Subterms the solver does not recognise as ring syntax become opaque atoms: it proves the goal treating them as fresh variables, so an identity that depends on their internal structure will not be found.
  • Carriers that are themselves function types (with a pointwise _≈_) are not supported.

Tactic.Solver.Ring.Tests.* exercises many more goals and bundle shapes.