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

Lemma isArity_subst_instance u T :
  isArity T →
  isArity (PCUICUnivSubst.subst_instance_constr u T).

Lemma is_prop_subst_instance:
  ∀ (u : universe_instance) (x0 : universe), is_prop_sort x0 → is_prop_sort (UnivSubst.subst_instance_univ u x0).

Lemma wf_ext_wk_wf {cf:checker_flags} Σ : wf_ext_wk Σ → wf Σ.


Lemma isErasable_subst_instance (Σ : global_env_ext) Γ T univs u :
  wf_ext_wk Σ → wf_local Σ Γ →
  wf_local (Σ.1, univs) (PCUICUnivSubst.subst_instance_context u Γ) →
  isErasable Σ Γ T →
  sub_context_set (monomorphic_udecl Σ.2) (global_ext_context_set (Σ.1, univs)) →
  consistent_instance_ext (Σ.1,univs) (Σ.2) u →
  isErasable (Σ.1,univs) (PCUICUnivSubst.subst_instance_context u Γ) (PCUICUnivSubst.subst_instance_constr u T).

Notation "Σ ;;; Γ |- s ▷ t" := (eval Σ Γ s t) (at level 50, Γ, s, t at next level) : type_scope.
Notation "Σ ⊢ s ▷ t" := (Ee.eval Σ s t) (at level 50, s, t at next level) : type_scope.

