------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the reflective ring solver may be used.
------------------------------------------------------------------------

module README.Tactic.RingSolver where

-- 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 (ℤ)
import Data.Nat.Literals as ℕ
import Data.Integer.Literals as ℤ

instance
  numberNat : Number ℕ
  numberNat = ℕ.number

instance
  numberInt : Number ℤ
  numberInt = ℤ.number

------------------------------------------------------------------------------
-- Imports!

open import Data.List.Base as List using (List; _∷_; [])
open import Relation.Binary.PropositionalEquality
  using (subst; cong; _≡_; module ≡-Reasoning)
open import Data.Bool as Bool using (Bool; true; false; if_then_else_)
open import Data.Unit using (⊤; tt)

open import Tactic.RingSolver.Core.AlmostCommutativeRing
  using (AlmostCommutativeRing)

------------------------------------------------------------------------
-- Integer examples
------------------------------------------------------------------------

module IntegerExamples where
  open import Data.Integer hiding (_^_)
  open import Data.Integer.Tactic.RingSolver

  open AlmostCommutativeRing ring using (_^_)

  -- Everything is automatic: you just ask Agda to solve it and it does!

  -- Addition
  lemma₁ : ∀ x y → x + y + 3 ≡ 2 + y + x + 1
  lemma₁ = solve-∀

  -- Multiplication
  lemma₂ : ∀ x → x * 2 + 1 ≡ x + 1 + x
  lemma₂ = solve-∀

  -- Negation
  lemma₃ : ∀ x y → (- x) + (- y) ≡ - (x + y)
  lemma₃ = solve-∀

  -- Subtraction
  lemma₄ : ∀ x y → (x - y) * 2 - 2 ≡ (- 2) * y - 1 + 2 * x - 1
  lemma₄ = solve-∀

  -- Exponentiation by constant literals
  lemma₅ : ∀ x y → (x + y) ^ 2 ≡ x ^ 2 + 2 * x * y + y ^ 2
  lemma₅ = solve-∀

  -- It can be interleaved with manual proofs as well.
  lemma₆ : ∀ x y z → y ≡ z → x + y * 1 + 3 ≡ 2 + z + x + 1
  lemma₆ x y z y≡z = begin
    x + y * 1 + 3 ≡⟨ solve (x ∷ y ∷ []) ⟩
    2 + y + x + 1 ≡⟨ cong (λ v → 2 + v + x + 1) y≡z ⟩
    2 + z + x + 1 ∎
    where open ≡-Reasoning

------------------------------------------------------------------------
-- Natural examples
------------------------------------------------------------------------

module NaturalExamples where
  open import Data.Nat
  open import Data.Nat.Tactic.RingSolver

  -- The solver is flexible enough to work with ℕ (even though it asks
  -- for rings!)
  lemma₁ : ∀ x y → x + y * 1 + 3 ≡ 2 + 1 + y + x
  lemma₁ = solve-∀

------------------------------------------------------------------------
-- Checking invariants
------------------------------------------------------------------------
-- 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
  open import Data.Nat hiding (_≤_)
  open import Data.Nat.Tactic.RingSolver

  -- A Skew Heap, indexed by its size.
  data Tree : ℕ → Set a where
    leaf : Tree 0
    node : ∀ {n m} → A → Tree n → Tree m → Tree (1 + n + m)

  -- A substitution operator, to clean things up.
  infixr 1 _⇒_
  _⇒_ : ∀ {n} → Tree n → ∀ {m} → n ≡ m → Tree m
  x ⇒ n≡m  = subst Tree n≡m x

  open ≡-Reasoning

  _∪_ : ∀ {n m} → Tree n → Tree m → Tree (n + m)
  leaf                 ∪ ys                   = ys
  node {a} {b} x xl xr ∪ leaf                 =
    node x xl xr ⇒ solve (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 ⇒ begin
          1 + (1 + c + d + b) + a ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
          1 + a + b + (1 + c + d) ∎
        else node y (node x xl xr ∪ yr) yl ⇒ begin
          1 + (1 + a + b + d) + c ≡⟨ solve (a ∷ b ∷ c ∷ d ∷ []) ⟩
          1 + a + b + (1 + c + d) ∎