```
open import Algebra

module Semantics (CM : CommutativeMonoid) where

open import Basics
open import Expr
open CommutativeMonoid CM
renaming (carrier to C; setoid to C-setoid)
open import Relation.Binary.PropositionalEquality
hiding (sym; trans)
renaming (refl to ≡-refl)

import Relation.Binary.EqReasoning as EqR
renaming (_≈⟨_⟩_ to _≈<_>_; _≡⟨_⟩_ to _≡<_>_)

open EqR C-setoid

Env : ℕ → Set
Env n = Vec C n

[_] : ∀ {n} → Expr n → Env n → C
[ var i ] ρ = ρ ! i
[ a ⊕ b ] ρ = [ a ] ρ ∙ [ b ] ρ
[ zero  ] ρ = ε

[∣_∣] : ∀ {n} → Eqn n → Env n → Set
[∣ a == b ∣] ρ = [ a ] ρ ≈ [ b ] ρ

_≅_ : ∀ {n} → Expr n → Expr n → Set
a ≅ b = ∀ ρ → [ a ] ρ ≈ [ b ] ρ

-- Soundness

open import Data.Product

sound-zero : ∀ {n m} (es : Vec (Expr m) n) →
zero ≅ poly (const 0) es
sound-zero {zero}  []       ρ = refl
sound-zero {suc n} (_ ∷ es) ρ =
begin
ε
≈< sym (proj₁ identity _) >
ε ∙ ε
≈< ∙-pres-≈ refl (sound-zero es ρ) >
ε ∙ [ poly (const 0) es ] ρ
∎

distr : ∀ {n} k j (e : Expr n) → k ⊗ e ⊕ j ⊗ e ≅ (k + j) ⊗ e
distr zero    j e ρ = proj₁ identity _
distr (suc k) j e ρ =
begin
[ (e ⊕ k ⊗ e) ⊕ j ⊗ e ] ρ
≈< assoc _ _ _ >
[ e ⊕ (k ⊗ e ⊕ j ⊗ e) ] ρ
≈< ∙-pres-≈ refl (distr k j e ρ) >
[ e ⊕ (k + j) ⊗ e ] ρ
∎

sound-plus : ∀ {n m} (ks js : Vec ℕ n) (xs : Vec (Expr m) n) →
poly ks xs ⊕ poly js xs ≅
poly (zipWith _+_ ks js) xs
sound-plus [] [] [] ρ = proj₁ identity _
sound-plus (k ∷ ks) (j ∷ js) (x ∷ xs) ρ =
begin
[ (k ⊗ x ⊕ poly ks xs) ⊕ (j ⊗ x ⊕ poly js xs) ] ρ
≈< shuffle (k ⊗ x) (poly ks xs) (j ⊗ x) (poly js xs) ρ >
[ (k ⊗ x ⊕ j ⊗ x) ⊕ (poly ks xs ⊕ poly js xs) ] ρ
≈< ∙-pres-≈ (distr k j x ρ) (sound-plus ks js xs ρ) >
[ (k + j) ⊗ x ⊕ poly (zipWith _+_ ks js) xs ] ρ
∎
where
shuffle : ∀ {n} (a b c d : Expr n) →
(a ⊕ b) ⊕ (c ⊕ d) ≅ (a ⊕ c) ⊕ (b ⊕ d)
shuffle a b c d ρ =
begin
[ (a ⊕ b) ⊕ (c ⊕ d) ] ρ
≈< assoc _ _ _ >
[ a ⊕ (b ⊕ (c ⊕ d)) ] ρ
≈< ∙-pres-≈ refl (sym (assoc _ _ _)) >
[ a ⊕ ((b ⊕ c) ⊕ d) ] ρ
≈< ∙-pres-≈ refl (∙-pres-≈ (comm _ _) refl) >
[ a ⊕ ((c ⊕ b) ⊕ d) ] ρ
≈< ∙-pres-≈ refl (assoc _ _ _) >
[ a ⊕ (c ⊕ (b ⊕ d)) ] ρ
≈< sym (assoc _ _ _) >
[ (a ⊕ c) ⊕ (b ⊕ d) ] ρ
∎

sound-var : ∀ {n m} (i : Fin n) (es : Vec (Expr m) n) →
(es ! i) ≅ poly (unit i) es
sound-var zero (e ∷ es) ρ =
begin
[ e ] ρ
≈< sym (proj₂ identity _) >
[ e ⊕ zero ] ρ
≈< sym (proj₂ identity _) >
[ (e ⊕ zero) ⊕ zero ] ρ
≈< ∙-pres-≈ refl (sound-zero es ρ) >
[ (e ⊕ zero) ⊕ poly (const 0) es ] ρ
∎
sound-var (suc i) (e ∷ es) ρ =
begin
[ es ! i ] ρ
≈< sound-var i es ρ >
[ poly (unit i) es ] ρ
≈< sym (proj₁ identity _) >
[ zero ⊕ poly (unit i) es ] ρ
∎

sound : ∀ {n} (e : Expr n) → e ≅ norm e
sound (var i) ρ =
begin
[ var i ] ρ
≡< cong (λ e → [ e ] ρ) (lem-tabulate-! var i) >
[ vars ! i ] ρ
≈< sound-var i vars ρ >
[ norm (var i) ] ρ
∎
sound (a ⊕ b) ρ =
begin
[ a ⊕ b ] ρ
≈< ∙-pres-≈ (sound a ρ) (sound b ρ) >
[ norm a ⊕ norm b ] ρ
≈< sound-plus (eval a) (eval b) vars ρ >
[ norm (a ⊕ b) ] ρ
∎
sound zero    ρ = sound-zero vars ρ

-- sound : ∀ {n}(a : Expr n) → a ≅ norm a
-- sound a ρ = {!!}

prove : ∀ {n}(eq : Eqn n) ρ → [∣ normEqn eq ∣] ρ → [∣ eq ∣] ρ
prove (a == b) ρ prf =
begin
[ a ] ρ
≈< sound a ρ >
[ norm a ] ρ
≈< prf >
[ norm b ] ρ
≈< sym (sound b ρ) >
[ b ] ρ
∎
```