Library MetaCoq.PCUIC.PCUICCSubst

From Coq Require Import CRelationClasses.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICLiftSubst
     PCUICUnivSubst PCUICTyping PCUICInduction PCUICReduction PCUICClosed.

Require Import ssreflect ssrbool.
From Equations Require Import Equations.

Closed single substitution:

no lifting involved and one term at a time.

Local Ltac inv H := inversion H; subst.

Fixpoint csubst t k u :=
  match u with
  | tRel n
     match k n with
    | Datatypes.Eqt
    | GttRel n
    | LttRel (Nat.pred n)
  | tEvar ev argstEvar ev ( (csubst t k) args)
  | tLambda na T MtLambda na (csubst t k T) (csubst t (S k) M)
  | tApp u vtApp (csubst t k u) (csubst t k v)
  | tProd na A BtProd na (csubst t k A) (csubst t (S k) B)
  | tLetIn na b ty b'tLetIn na (csubst t k b) (csubst t k ty) (csubst t (S k) b')
  | tCase ind p c brs
    let brs' := (fun brmap_branch_k (csubst t) id k br) brs in
    tCase ind (map_predicate_k id (csubst t) k p)
      (csubst t k c) brs'
  | tProj p ctProj p (csubst t k c)
  | tFix mfix idx
    let k' := List.length mfix + k in
    let mfix' := (map_def (csubst t k) (csubst t k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx
    let k' := List.length mfix + k in
    let mfix' := (map_def (csubst t k) (csubst t k')) mfix in
    tCoFix mfix' idx
  | xx

It is equivalent to general substitution when substituting a closed term
Lemma closed_subst t k u : closed t
    csubst t k u = subst [t] k u.
  revert k; induction u using term_forall_list_ind; intros k Hs;
    simpl; try f_equal; eauto with pcuic; solve_all.
  - destruct (PeanoNat.Nat.compare_spec k n).
    + subst k.
      rewrite PeanoNat.Nat.leb_refl Nat.sub_diag /=.
      now rewrite lift_closed.
    + destruct (leb_spec_Set k n); try lia.
      destruct (nth_error_spec [t] (n - k) ).
      simpl in l0; lia.
      now rewrite Nat.sub_1_r.
    + now destruct (Nat.leb_spec k n); try lia.

It respects closedness of the substitutend as well.
Lemma closed_csubst t k u : closed t closedn (S k) u closedn k (csubst t 0 u).
  rewrite closed_subst; auto.
  eapply closedn_subst0. simpl. erewrite closed_upwards; eauto. lia.
  simpl. now rewrite Nat.add_1_r.