roboguy13

-- Idea:
-- (1) Define a language of normal forms:                                                       Nf
-- (2) Define translations to and from the normal form language:                                from-Nf, to-Nf
-- (3) Show that normal forms are equal if and only if they are equal in the original language: ==→~, ~→==
-- (4) Prove the theorem about normal form language:                                            thm′
-- (5) Reflect that proof back into a statement about the original language:                    thm

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality renaming (subst to Eq-subst)

roboguy13

open import Relation.Binary.PropositionalEquality
open import Data.Product

open ≡-Reasoning

module MagmaMonoid where

Associative : ∀ {A} → (A → A → A) → Set
Associative _<>_ =
  ∀ a b c →

roboguy13

-- The algorithm here is based on the one in the paper "First-order unification by structural recursion" by Conor McBride.
-- There are some notes on the syntax in the McBride paper and how it
-- corresponds to the names here in some of the places where they differ.
--
-- The proofs are after the comment marking the beginning of the proofs.

open import Data.Nat hiding (_≤_)
import Data.Nat.Properties
import Data.Nat.Properties as ℕᵖ
open import Data.Product