module Ring.Syntax where
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive
open import SOAS.Metatheory.Syntax
open import Ring.Signature
private
variable
Ξ Ξ Ξ : Ctx
Ξ± : *T
π : Familyβ
module R:Terms (π : Familyβ) where
data R : Familyβ where
var : β βΎΜ£ R
mvar : π Ξ± Ξ β Sub R Ξ Ξ β R Ξ± Ξ
π : R * Ξ
_β_ : R * Ξ β R * Ξ β R * Ξ
π : R * Ξ
_β_ : R * Ξ β R * Ξ β R * Ξ
β_ : R * Ξ β R * Ξ
infixl 20 _β_
infixl 30 _β_
infixr 50 β_
open import SOAS.Metatheory.MetaAlgebra β
F π
Rα΅ : MetaAlg R
Rα΅ = record
{ πππ = Ξ» where
(zeroβ β
_) β π
(addβ β
a , b) β _β_ a b
(oneβ β
_) β π
(multβ β
a , b) β _β_ a b
(negβ β
a) β β_ a
; π£ππ = var ; ππ£ππ = Ξ» πͺ mΞ΅ β mvar πͺ (tabulate mΞ΅) }
module Rα΅ = MetaAlg Rα΅
module _ {π : Familyβ}(πα΅ : MetaAlg π) where
open MetaAlg πα΅
π€ππ : R βΎΜ£ π
π : Sub R Ξ Ξ β Ξ ~[ π ]β Ξ
π (t β Ο) new = π€ππ t
π (t β Ο) (old v) = π Ο v
π€ππ (mvar πͺ mΞ΅) = ππ£ππ πͺ (π mΞ΅)
π€ππ (var v) = π£ππ v
π€ππ π = πππ (zeroβ β
tt)
π€ππ (_β_ a b) = πππ (addβ β
π€ππ a , π€ππ b)
π€ππ π = πππ (oneβ β
tt)
π€ππ (_β_ a b) = πππ (multβ β
π€ππ a , π€ππ b)
π€ππ (β_ a) = πππ (negβ β
π€ππ a)
π€ππα΅β : MetaAlgβ Rα΅ πα΅ π€ππ
π€ππα΅β = record
{ β¨πππβ© = Ξ»{ {t = t} β β¨πππβ© t }
; β¨π£ππβ© = refl
; β¨ππ£ππβ© = Ξ»{ {πͺ = πͺ}{mΞ΅} β cong (ππ£ππ πͺ) (dext (π-tab mΞ΅)) } }
where
open β‘-Reasoning
β¨πππβ© : (t : β
R Ξ± Ξ) β π€ππ (Rα΅.πππ t) β‘ πππ (β
β π€ππ t)
β¨πππβ© (zeroβ β
_) = refl
β¨πππβ© (addβ β
_) = refl
β¨πππβ© (oneβ β
_) = refl
β¨πππβ© (multβ β
_) = refl
β¨πππβ© (negβ β
_) = refl
π-tab : (mΞ΅ : Ξ ~[ R ]β Ξ)(v : β Ξ± Ξ ) β π (tabulate mΞ΅) v β‘ π€ππ (mΞ΅ v)
π-tab mΞ΅ new = refl
π-tab mΞ΅ (old v) = π-tab (mΞ΅ β old) v
module _ (g : R βΎΜ£ π)(gα΅β : MetaAlgβ Rα΅ πα΅ g) where
open MetaAlgβ gα΅β
π€ππ! : (t : R Ξ± Ξ) β π€ππ t β‘ g t
π-ix : (mΞ΅ : Sub R Ξ Ξ)(v : β Ξ± Ξ ) β π mΞ΅ v β‘ g (index mΞ΅ v)
π-ix (x β mΞ΅) new = π€ππ! x
π-ix (x β mΞ΅) (old v) = π-ix mΞ΅ v
π€ππ! (mvar πͺ mΞ΅) rewrite cong (ππ£ππ πͺ) (dext (π-ix mΞ΅))
= trans (sym β¨ππ£ππβ©) (cong (g β mvar πͺ) (tabβixβid mΞ΅))
π€ππ! (var v) = sym β¨π£ππβ©
π€ππ! π = sym β¨πππβ©
π€ππ! (_β_ a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
π€ππ! π = sym β¨πππβ©
π€ππ! (_β_ a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
π€ππ! (β_ a) rewrite π€ππ! a = sym β¨πππβ©
R:Syn : Syntax
R:Syn = record
{ β
F = β
F
; β
:CS = β
:CompatStr
; mvarα΅’ = R:Terms.mvar
; π:Init = Ξ» π β let open R:Terms π in record
{ β₯ = R β Rα΅
; β₯-is-initial = record { ! = Ξ»{ {π β πα΅} β π€ππ πα΅ β π€ππα΅β πα΅ }
; !-unique = Ξ»{ {π β πα΅} (f β fα΅β) {x = t} β π€ππ! πα΅ f fα΅β t } } } }
open Syntax R:Syn public
open R:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Rα΅ public
open import SOAS.Metatheory R:Syn public