-- Parallel substitution as an operation for untyped de Bruijn terms -- Author: Andreas Abel -- Date : 2011-03-01 -- -- Instead of distinguishing renamings and substitutions as in -- -- Chung-Kil Hur et al., -- Strongly Typed Term Representations in Coq -- -- which leads to 4 different composition operations, -- we define a generic substitution/renaming operation. -- This is inspired by -- -- Conor McBride -- Type Preserving Renaming and Substitution -- -- but, being not restricted to structural recursion, we can utilize -- the lexicographically terminating definition of -- -- Thorsten Altenkirch and Bernhard Reus -- Monadic Presentations of Lambda Terms Using Generalized Inductive Types -- -- This way, we have a single composition operation and lemma, which is mutual -- with a lemma for composition of liftings. module ParallelSubstitution where open import Data.Nat open import Relation.Binary.PropositionalEquality renaming (subst to coerce) open ≡-Reasoning -- since we model substitutions as functions over natural numbers -- (instead of lists), functional extensionality is very convenient to have! postulate funExt : ∀ {A : Set}{B : Set}{f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g -- De Bruijn lambda terms data Tm : Set where var : (x : ℕ) → Tm abs : (t : Tm) → Tm app : (t u : Tm) → Tm -- A structurally ordered two-element set data VarTrm : ℕ → Set where Var : VarTrm 0 -- we are dealing with variables (natural numbers) Trm : VarTrm 1 -- we are dealing with terms max01 : ℕ → ℕ → ℕ max01 0 m = m max01 n m = n compVT : ∀ {n m} (vt : VarTrm n) (vt' : VarTrm m) → VarTrm (max01 n m) compVT Var vt' = vt' compVT Trm vt = Trm -- A set of variables or terms VT : ∀ {n} → (vt : VarTrm n) → Set VT Var = ℕ VT Trm = Tm -- A mapping which is either a renaming (Var) or substitution (Trm) RenSub : ∀ {n} → (vt : VarTrm n) → Set RenSub vt = ℕ → VT vt Ren = ℕ → ℕ -- Renamings Subst = ℕ → Tm -- Substitutions -- We define lifting in terms of substitution -- See, e.g., Altenkirch and Reus, CSL 1999 mutual lift : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → RenSub vt -- lifting a renaming lift {vt = Var} tau 0 = 0 lift {vt = Var} tau (suc x') = suc (tau x') -- lifting a substituion lift {vt = Trm} tau 0 = var 0 lift {vt = Trm} tau (suc x') = subst suc (tau x') -- shift subst : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → Tm → Tm subst {vt = vt } tau (abs t) = abs (subst (lift tau) t) subst {vt = vt } tau (app t u) = app (subst tau t) (subst tau u) -- PUT THESE LAST BECAUSE OF AGDA SPLIT HEURISTICS: subst {vt = Var} tau (var x) = var (tau x) -- lookup in renaming subst {vt = Trm} tau (var x) = tau x -- lookup in substitution -- substitution composition comp : ∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2) {m}{vt1 : VarTrm m}(sigma : RenSub vt1) → RenSub (compVT vt1 vt2) comp tau {vt1 = Var} sigma x = tau (sigma x) comp tau {vt1 = Trm} sigma x = subst tau (sigma x) -- Composition lemma mutual comp_lift : ∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2) {m}{vt1 : VarTrm m}(sigma : RenSub vt1) → comp (lift tau) (lift sigma) ≡ lift (comp tau sigma) comp_lift tau sigma = funExt (comp_lift' tau sigma) comp_lift' : ∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2) {m}{vt1 : VarTrm m}(sigma : RenSub vt1)(x : ℕ) → comp (lift tau) (lift sigma) x ≡ lift (comp tau sigma) x comp_lift' {vt2 = Var} tau {vt1 = Var} sigma zero = refl comp_lift' {vt2 = Trm} tau {vt1 = Var} sigma zero = refl comp_lift' {vt2 = Var} tau {vt1 = Trm} sigma zero = refl comp_lift' {vt2 = Trm} tau {vt1 = Trm} sigma zero = refl comp_lift' {vt2 = Var} tau {vt1 = Var} sigma (suc x') = refl comp_lift' {vt2 = Trm} tau {vt1 = Var} sigma (suc x') = refl comp_lift' {vt2 = Var} tau {vt1 = Trm} sigma (suc x') = begin subst (lift tau) (subst suc (sigma x')) ≡⟨ comp_subst (lift tau) suc (sigma x') ⟩ subst (comp (lift tau) suc) (sigma x') ≡⟨ refl ⟩ subst (λ x → comp (lift tau) suc x) (sigma x') ≡⟨ refl ⟩ subst (λ x → suc (tau x)) (sigma x') ≡⟨ refl ⟩ subst (λ x → comp suc tau x) (sigma x') ≡⟨ refl ⟩ subst (comp suc tau) (sigma x') ≡⟨ sym (comp_subst suc tau (sigma x')) ⟩ subst suc (subst tau (sigma x')) ∎ comp_lift' {vt2 = Trm} tau {vt1 = Trm} sigma (suc x') = begin subst (lift tau) (subst suc (sigma x')) ≡⟨ comp_subst (lift tau) suc (sigma x') ⟩ subst (comp (lift tau) suc) (sigma x') ≡⟨ refl ⟩ subst (λ x → comp (lift tau) suc x) (sigma x') ≡⟨ refl ⟩ subst (λ x → subst suc (tau x)) (sigma x') -- distinct line! ≡⟨ refl ⟩ subst (λ x → comp suc tau x) (sigma x') ≡⟨ refl ⟩ subst (comp suc tau) (sigma x') ≡⟨ sym (comp_subst suc tau (sigma x')) ⟩ subst suc (subst tau (sigma x')) ∎ comp_subst : ∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2) {m}{vt1 : VarTrm m}(sigma : RenSub vt1)(t : Tm) → subst tau (subst sigma t) ≡ subst (comp tau sigma) t comp_subst {vt2 = Var} tau {vt1 = Var} sigma (var x) = refl comp_subst {vt2 = Var} tau {vt1 = Trm} sigma (var x) = refl comp_subst {vt2 = Trm} tau {vt1 = Var} sigma (var x) = refl comp_subst {vt2 = Trm} tau {vt1 = Trm} sigma (var x) = refl comp_subst {vt2 = vt2} tau {vt1 = vt1} sigma (abs t) = begin subst tau (subst sigma (abs t)) ≡⟨ refl ⟩ subst tau (abs (subst (lift sigma) t)) ≡⟨ refl ⟩ abs (subst (lift tau) (subst (lift sigma) t)) ≡⟨ cong abs (comp_subst (lift tau) (lift sigma) t) ⟩ abs (subst (comp (lift tau) (lift sigma)) t) ≡⟨ cong (λ sigma' → abs (subst sigma' t)) (comp_lift tau sigma) ⟩ abs (subst (lift (comp tau sigma)) t) ≡⟨ refl ⟩ subst (comp tau sigma) (abs t) ∎ comp_subst {vt2 = vt2} tau {vt1 = vt1} sigma (app t u) = begin subst tau (subst sigma (app t u)) ≡⟨ refl ⟩ app (subst tau (subst sigma t)) (subst tau (subst sigma u)) ≡⟨ cong (λ t' → app t' (subst tau (subst sigma u))) (comp_subst tau sigma t) ⟩ app (subst (comp tau sigma) t) (subst tau (subst sigma u)) ≡⟨ cong (λ u' → app (subst (comp tau sigma) t) u') (comp_subst tau sigma u) ⟩ app (subst (comp tau sigma) t) (subst (comp tau sigma) u) ≡⟨ refl ⟩ subst (comp tau sigma) (app t u) ∎