Library MetaCoq.Erasure.ESubstitution

Module PA := PCUICAst.
Module P := PCUICWcbvEval.

Lemma All2_All_mix_left {A B} {P : A → Type} {Q : A → B → Type}
      {l : list A} {l'}:
  All P l → All2 Q l l' → All2 (fun x y ⇒ (P x × Q x y)%type) l l'.

Lemma Is_type_extends (Σ : global_env_ext) Γ t :
  wf_local Σ Γ →
  ∀ (Σ' : global_env), wf Σ' → extends Σ Σ' → isErasable Σ Γ t → isErasable (Σ', Σ.2) Γ t.

Lemma Is_proof_extends (Σ : global_env_ext) Γ t :
  wf_local Σ Γ →
  ∀ Σ', wf Σ' → extends Σ Σ' → Is_proof Σ Γ t → Is_proof (Σ',Σ.2) Γ t.

Lemma Informative_extends:
  ∀ (Σ : global_env_ext) (ind : inductive)
    (mdecl : PCUICAst.mutual_inductive_body) (idecl : PCUICAst.one_inductive_body),

    PCUICTyping.declared_inductive (fst Σ) mdecl ind idecl →
    ∀ (Σ' : global_env) (u0 : universe_instance),
      wf Σ' →
      extends Σ Σ' →
      Informative Σ ind → Informative (Σ', Σ.2) ind.

Lemma erases_extends :
  env_prop (fun Σ Γ t T ⇒
              ∀ Σ', wf Σ' → extends Σ Σ' → ∀ t', erases Σ Γ t t' → erases (Σ', Σ.2) Γ t t').

Lemma Is_type_weakening:
  ∀ (Σ : global_env_ext) (Γ Γ' Γ'' : PCUICAst.context),
    wf_local Σ (Γ ,,, Γ') →
    wf Σ →
    wf_local Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') →
    ∀ t : PCUICAst.term,
      isErasable Σ (Γ ,,, Γ') t → isErasable Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') (PCUICLiftSubst.lift #|Γ''| #|Γ'| t).


Lemma erases_ctx_ext (Σ : global_env_ext) Γ Γ' t t' :
  erases Σ Γ t t' → Γ = Γ' → erases Σ Γ' t t'.

Lemma erases_weakening' (Σ : global_env_ext) (Γ Γ' Γ'' : PCUICAst.context) (t T : PCUICAst.term) t' :
    wf Σ →
    wf_local Σ (Γ ,,, Γ') →
    wf_local Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') →
    Σ ;;; Γ ,,, Γ' |- t : T →
    Σ ;;; Γ ,,, Γ' |- t ⇝ℇ t' →
    Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ' |- (PCUICLiftSubst.lift #|Γ''| #|Γ'| t) ⇝ℇ (lift #|Γ''| #|Γ'| t').

Lemma erases_weakening (Σ : global_env_ext) (Γ Γ' : PCUICAst.context) (t T : PCUICAst.term) t' :
  wf Σ →
  wf_local Σ (Γ ,,, Γ') →
  Σ ;;; Γ |- t : T →
  Σ ;;; Γ |- t ⇝ℇ t' →
  Σ ;;; Γ ,,, Γ' |- (PCUICLiftSubst.lift #|Γ'| 0 t) ⇝ℇ (lift #|Γ'| 0 t').

Lemma All2_nth_error_None {A B} {P : A → B → Type} {l l'} n :
  All2 P l l' →
  nth_error l n = None →
  nth_error l' n = None.

Lemma All2_length {A B} {P : A → B → Type} l l' : All2 P l l' → #|l| = #|l'|.


Lemma is_type_subst (Σ : global_env_ext) Γ Γ' Δ a s :
  wf Σ → subslet Σ Γ s Γ' →
  
  wf_local Σ (Γ ,,, subst_context s 0 Δ) →
  isErasable Σ (Γ ,,, Γ' ,,, Δ) a →
  isErasable Σ (Γ ,,, subst_context s 0 Δ) (PCUICLiftSubst.subst s #|Δ| a).

Lemma substlet_typable (Σ : global_env_ext) Γ s Γ' n t :
  subslet Σ Γ s Γ' → nth_error s n = Some t → {T & Σ ;;; Γ |- t : T}.

Lemma erases_eq (Σ : global_env_ext) Γ Γ' t t' s s' :
  erases Σ Γ t t' →
  Γ = Γ' →
  t = s →
  t' = s' →
  erases Σ Γ' s s'.

Lemma erases_subst (Σ : global_env_ext) Γ Γ' Δ t s t' s' T :
  wf Σ →
  subslet Σ Γ s Γ' →
  wf_local Σ (Γ ,,, subst_context s 0 Δ) →
  Σ ;;; Γ ,,, Γ' ,,, Δ |- t : T →
  Σ ;;; Γ ,,, Γ' ,,, Δ |- t ⇝ℇ t' →
  All2 (erases Σ Γ) s s' →
  Σ ;;; (Γ ,,, subst_context s 0 Δ) |- (PCUICLiftSubst.subst s #|Δ| t) ⇝ℇ subst s' #|Δ| t'.