Lemma Is_type_conv_context (Σ : global_env_ext) (Γ : context) t (Γ' : context) :
  wf Σ → wf_local Σ Γ → wf_local Σ Γ' →
  PCUICContextConversion.conv_context Σ Γ Γ' → isErasable Σ Γ t → isErasable Σ Γ' t.

Lemma wf_local_rel_conv:
  ∀ Σ : global_env × universes_decl,
    wf Σ.1 →
    ∀ Γ Γ' : context,
      PCUICContextConversion.context_relation (PCUICContextConversion.conv_decls Σ) Γ Γ' →
      ∀ Γ0 : context, wf_local Σ Γ' → wf_local_rel Σ Γ Γ0 → wf_local_rel Σ Γ' Γ0.

Lemma erases_context_conversion :
env_prop
  (fun (Σ : PCUICAst.global_env_ext) (Γ : PCUICAst.context) (t T : PCUICAst.term) ⇒
      ∀ Γ' : PCUICAst.context,
        PCUICContextConversion.conv_context Σ Γ Γ' →
        wf_local Σ Γ' →
        ∀ t', erases Σ Γ t t' → erases Σ Γ' t t').

Lemma fix_context_subst_instance:
  ∀ (mfix : list (BasicAst.def term)) (u : universe_instance),
    map (map_decl (PCUICUnivSubst.subst_instance_constr u))
        (PCUICLiftSubst.fix_context mfix) =
    PCUICLiftSubst.fix_context
      (map
         (map_def (PCUICUnivSubst.subst_instance_constr u)
                  (PCUICUnivSubst.subst_instance_constr u)) mfix).

Lemma erases_subst_instance_constr0
  : env_prop (fun Σ Γ t T ⇒ wf_ext_wk Σ →
                           ∀ t' u univs,
                             wf_local (Σ.1, univs) (PCUICUnivSubst.subst_instance_context u Γ) →
sub_context_set (monomorphic_udecl Σ.2) (global_ext_context_set (Σ.1, univs)) →
      consistent_instance_ext (Σ.1,univs) (Σ.2) u →
    Σ ;;; Γ |- t ⇝ℇ t' →
    (Σ.1,univs) ;;; (PCUICUnivSubst.subst_instance_context u Γ) |- PCUICUnivSubst.subst_instance_constr u t ⇝ℇ t').

Lemma erases_subst_instance_constr :
  ∀ Σ : global_env_ext, wf_ext_wk Σ →
  ∀ Γ, wf_local Σ Γ →
  ∀ t T, Σ ;;; Γ |- t : T →
    ∀ t' u univs,
  wf_local (Σ.1, univs) (PCUICUnivSubst.subst_instance_context u Γ) →
sub_context_set (monomorphic_udecl Σ.2) (global_ext_context_set (Σ.1, univs)) → consistent_instance_ext (Σ.1,univs) (Σ.2) u →
    Σ ;;; Γ |- t ⇝ℇ t' →
    (Σ.1,univs) ;;; (PCUICUnivSubst.subst_instance_context u Γ) |- PCUICUnivSubst.subst_instance_constr u t ⇝ℇ t'.

Lemma erases_subst_instance'' Σ φ Γ t T u univs t' :
  wf_ext_wk (Σ, univs) →
  (Σ, univs) ;;; Γ |- t : T →
  sub_context_set (monomorphic_udecl univs) (global_context_set Σ) →
  consistent_instance_ext (Σ, φ) univs u →
  (Σ, univs) ;;; Γ |- t ⇝ℇ t' →
  (Σ, φ) ;;; subst_instance_context u Γ
            |- subst_instance_constr u t ⇝ℇ t'.

Lemma erases_subst_instance_decl Σ Γ t T c decl u t' :
  wf Σ.1 →
  lookup_env Σ.1 c = Some decl →
  (Σ.1, universes_decl_of_decl decl) ;;; Γ |- t : T →
  consistent_instance_ext Σ (universes_decl_of_decl decl) u →
  (Σ.1, universes_decl_of_decl decl) ;;; Γ |- t ⇝ℇ t' →
   Σ ;;; subst_instance_context u Γ
            |- subst_instance_constr u t ⇝ℇ t'.

Lemma erases_App (Σ : global_env_ext) Γ f L T t :
  Σ ;;; Γ |- tApp f L : T →
  erases Σ Γ (tApp f L) t →
  (t = tBox × squash (isErasable Σ Γ (tApp f L)))
  ∨ ∃ f' L', t = EAst.tApp f' L' ∧
             erases Σ Γ f f' ∧
             erases Σ Γ L L'.

Lemma erases_mkApps (Σ : global_env_ext) Γ f f' L L' :
  erases Σ Γ f f' →
  Forall2 (erases Σ Γ) L L' →
  erases Σ Γ (mkApps f L) (EAst.mkApps f' L').

Lemma erases_mkApps_inv (Σ : global_env_ext) Γ f L T t :
  wf Σ →
  Σ ;;; Γ |- mkApps f L : T →
  Σ;;; Γ |- mkApps f L ⇝ℇ t →
  (∃ L1 L2 L2', L = (L1 ++ L2)%list ∧
                squash (isErasable Σ Γ (mkApps f L1)) ∧
                erases Σ Γ (mkApps f L1) tBox ∧
                Forall2 (erases Σ Γ) L2 L2' ∧
                t = EAst.mkApps tBox L2'
  )
  ∨ ∃ f' L', t = EAst.mkApps f' L' ∧
             erases Σ Γ f f' ∧
             Forall2 (erases Σ Γ) L L'.

Lemma lookup_env_erases (Σ : global_env_ext) c decl Σ' :
  wf Σ →
  erases_global Σ Σ' →
  PCUICTyping.lookup_env (fst Σ) c = Some (ConstantDecl c decl) →
  ∃ decl', ETyping.lookup_env Σ' c = Some (EAst.ConstantDecl c decl') ∧
           erases_constant_body (Σ.1, cst_universes decl) decl decl'.

Record extraction_pre (Σ : global_env_ext) : Type
  := Build_extraction_pre
  { extr_env_axiom_free' : axiom_free (fst Σ);
    extr_env_wf' : wf_ext Σ }.


Definition EisConstruct_app :=
  fun t ⇒ match (EAstUtils.decompose_app t).1 with
        | E.tConstruct _ _ ⇒ true
        | _ ⇒ false
        end.

Lemma fst_decompose_app_rec t l : fst (EAstUtils.decompose_app_rec t l) = fst (EAstUtils.decompose_app t).

Lemma is_construct_erases Σ Γ t t' :
  Σ;;; Γ |- t ⇝ℇ t' →
  negb (isConstruct_app t) → negb (EisConstruct_app t').

Lemma is_FixApp_erases Σ Γ t t' :
  Σ;;; Γ |- t ⇝ℇ t' →
  negb (isFixApp t) → negb (Ee.isFixApp t').

Lemma erases_correct Σ t T t' v Σ' :
  extraction_pre Σ →
  Σ;;; [] |- t : T →
  Σ;;; [] |- t ⇝ℇ t' →
   erases_global Σ Σ' →
  Σ;;; [] |- t ▷ v →
  ∃ v', Σ;;; [] |- v ⇝ℇ v' ∧ Σ' ⊢ t' ▷ v'.