subst.lean

mutual
inductive Subst : Type where
| ids : Subst
| tcons : Term → Subst → Subst
| shift : Subst
| comp : Subst → Subst → Subst
inductive Term : Type where
| var : Term
| lam : Term → Term
| app : Term → Term → Term
| sub : Term → Subst → Term
end

open Subst
open Term

notation "↑" => shift
notation t " ⬝ " σ => (tcons t σ)
notation σ:80 " ∘ " τ:80 => (comp σ τ)
notation t:70 " @ " u:70 => (app t u)
notation "Λ" => lam
notation t:60 "⟨" σ:60 "⟩" => (sub t σ)

inductive Ty where
| base : Ty
| arrow : Ty → Ty → Ty

open Ty

notation t " ⇒ " u:60 => (arrow t u)

notation "Ctx" => List Ty

set_option hygiene false

notation ctx₁:50 " ⊢ " sub:50 " :~ " ctx₂:50 => (TypeCtx ctx₁ sub ctx₂)
notation ctx:50 " ⊢ " t:50 " :+ " ty:50 => (TypeTerm ctx t ty)
mutual
inductive TypeCtx : Ctx → Subst → Ctx → Type where
| idTy : ∀ Γ, Γ ⊢ ids :~ Γ
| tconsTy : ∀ (Γ Δ : Ctx) A t σ, (Γ ⊢ t :+ A) → (Γ ⊢ σ :~ Δ) → Γ ⊢ t ⬝ σ :~ A :: Δ
| shiftTy : ∀ Γ A, (A :: Γ) ⊢ ↑ :~ Γ
| compTy : ∀ Γ Δ Ξ, Γ ⊢ σ :~ Δ → Δ ⊢ τ :~ Ξ → Γ ⊢ σ ∘ τ :~ Ξ
inductive TypeTerm : Ctx → Term → Ty → Type where
| varTy : ∀ Γ A, (A :: Γ) ⊢ var :+ A
| appTy : ∀ Γ A B t u, Γ ⊢ t :+ A ⇒ B → Γ ⊢ u :+ A → Γ ⊢ t @ u :+ B
| lamTy : ∀ Γ A t, (A :: Γ) ⊢ t :+ B → Γ ⊢ Λ t :+ A ⇒ B
| subTy : ∀ Γ Δ A t σ, Γ ⊢ σ :~ Δ → Δ ⊢ t :+ A → Γ ⊢ t⟨σ⟩ :+ A
end

infix:40 " ≅ " => SubstCong
infix:40 " ≃ " => TermCong

-- Taken from http://www.macs.hw.ac.uk/~fairouz/forest/papers/research-reports/Glasgow-TR-95-04.pdf
mutual
inductive SubstCong : Subst → Subst → Prop where
| idL : ids ∘ σ ≅ σ
| shiftId : ↑ ∘ (a ⬝ σ) ≅ σ
| mapS : (a ⬝ σ) ∘ τ ≅ a⟨τ⟩ ⬝ (σ ∘ τ)
| ass : (σ ∘ τ) ∘ ρ ≅ σ ∘ (τ ∘ ρ)
inductive TermCong : Term → Term → Prop where
| beta : (Λ a) @ b ≃ a⟨ tcons b ids ⟩
| varId : var⟨ ids ⟩ ≃ var
| varCons : var⟨a ⬝ σ⟩ ≃ a
| appSubst : (a @ b)⟨ σ ⟩ ≃ a⟨σ⟩ @ b⟨σ⟩
| absSubst : (Λ a)⟨σ⟩ ≃ Λ (a ⟨ var ⬝ (σ ∘ ↑)⟩)
| clos : a⟨σ⟩⟨τ⟩ ≃ a⟨σ ∘ τ⟩
end

-- Now we need to extend this to actually be a congruence: go under each constructor and refl sym trans.