module Palmse.Monoid.NbeComplete (A : Set) where

import Palmse.Monoid.Exp; open Palmse.Monoid.Exp A
import Palmse.Monoid.Nbe; open Palmse.Monoid.Nbe A
import Palmse.Monoid.Laws; open Palmse.Monoid.Laws A
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as Reason
open Reason (≡-setoid Exp)

sem-fun : {e e' e'' : Exp} -> e ∼ e' -> [[ e ]] e'' ≡ [[ e' ]] e''
sem-fun ass = ≡-refl
sem-fun idl = ≡-refl
sem-fun idr = ≡-refl
sem-fun ref = ≡-refl 
sem-fun (sym p) = ≡-sym (sem-fun p)
sem-fun (tra p q) = ≡-trans (sem-fun p) (sem-fun q)
sem-fun {e'' = e''} (fun {e₀} {e₁} {e₂} {e₃} p q) = 
  begin
    [[ e₀ ○ e₂ ]] e''
       ≈⟨ ≡-refl ⟩
    [[ e₀ ]] ([[ e₂ ]] e'') 
       ≈⟨ ≡-cong [[ e₀ ]] (sem-fun q)  ⟩
    [[ e₀ ]] ([[ e₃ ]] e'')
       ≈⟨ sem-fun p ⟩
    [[ e₁ ]] ([[ e₃ ]] e'')
       ≈⟨ ≡-refl ⟩
    [[ e₁ ○ e₃ ]] e''
  ∎

-- fun is congruence wrt composition
-- note that =-refl steps in fun-case are redundant 
-- and only there for didactic purposes
-- note that idl, idr, ass are done by =-refl, because Agda normalizes the types
-- (application of nbe)

complete : {e e' : Exp} -> e ∼ e' -> nbe e ≡ nbe e'
complete p = sem-fun {e'' = id} p

-- nbe e = [[ e ]] id, so we only need to apply sem-fun to id