semantics.debruijn.syntax

Require Import base data.fintype.

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

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.

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.

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.

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

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.

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

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

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

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

Lemma scons_inst_eta_id m :
  var bound .: shift >> @var m.+1 = @var _.
Proof. exact: scons_inst_eta. Qed.

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.

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

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 inst_ids n (s : tm n) :
  inst (@var _) s = s.
Proof.
  by rewrite -ren_inst ren_id.
Qed.

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

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 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 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 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 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 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.