module DeBruijnExSubstSized where open import Prelude -- using (_∘_) -- composition, identity open import Data.Nat open import Data.Maybe open import Logic.Identity renaming (subst to subst≡) import Logic.ChainReasoning module Chain = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans) open Chain open import DeBruijn Size : Set Size = Nat -- untyped de Bruijn terms data LamE (A : Set) : Size -> Set where varE : {ι : _} -> A -> LamE A (suc ι) appE : {ι : _} -> LamE A ι -> LamE A ι -> LamE A (suc ι) absE : {ι : _} -> LamE (Maybe A) ι -> LamE A (suc ι) flatE : {ι : _} -> LamE (LamE A ι) ι -> LamE A (suc ι) -- functoriality of LamE lamE : {A B : Set} -> (A -> B) -> {ι : _} -> LamE A ι -> LamE B ι lamE f {suc ι} (varE a) = varE (f a) lamE f {suc ι} (appE t1 t2) = appE (lamE f t1) (lamE f t2) lamE f {suc ι} (absE r) = absE (lamE (fmap f) r) lamE f {suc ι} (flatE r) = flatE (lamE (lamE f) r) eval : {ι : _} -> {A : Set} -> LamE A ι -> Lam A eval {suc ι} (varE a) = var a eval {suc ι} (appE t1 t2) = app (eval t1) (eval t2) eval {suc ι} (absE r) = abs (eval r) eval {suc ι} (flatE r) = subst (eval) (eval r) evalNAT : {A B : Set}(f : A -> B) -> {ι : _} -> (t : LamE A ι) -> eval (lamE f t) ≡ lam f (eval t) evalNAT f {suc ι} (varE a) = refl evalNAT f {suc ι} (appE t1 t2) = chain> eval (lamE f (appE t1 t2)) === eval (appE (lamE f t1) (lamE f t2)) by refl === app (eval (lamE f t1)) (eval (lamE f t2)) by refl === app (lam f (eval t1)) (eval (lamE f t2)) by cong (\ x -> app x (eval (lamE f t2))) (evalNAT f t1) === app (lam f (eval t1)) (lam f (eval t2)) by cong (\ x -> app (lam f (eval t1)) x) (evalNAT f t2) === lam f (app (eval t1) (eval t2)) by refl === lam f (eval (appE t1 t2)) by refl evalNAT f {suc ι} (absE r) = chain> eval (lamE f (absE r)) === eval (absE (lamE (fmap f) r)) by refl === abs (eval (lamE (fmap f) r)) by refl === abs (lam (fmap f) (eval r)) by cong abs (evalNAT (fmap f) r) === lam f (abs (eval r)) by refl === lam f (eval (absE r)) by refl evalNAT f {suc ι} (flatE r) = chain> eval (lamE f (flatE r)) === eval (flatE (lamE (lamE f) r)) by refl === subst eval (eval (lamE (lamE f) r)) by refl === subst eval (lam (lamE f) (eval r)) by cong (subst eval) (evalNAT (lamE f) r) === subst (eval ∘ lamE f) (eval r) by substLaw1 (lamE f) eval (eval r) === subst (lam f ∘ eval) (eval r) by substExt _ _ (evalNAT f) (eval r) === lam f (subst eval (eval r)) by substLaw2 f eval (eval r) === lam f (eval (flatE r)) by refl evalNATcor : {A : Set}{ι : _}(ee : LamE (LamE A ι) ι) -> subst id (eval (lamE eval ee)) ≡ eval (flatE ee) evalNATcor ee = chain> subst id (eval (lamE eval ee)) === subst id (lam eval (eval ee)) by cong (subst id) (evalNAT eval ee) === subst eval (eval ee) by substLaw1 eval id (eval ee) === eval (flatE ee) by refl