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

-- 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 as List using (List; _∷_; [])
open import Function
open import Relation.Binary.PropositionalEquality as ≡
using (subst; _≡_; 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.Tactic.RingSolver

open AlmostCommutativeRing 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-∀

lemma₂ : ∀ x y → (x + y) ^ 2 ≈ x ^ 2 + 2 * x * y + y ^ 2
lemma₂ = solve-∀

-- 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 ≡⟨ solve (x ∷ y ∷ []) ⟩
3 + y + x     ≡⟨⟩
2 + 1 + y + x ∎
where open ≡-Reasoning

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

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

open AlmostCommutativeRing ring

-- 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.Tactic.RingSolver
open AlmostCommutativeRing ring

-- 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) ∎
```