------------------------------------------------------------------------
-- 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 7 _⊙_

-- 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 4  a b c d  (a  b)  (c  d)  a  (b  c)  d) refl
                                -- ^ Here we reflect the shape of the proof we want