# semantics.debruijn.syntax

Require Import base data.fintype.

## Well-scoped untyped lambda terms.

Inductive tm (n : nat) : Type :=
| var (x : fin n)
| app (s t : tm n)
| lam (s : tm n.+1).

## Instantiation

Fixpoint rename {m n} (f : ren m n) (s : tm m) : tm n :=
match s with
| var x => var (f x)
| app s t => app (rename f s) (rename f t)
| lam s => lam (rename (up f) s)
end.

Definition subst m n := fin m -> tm n.

Definition upi {m n} (σ : subst m n) : subst m.+1 n.+1 :=
var bound .: σ >> rename shift.

Fixpoint inst {m n} (f : subst m n) (s : tm m) : tm n :=
match s with
| var x => f x
| app s t => app (inst f s) (inst f t)
| lam s => lam (inst (upi f) s)
end.

## Renaming as a special case of instantiation

Lemma 3.1
Lemma ren_inst m n (f : ren m n) (s : tm m) :
rename f s = inst (f >> @var _) s.
Proof.
elim: s n f => //={m}[m s ihs t iht|m s ihs] n f.
- by rewrite ihs iht.
- rewrite ihs. by fsimpl.
Qed.

Corollary 3.2
Lemma upi_def {m n} (σ : subst m n) :
upi σ = var bound .: σ >> inst (shift >> @var n.+1).
Proof.
fext=>/=; case=>//=i. by rewrite ren_inst.
Qed.

## Definitional laws

Fact 3.3 (1)
Lemma inst_app m n (σ : subst m n) (s t : tm m) :
inst σ (app s t) = app (inst σ s) (inst σ t).
Proof. by []. Qed.

Fact 3.3 (2)
Lemma inst_lam m n (σ : subst m n) (s : tm m.+1) :
inst σ (lam s) = lam (inst (var bound .: σ >> inst (shift >> @var _)) s).
Proof. by rewrite/= upi_def. Qed.

Fact 3.3 (3)
Lemma inst_bound m n (σ : subst m n) (s : tm n) :
inst (s .: σ) (var bound) = s.
Proof. by []. Qed.

Fact 3.3 (4)
Lemma inst_shift m n (σ : subst m n) (s : tm n) :
(shift >> @var _) >> inst (s .: σ) = σ.
Proof. by []. Qed.

Fact 3.3 (5)
Lemma scomp_id_l m n (σ : subst m n) :
@var _ >> inst σ = σ.
Proof. by []. Qed.

Fact 3.3 (6)
Lemma scons_inst_eta m n (σ : subst m.+1 n) :
inst σ (var bound) .: (shift >> @var _) >> inst σ = σ.
Proof. fext=>/=; by case. Qed.

Fact 3.3 (7)
Lemma scons_inst_eta_id m :
var bound .: shift >> @var m.+1 = @var _.
Proof. exact: scons_inst_eta. Qed.

Fact 3.3 (8)
Lemma scons_scomp_eta m n k (σ : subst m n) (τ : subst n k) (s : tm n) :
(s .: σ) >> inst τ = inst τ s .: σ >> inst τ.
Proof. fext=>/=; by case. Qed.

## Identity law

Lemma upi_ids n : upi (@var n) = @var n.+1.
Proof. fext=>/=. by case. Qed.

Lemma 3.4 (1)
Lemma ren_id n (s : tm n) : rename id s = s.
Proof.
elim: s => {n} //=.
- by move=> n s-> t->.
- move=> n s e. unfold up. fsimpl. by rewrite e.
Qed.

Lemma 3.4 (2)
Lemma inst_ids n (s : tm n) :
inst (@var _) s = s.
Proof.
by rewrite -ren_inst ren_id.
Qed.

Lemma 3.4 (3)
Lemma scomp_id m n (σ : subst m n) :
σ >> inst (@var n) = σ.
Proof.
fext=> i/=. exact: inst_ids.
Qed.

## Composition law

Lemma 3.5 (1)
Lemma ren_inst_comp m n k (f : ren m n) (g : subst n k) (s : tm m) :
inst g (rename f s) = inst (f >> g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- rewrite ihs. by fsimpl.
Qed.

Lemma 3.5 (2)
Lemma ren_comp m n k (f : ren m n) (g : ren n k) (s : tm m) :
rename g (rename f s) = rename (f >> g) s.
Proof.
by rewrite ren_inst ren_inst_comp ren_inst.
Qed.

Lemma upi_up_comp m n k (f : subst m n) (g : ren n k) :
upi f >> rename (up g) = upi (f >> rename g).
Proof.
fext=> /=-[i|]//=. by rewrite !ren_comp.
Qed.

Lemma 3.5 (3)
Lemma inst_ren_comp m n k (f : subst m n) (g : ren n k) (s : tm m) :
rename g (inst f s) = inst (f >> rename g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- by rewrite ihs upi_up_comp.
Qed.

Lemma 3.5 (4)
Lemma upi_comp m n k (f : subst m n) (g : subst n k) :
upi f >> inst (upi g) = upi (f >> inst g).
Proof.
fext=> /=-[i|]//=. by rewrite ren_inst_comp inst_ren_comp.
Qed.

Lemma 3.5 (5)
Lemma inst_comp m n k (f : subst m n) (g : subst n k) (s : tm m) :
inst g (inst f s) = inst (f >> inst g) s.
Proof.
elim: s n k f g => //={m}[m s ihs t iht|m s ihs] n k f g.
- by rewrite ihs iht.
- by rewrite ihs upi_comp.
Qed.

Lemma 3.5 (6)
Lemma scomp_assoc m n k l (σ : subst m n) (τ : subst n k) (θ : subst k l) :
(σ >> inst τ) >> inst θ = σ >> inst (τ >> inst θ).
Proof.
fext=> i /=. exact: inst_comp.
Qed.