------------------------------------------------------------------------
-- This module automates the process of producing equivalence proofs
-- on arbitrary Monoids using the Reflection module provided in Agda's
-- standard library.
--
-- Proofs involving associativity can be frustratingly mechanical, but this
-- module primarily serves as an introduction to the Reflection module.
--
-- For a more advanced use of the Reflection module, see Algebra.RingSolver
-- I have also implemented a Solver module for CommutativeMonoids.
--
-- What is a monoid?
-- A "Carrier" set of values
-- An equivalence _≈_
-- An associative, binary operation _∙_ which respects _≈_
-- An identity element ε
--
-- By the end of this module, we'll be able to automate proofs like:
-- ∀ a b c d → (a ∙ b) ∙ (c ∙ d) ≈ a ∙ (b ∙ c) ∙ d
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Algebra using (Monoid; module Monoid)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Vec using (Vec; lookup)
open import Data.List using (List; _∷_; []; [_]; _++_; foldr)
open import Data.Product using (proj₁; proj₂)
open import Level using (Level)
import Relation.Binary.EqReasoning as Eq

module MonoidSolver {a ℓ : Level} (M : Monoid a ℓ) where

open Monoid M using (Carrier; _∙_; _≈_; ε; ∙-cong; assoc; identity; refl; setoid; sym)
open Eq setoid using (begin_; _≈⟨_⟩_; _∎)

-- The Syntax type allows us to reflect the shape of the proof
-- we wish to automate. We will "reflect" our goal into a Syntax
-- value and use this convert our proof obligation to a much
-- simpler one on normal forms. The 'n' is the number of unique
-- variables in the expression.

data Syntax (n : ℕ) : Set where
  _⊙_ : Syntax n → Syntax n → Syntax n
  var : Fin n → Syntax n
  :0 : Syntax n

infixl  _⊙_

-- This semantic evaluation function constructs a value
-- of Carrier which preserves the shape of the Syntax
-- tree. This is the shape of the proof we want to have.

⟦_⟧ : {n : ℕ} → Syntax n → Vec Carrier n → Carrier
⟦ x₁ ⊙ x₂ ⟧ ρ = ⟦ x₁ ⟧ ρ ∙ ⟦ x₂ ⟧ ρ
⟦ var i   ⟧ ρ = lookup i ρ
⟦ :0      ⟧ _ = ε

private
  flatten : {n : ℕ} → Syntax n → Vec Carrier n → List Carrier
  flatten (x₁ ⊙ x₂) ρ = flatten x₁ ρ ++ flatten x₂ ρ
  flatten (var i)   ρ = [ lookup i ρ ]
  flatten :0        _ = []

  sum : List Carrier → Carrier
  sum = foldr _∙_ ε

-- This normalized semantic evaluation function constructs a
-- value of Carrier which is semantically equivalent to the
-- one produced by ⟦_⟧, however all occurences of _∙_ are
-- made right-associative and all ε elements are eliminated.
-- This is the shape of the proof we want to provide.

⟦_⇓⟧ : {n : ℕ} → Syntax n → Vec Carrier n → Carrier
⟦ x ⇓⟧ ρ = sum (flatten x ρ)

private
  sum-++ : (xs ys : List Carrier) → sum (xs ++ ys) ≈ sum xs ∙ sum ys
  sum-++ []       ys = sym (proj₁ identity _)
  sum-++ (x ∷ xs) ys = begin
    x ∙  sum (xs ++ ys)   ≈⟨ ∙-cong refl (sum-++ xs ys) ⟩
    x ∙ (sum xs ∙ sum ys) ≈⟨ sym (assoc _ _ _) ⟩
    x ∙  sum xs ∙ sum ys  ∎

-- By proving that these two semantic evaluation functions produce
-- semantically equivalent values we'll be able to use equivalence
-- proofs about the normalized forms to talk about the equivalence
-- of the original values.

correct : {n : ℕ} (s : Syntax n) (ρ : Vec Carrier n) → ⟦ s ⇓⟧ ρ ≈ ⟦ s ⟧ ρ
correct :0        ρ = refl
correct (var i)   ρ = proj₂ identity (lookup i ρ)
correct (x₁ ⊙ x₂) ρ = begin
   ⟦ x₁      ⊙  x₂ ⇓⟧ ρ ≈⟨ sum-++ (flatten x₁ ρ) (flatten x₂ ρ) ⟩
   ⟦ x₁ ⇓⟧ ρ ∙ ⟦ x₂ ⇓⟧ ρ ≈⟨ ∙-cong (correct x₁ ρ) (correct x₂ ρ) ⟩
   ⟦ x₁  ⟧ ρ ∙ ⟦ x₂  ⟧ ρ ∎ 

import Relation.Binary.Reflection as R
open R setoid var ⟦_⟧ ⟦_⇓⟧ correct public using (prove; close; solve; solve₁; _⊜_)

private
  -- Now for a simple example
  Example = ∀ a b c d → (a ∙ b) ∙ (c ∙ d) ≈ a ∙ (b ∙ c) ∙ d

  -- A manual proof using equational reasoning looks like this.
  manual : Example
  manual a b c d = begin
    (a ∙ b) ∙ (c ∙ d) ≈⟨ sym (assoc (a ∙ b) c d) ⟩
     a ∙ b  ∙  c ∙ d  ≈⟨ ∙-cong (assoc a b c) refl ⟩
     a ∙ (b ∙ c) ∙ d  ∎

  -- Let's see the solver in action!
  automatic : Example
  automatic = solve  (λ a b c d → (a ⊙ b) ⊙ (c ⊙ d) ⊜ a ⊙ (b ⊙ c) ⊙ d) refl
                                -- ^ Here we reflect the shape of the proof we want