-- 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   -- we are dealing with variables (natural numbers)
  Trm : VarTrm   -- we are dealing with terms

max01 : ℕ → ℕ → ℕ
max01  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         =      
  lift {vt = Var} tau (suc x') = suc (tau x') 
  -- lifting a substituion  
  lift {vt = Trm} tau         = var 
  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)
    ∎