linear.v

Require Import List.
Import ListNotations.
Require Import Bool.
Require Import PeanoNat.
Require Import Lia.

Definition Index := nat.
Definition Level := nat.

Inductive Term :=
  | T_var : forall (n : Index), Term
  | T_apply : forall (funct : Term) (arg : Term), Term
  | T_lambda : forall (body : Term), Term.

Fixpoint shift by_ depth term :=
  match term with
  | T_var var => 
    match Nat.ltb var depth with
    | true => T_var var
    | false => T_var (by_ + var)
    end
  | T_apply funct arg =>
    let funct := shift by_ depth funct in
    let arg := shift by_ depth arg in
    T_apply funct arg
  | T_lambda body => 
    let body := shift by_ (1 + depth) body in
    T_lambda body
  end.
Fixpoint subst to_ depth term  :=
  match term with
  | T_var var => 
    match Nat.compare var depth with
    | Lt => T_var var
    | Eq => shift depth 0 to_
    | Gt => T_var (pred var)
    end
  | T_apply funct arg =>
    let funct := subst to_ depth funct in
    let arg := subst to_ depth arg in
    T_apply funct arg
  | T_lambda body => 
    let body := subst to_ (1 + depth) body in
    T_lambda body
  end.

Fixpoint count var term :=
  match term with
  | T_var n =>
    match Nat.eqb n var with
    | true => 1
    | false => 0
    end
  | T_apply funct arg =>
    count var funct + count var arg
  | T_lambda body => count (1 + var) body
  end.

Fixpoint size term :=
  match term with
  | T_var _ => 0
  | T_apply funct arg => size funct + size arg
  | T_lambda body => 1 + size body
  end.

Lemma shift_preserves_size term by_
  : forall depth, size (shift by_ depth term) = size term.
  induction term; intuition.
  -
    simpl; destruct (n <? depth); reflexivity.
  -
    rename term1 into lam; rename IHterm1 into IHlam.
    rename term2 into arg; rename IHterm2 into IHarg.
    specialize (IHlam depth); specialize (IHarg depth).
    simpl; rewrite IHlam, IHarg.
    reflexivity.
  -
    rename term into body; rename IHterm into IHbody.
    specialize (IHbody (1 + depth)).
    simpl in *; rewrite IHbody.
    reflexivity.
Defined.

Lemma subst_preserves_size term to_
  : forall depth, size (subst to_ depth term) =
    size term + (size to_ * count depth term).
  induction term; intuition.
  -
    simpl.
    destruct (Nat.compare_spec n depth); simpl.
    rewrite shift_preserves_size.
    rewrite H; rewrite (Nat.eqb_refl depth); lia.
    destruct (Nat.eqb_spec n depth); lia.
    destruct (Nat.eqb_spec n depth); lia.
  -
    rename term1 into lam; rename IHterm1 into IHlam.
    rename term2 into arg; rename IHterm2 into IHarg.
    specialize (IHlam depth); specialize (IHarg depth).
    simpl; rewrite IHlam, IHarg; lia.
  -
    rename term into body; rename IHterm into IHbody.
    specialize (IHbody (1 + depth)).
    simpl in *; rewrite IHbody; reflexivity.
Qed.

Unset Automatic Proposition Inductives.

Inductive Step : Term -> Term -> Type :=
  | ST_beta : forall body arg (H : count 0 body = 1),
    Step (T_apply (T_lambda body) arg) (subst arg 0 body)
  | ST_app_funct : forall funct funct' arg, Step funct funct' ->
    Step (T_apply funct arg) (T_apply funct' arg)
  | ST_app_arg : forall funct arg arg', Step arg arg' ->
    Step (T_apply funct arg) (T_apply funct arg')
  | ST_lambda : forall body body', Step body body' ->
    Step (T_lambda body) (T_lambda body').

Lemma step_preserve_size term term' (step : Step term term')
  : 1 + size term' = size term.
  induction step; simpl; first [ lia | idtac ].
  rewrite subst_preserves_size; lia.
Defined.