Require Import base wp.states data.fintype.

Inductive tm (n : nat) :=
| Act (a : action) (s : tm n)
| If (b : guard) (s t : tm n)
| Def (s t : tm n.+1)
| Jump (f : fin n).
Arguments Jump {n} f.

Definition Ω {n} : tm n :=
  Def (Jump bound) (Jump bound).

Fixpoint rinst {m n : nat} (ξ : ren m n) (s : tm m) : tm n :=
  match s with
  | Act a s => Act a (rinst ξ s)
  | If b s t => If b (rinst ξ s) (rinst ξ t)
  | Def s t => Def (rinst (up ξ) s) (rinst (up ξ) t)
  | Jump f => Jump (ξ f)
  end.

Definition subst (m n : nat) : Type :=
  fin m -> tm n.

Definition upi {m n : nat} (θ : subst m n) : subst m.+1 n.+1 :=
  Jump bound .: θ >> rinst shift.

Fixpoint inst {m n : nat} (θ : subst m n) (s : tm m) : tm n :=
  match s with
  | Act a s => Act a (inst θ s)
  | If b s t => If b (inst θ s) (inst θ t)
  | Def s t => Def (inst (upi θ) s) (inst (upi θ) t)
  | Jump f => θ f
  end.

Lemma rinst_inst m n (ξ : ren m n) (s : tm m) :
  rinst ξ s = inst (ξ >> Jump) s.
Proof.
  elim: s n ξ => //={m} [m a s ih|m b s ihs t iht|m s ihs t iht] n ξ.
  by rewrite ih. by rewrite ihs iht. rewrite ihs iht /upi/up; by fsimpl.
Qed.

Lemma rinst_id n (s : tm n) :
  rinst id s = s.
Proof.
  elim: s => //={n}[n a s ih|n b s ihs t iht|n s ihs t iht].
  by rewrite ih. by rewrite ihs iht. unfold up; fsimpl. by rewrite ihs iht.
Qed.

Lemma inst_ids n (s : tm n) :
  inst Jump s = s.
Proof. by rewrite-{2}[s]rinst_id rinst_inst. Qed.

Lemma rinst_inst_comp m n k (ξ : ren m n) (θ : subst n k) (s : tm m) :
  inst θ (rinst ξ s) = inst (ξ >> θ) s.
Proof.
  elim: s n k ξ θ => //={m}[m a s ih|m b s ihs t iht|m s ihs t iht] n k ξ θ.
  by rewrite ih. by rewrite ihs iht. rewrite ihs iht /up/upi; by fsimpl.
Qed.

Lemma rinst_comp m n k (ξ : ren m n) (ζ : ren n k) (s : tm m) :
  rinst ζ (rinst ξ s) = rinst (ξ >> ζ) s.
Proof.
  by rewrite {1}rinst_inst rinst_inst_comp rinst_inst.
Qed.

Lemma rinst_compF m n k (ξ : ren m n) (ζ : ren n k) :
  rinst ξ >> rinst ζ = rinst (ξ >> ζ).
Proof.
  fext. exact: rinst_comp.
Qed.

Lemma inst_rinst_comp m n k (θ : subst m n) (ξ : ren n k) (s : tm m) :
  rinst ξ (inst θ s) = inst (θ >> rinst ξ) s.
Proof.
  elim: s n k ξ θ => //={m}[m a s ih|m b s ihs t iht|m s ihs t iht] n k ξ θ.
  by rewrite ih. by rewrite ihs iht. rewrite ihs iht /up/upi/=; fsimpl=>/=.
  rewrite !rinst_compF. by fsimpl.
Qed.

Lemma upi_comp m n k (θ₁ : subst m n) (θ₂ : subst n k) :
  upi θ₁ >> inst (upi θ₂) = upi (θ₁ >> inst θ₂).
Proof.
  fext=>/=-[]//=i. by rewrite rinst_inst_comp inst_rinst_comp.
Qed.

Lemma inst_comp m n k (θ₁ : subst m n) (θ₂ : subst n k) (s : tm m) :
  inst θ₂ (inst θ₁ s) = inst (θ₁ >> inst θ₂) s.
Proof.
  elim: s n k θ₁ θ₂ => //={m}[m a s ih|m b s ihs t iht|m s ihs t iht] n k θ₁ θ₂.
    by rewrite ih. by rewrite ihs iht. by rewrite ihs iht upi_comp.
Qed.