Library MetaCoq.Erasure.ECSubst

From Coq Require Import Program.
From MetaCoq.Template Require Import utils.
From MetaCoq.Erasure Require Import EAst EAstUtils EInduction ELiftSubst.

Require Import ssreflect ssrbool.
From Equations Require Import Equations.

Local Ltac inv H := inversion H; subst.

Fixpoint csubst t k u :=
  match u with
  | tBox ⇒ tBox
  | tRel n ⇒
     match Nat.compare k n with
    | Datatypes.Eq ⇒ t
    | Gt ⇒ tRel n
    | Lt ⇒ tRel (Nat.pred n)
    end
  | tEvar ev args ⇒ tEvar ev (List.map (csubst t k) args)
  | tLambda na M ⇒ tLambda na (csubst t (S k) M)
  | tApp u v ⇒ tApp (csubst t k u) (csubst t k v)
  | tLetIn na b b' ⇒ tLetIn na (csubst t k b) (csubst t (S k) b')
  | tCase ind c brs ⇒
    let brs' := List.map (fun br ⇒ (br.1, csubst t (#|br.1| + k) br.2)) brs in
    tCase ind (csubst t k c) brs'
  | tProj p c ⇒ tProj p (csubst t k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (csubst t k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (csubst t k')) mfix in
    tCoFix mfix' idx
  | tConstruct ind n args ⇒ tConstruct ind n (map (csubst t k) args)
  | x ⇒ x
  end.

Definition substl defs body : term :=
  fold_left (fun bod term ⇒ csubst term 0 bod)
    defs body.

Lemma closed_subst t k u : closed t →
    csubst t k u = subst [t] k u.
Proof.
  revert k; induction u using term_forall_list_ind; intros k Hs;
    simpl; try f_equal; eauto; 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.
Qed.

Lemma substl_subst s u : forallb (closedn 0) s →
  substl s u = subst s 0 u.
Proof.
  unfold substl.
  induction s in u |- *; cbn; intros H.
  - now rewrite subst_empty.
  - move/andP: H ⇒ [cla cls]. rewrite IHs; try eassumption.
    rewrite closed_subst; try eassumption.
    change (a :: s) with ([a] ++ s).
    rewrite subst_app_decomp. cbn.
    repeat f_equal. rewrite lift_closed; eauto.
Qed.


Lemma closed_csubst t k u :
  closed t →
  closedn (S k) u →
  closedn k (ECSubst.csubst t 0 u).
Proof.
  intros.
  rewrite ECSubst.closed_subst //.
  eapply closedn_subst ⇒ /= //.
  rewrite andb_true_r. eapply closed_upwards; tea. lia.
Qed.

Lemma closed_substl ts k u :
  forallb (closedn 0) ts →
  closedn (#|ts| + k) u →
  closedn k (ECSubst.substl ts u).
Proof.
  induction ts in u |- *; cbn ⇒ //.
  move/andP⇒ [] cla clts.
  intros clu. eapply IHts ⇒ //.
  eapply closed_csubst ⇒ //.
Qed.

Lemma csubst_mkApps {a k f l} : csubst a k (mkApps f l) = mkApps (csubst a k f) (map (csubst a k) l).
Proof.
  induction l using rev_ind; simpl; auto.
  rewrite mkApps_app /= IHl.
  now rewrite -[EAst.tApp _ _](mkApps_app _ _ [_]) map_app.
Qed.

Lemma csubst_closed t k x : closedn k x → csubst t k x = x.
Proof.
  induction x in k |- × using EInduction.term_forall_list_ind; simpl; auto.
  all:try solve [intros; f_equal; solve_all; eauto].
  intros Hn. eapply Nat.ltb_lt in Hn.
  - destruct (Nat.compare_spec k n); try lia. reflexivity.
  - move/andP ⇒ []. intros. f_equal; solve_all; eauto.
  - move/andP ⇒ []. intros. f_equal; solve_all; eauto.
  - move/andP ⇒ []. intros. f_equal; solve_all; eauto.
    destruct x0; cbn in ×. f_equal; auto.
Qed.

Lemma subst_csubst_comm l t k b :
  forallb (closedn 0) l → closed t →
  subst l 0 (csubst t (#|l| + k) b) =
  csubst t k (subst l 0 b).
Proof.
  intros hl cl.
  rewrite !closed_subst //.
  rewrite distr_subst. f_equal.
  symmetry. solve_all.
  rewrite subst_closed //.
  eapply closed_upwards; tea. lia.
Qed.

Lemma substl_csubst_comm l t k b :
  forallb (closedn 0) l → closed t →
  substl l (csubst t (#|l| + k) b) =
  csubst t k (substl l b).
Proof.
  intros hl cl.
  rewrite substl_subst //.
  rewrite substl_subst //.
  apply subst_csubst_comm ⇒ //.
Qed.

Lemma isLambda_csubst a k t : isLambda t → isLambda (csubst a k t).
Proof. destruct t ⇒ //. Qed.
Lemma isBox_csubst a k t : isBox t → isBox (csubst a k t).
Proof. destruct t ⇒ //. Qed.