semantics.debruijn.reduction

Require Import base data.fintype debruijn.syntax.

Inductive step {m} : tm m -> tm m -> Prop :=
| step_beta s t u :
    u = inst (t .: @var m) s -> step (app (lam s) t) u
| step_eta s t :
    s = inst (shift >> @var _) t -> step (lam (app s (var bound))) t
| step_appL s1 s2 t :
    step s1 s2 -> step (app s1 t) (app s2 t)
| step_appR s t1 t2 :
    step t1 t2 -> step (app s t1) (app s t2)
| step_lam s1 s2 :
    @step m.+1 s1 s2 -> step (lam s1) (lam s2).

Theorem substitutivity m n (sigma : subst m n) s t :
  step s t -> step (inst sigma s) (inst sigma t).
Proof.
  move=> st. elim: st n sigma => //={m s t}; eauto using @step.
  - move=> m s t u -> n f; apply: step_beta.
    rewrite !inst_comp. f_equal.
    fsimpl=>/=. f_equal. rewrite scomp_id_l. fext=> i /=.
    rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
  - move=> m s t -> n f; apply: step_eta.
    rewrite upi_def !inst_comp. fsimpl.
    rewrite scomp_id_l. by fsimpl.
Qed.