module Example where

open import Basics
open import Expr hiding (eqn₁)
import Semantics as Sem
open import Relation.Binary.PropositionalEquality

eqn₁ : Eqn 
eqn₁ = build  λ a b → (a ⊕ b) ⊕ a == b ⊕ (a ⊕ a)

open import Algebra
open import Data.Nat.Properties using (commutativeSemiring)
open CommutativeSemiring commutativeSemiring
     using (+-commutativeMonoid)

open Sem +-commutativeMonoid

prf₁ : ∀ n m → (n + m) + n ≡ m + (n + n)
prf₁ n m = prove eqn₁ (n ∷ m ∷ []) refl

prf₂ : ∀ a b c d → _
prf₂ a b c d =
  prove
    (build  λ a b c d → (a ⊕ b) ⊕ (c ⊕ d) == (a ⊕ c) ⊕ (b ⊕ d))
    (a ∷ b ∷ c ∷ d ∷ [])
    refl