Library MetaCoq.Erasure.ECSubst

(* Distributed under the terms of the MIT license. *)
From Coq Require Import Program.
From MetaCoq.Utils 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 closedn_subst s k k' t :
  forallb (closedn k) s -> closedn (k + k' + |s|) t -> closedn (k + k') (subst s k' t). Proof. intros Hs. solve_all. revert H. induction t in k' |- * using term_forall_list_ind; intros; simpl in *; rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; simpl closed in *; try change_Sk; repeat (rtoProp; solve_all); unfold compose, test_def, on_snd, test_snd in *; simpl in *; eauto with all. - elim (Nat.leb_spec k' n); intros. simpl. apply Nat.ltb_lt in H. destruct nth_error eqn:Heq. -- eapply closedn_lift. now eapply nth_error_all in Heq; simpl; eauto; simpl in *. -- simpl. elim (Nat.ltb_spec); auto. intros. apply nth_error_None in Heq. lia. -- simpl. apply Nat.ltb_lt in H0. apply Nat.ltb_lt. apply Nat.ltb_lt in H0. lia. - specialize (IHt2 (S k')). rewrite <- Nat.add_succ_comm in IHt2. eauto. - specialize (IHt2 (S k')). rewrite <- Nat.add_succ_comm in IHt2. eauto. - specialize (IHt3 (S k')). rewrite <- Nat.add_succ_comm in IHt3. eauto. - rtoProp; solve_all. rewrite -> !Nat.add_assoc in *. specialize (b0 (|m| + k')). unfold is_true. rewrite <- b0. f_equal. lia.
    unfold is_true. rewrite <- H0. f_equal. lia.
  - rtoProp; solve_all. rewrite -> !Nat.add_assoc in *.
    specialize (b0 (|m| + k')). unfold is_true. rewrite <- b0. f_equal. lia. unfold is_true. rewrite <- H0. f_equal. lia. Qed. Lemma closedn_subst0 s k t : forallb (closedn k) s -> closedn (k + |s|) t ->
  closedn k (subst0 s t).
Proof.
  intros.
  generalize (closedn_subst s k 0 t H).
  rewrite Nat.add_0_r. eauto.
Qed.



Lemma closed_csubst t k u : closed t -> closedn (S k) u -> closedn k (csubst t 0 u).
Proof.
  intros.
  rewrite closed_subst; auto.
  eapply closedn_subst0. simpl. erewrite closed_upwards; eauto. lia.
  simpl. now rewrite Nat.add_1_r.
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.