Library MetaCoq.PCUIC.TemplateToPCUICCorrectness

Module T := Template.Ast.
Module TTy := Checker.Typing.


Module TL := Template.LiftSubst.

Lemma mkApps_morphism (f : term → term) u v :
  (∀ x y, f (tApp x y) = tApp (f x) (f y)) →
  f (mkApps u v) = mkApps (f u) (List.map f v).


Lemma trans_lift n k t :
  trans (TL.lift n k t) = lift n k (trans t).

Lemma mkApps_app f l l' : mkApps f (l ++ l') = mkApps (mkApps f l) l'.

Lemma trans_mkApp u a : trans (T.mkApp u a) = tApp (trans u) (trans a).

Lemma trans_mkApps u v : T.wf u → List.Forall T.wf v →
  trans (T.mkApps u v) = mkApps (trans u) (List.map trans v).

Lemma trans_subst t k u : All T.wf t → T.wf u →
  trans (TL.subst t k u) = subst (map trans t) k (trans u).

Notation Tterm := Template.Ast.term.
Notation Tcontext := Template.Ast.context.

Lemma trans_subst_instance_constr u t : trans (Template.UnivSubst.subst_instance_constr u t) =
                                        subst_instance_constr u (trans t).


Lemma forall_decls_declared_constant Σ cst decl :
  TTy.declared_constant Σ cst decl →
  declared_constant (trans_global_decls Σ) cst (trans_constant_body decl).

Lemma forall_decls_declared_minductive Σ cst decl :
  TTy.declared_minductive Σ cst decl →
  declared_minductive (trans_global_decls Σ) cst (trans_minductive_body decl).

Lemma forall_decls_declared_inductive Σ mdecl ind decl :
  TTy.declared_inductive Σ mdecl ind decl →
  declared_inductive (trans_global_decls Σ) (trans_minductive_body mdecl) ind (trans_one_ind_body decl).

Lemma forall_decls_declared_constructor Σ cst mdecl idecl decl :
  TTy.declared_constructor Σ mdecl idecl cst decl →
  declared_constructor (trans_global_decls Σ) (trans_minductive_body mdecl) (trans_one_ind_body idecl)
                    cst ((fun '(x, y, z) ⇒ (x, trans y, z)) decl).

Lemma forall_decls_declared_projection Σ cst mdecl idecl decl :
  TTy.declared_projection Σ mdecl idecl cst decl →
  declared_projection (trans_global_decls Σ) (trans_minductive_body mdecl) (trans_one_ind_body idecl)
                    cst ((fun '(x, y) ⇒ (x, trans y)) decl).

Lemma destArity_mkApps ctx t l : l ≠ [] → destArity ctx (mkApps t l) = None.

Lemma trans_destArity ctx t :
  T.wf t →
  match TTy.destArity ctx t with
  | Some (args, s) ⇒
    destArity (trans_local ctx) (trans t) =
    Some (trans_local args, s)
  | None ⇒ True
  end.

Lemma Alli_map_option_out_mapi_Some_spec {A B B'} (f : nat → A → option B) (g' : B → B')
      (g : nat → A → option B') P l t :
  Alli P 0 l →
  (∀ i x t, P i x → f i x = Some t → g i x = Some (g' t)) →
  map_option_out (mapi f l) = Some t →
  map_option_out (mapi g l) = Some (map g' t).

Definition on_pair {A B C D} (f : A → B) (g : C → D) (x : A × C) :=
  (f (fst x), g (snd x)).

Lemma trans_inds kn u bodies : map trans (TTy.inds kn u bodies) = inds kn u (map trans_one_ind_body bodies).

Lemma trans_instantiate_params_subst params args s t :
  All TypingWf.wf_decl params → All Ast.wf s →
  All Ast.wf args →
  ∀ s' t',
    TTy.instantiate_params_subst params args s t = Some (s', t') →
    instantiate_params_subst (map trans_decl params)
                             (map trans args) (map trans s) (trans t) =
    Some (map trans s', trans t').

Lemma trans_instantiate_params params args t :
  T.wf t →
  All TypingWf.wf_decl params →
  All Ast.wf args →
  ∀ t',
    TTy.instantiate_params params args t = Some t' →
    instantiate_params (map trans_decl params) (map trans args) (trans t) =
    Some (trans t').

Lemma trans_it_mkProd_or_LetIn ctx t :
  trans (Template.AstUtils.it_mkProd_or_LetIn ctx t) =
  it_mkProd_or_LetIn (map trans_decl ctx) (trans t).

Lemma trans_types_of_case (Σ : T.global_env) ind mdecl idecl args p u pty indctx pctx ps btys :
  T.wf p → T.wf pty → T.wf (T.ind_type idecl) →
  All Ast.wf args →
  TTy.wf Σ →
  TTy.declared_inductive Σ mdecl ind idecl →
  TTy.types_of_case ind mdecl idecl args u p pty = Some (indctx, pctx, ps, btys) →
  types_of_case ind (trans_minductive_body mdecl) (trans_one_ind_body idecl)
  (map trans args) u (trans p) (trans pty) =
  Some (trans_local indctx, trans_local pctx, ps, map (on_snd trans) btys).



Lemma mkApps_trans_wf U l : T.wf (T.tApp U l) → ∃ U' V', trans (T.tApp U l) = tApp U' V'.

Lemma trans_eq_term ϕ T U :
  T.wf T → T.wf U → TTy.eq_term ϕ T U →
  eq_term ϕ (trans T) (trans U).

Lemma trans_eq_term_list ϕ T U :
  List.Forall T.wf T → List.Forall T.wf U → Forall2 (TTy.eq_term ϕ) T U →
  All2 (eq_term ϕ) (List.map trans T) (List.map trans U).

Lemma leq_term_mkApps ϕ t u t' u' :
  eq_term ϕ t t' → All2 (eq_term ϕ) u u' →
  leq_term ϕ (mkApps t u) (mkApps t' u').

Lemma eq_term_upto_univ_App `{checker_flags} Re Rle f f' :
  eq_term_upto_univ Re Rle f f' →
  isApp f = isApp f'.

Lemma eq_term_upto_univ_mkApps `{checker_flags} Re Rle f l f' l' :
  eq_term_upto_univ Re Rle f f' →
  All2 (eq_term_upto_univ Re Re) l l' →
  eq_term_upto_univ Re Rle (mkApps f l) (mkApps f' l').

Lemma trans_eq_term_upto_univ Re Rle T U :
  T.wf T → T.wf U → TTy.eq_term_upto_univ Re Rle T U →
  eq_term_upto_univ Re Rle (trans T) (trans U).

Lemma trans_leq_term ϕ T U :
  T.wf T → T.wf U → TTy.leq_term ϕ T U →
  leq_term ϕ (trans T) (trans U).


Lemma trans_nth n l x : trans (nth n l x) = nth n (List.map trans l) (trans x).

Lemma trans_iota_red pars ind c u args brs :
  T.wf (Template.Ast.mkApps (Template.Ast.tConstruct ind c u) args) →
  List.Forall (compose T.wf snd) brs →
  trans (TTy.iota_red pars c args brs) =
  iota_red pars c (List.map trans args) (List.map (on_snd trans) brs).

Lemma trans_unfold_fix mfix idx narg fn :
  List.Forall (fun def : def Tterm ⇒ T.wf (dtype def) ∧ T.wf (dbody def) ∧
              T.isLambda (dbody def) = true) mfix →
  TTy.unfold_fix mfix idx = Some (narg, fn) →
  unfold_fix (map (map_def trans trans) mfix) idx = Some (narg, trans fn).

Lemma trans_unfold_cofix mfix idx narg fn :
  List.Forall (fun def : def Tterm ⇒ T.wf (dtype def) ∧ T.wf (dbody def)) mfix →
  TTy.unfold_cofix mfix idx = Some (narg, fn) →
  unfold_cofix (map (map_def trans trans) mfix) idx = Some (narg, trans fn).

Definition isApp t := match t with tApp _ _ ⇒ true | _ ⇒ false end.

Lemma trans_is_constructor:
  ∀ (args : list Tterm) (narg : nat),
    Checker.Typing.is_constructor narg args = true → is_constructor narg (map trans args) = true.

Lemma refine_red1_r Σ Γ t u u' : u = u' → red1 Σ Γ t u → red1 Σ Γ t u'.

Lemma refine_red1_Γ Σ Γ Γ' t u : Γ = Γ' → red1 Σ Γ t u → red1 Σ Γ' t u.

Lemma trans_red1 Σ Γ T U :
  TTy.on_global_env (fun Σ ⇒ wf_decl_pred) Σ →
  List.Forall wf_decl Γ →
  T.wf T → TTy.red1 Σ Γ T U →
  red1 (map trans_global_decl Σ) (trans_local Γ) (trans T) (trans U).

Lemma global_ext_levels_trans Σ
  : global_ext_levels (trans_global Σ) = TTy.global_ext_levels Σ.

Lemma global_ext_constraints_trans Σ
  : global_ext_constraints (trans_global Σ) = TTy.global_ext_constraints Σ.

Lemma trans_cumul (Σ : Ast.global_env_ext) Γ T U :
  TTy.on_global_env (fun Σ ⇒ wf_decl_pred) Σ →
  List.Forall wf_decl Γ →
  T.wf T → T.wf U → TTy.cumul Σ Γ T U →
  trans_global Σ ;;; trans_local Γ |- trans T ≤ trans U.

Definition Tlift_typing (P : Template.Ast.global_env_ext → Tcontext → Tterm → Tterm → Type) :=
  fun Σ Γ t T ⇒
    match T with
    | Some T ⇒ P Σ Γ t T
    | None ⇒ { s : universe & P Σ Γ t (T.tSort s) }
    end.

Lemma trans_wf_local:
  ∀ (Σ : Template.Ast.global_env_ext) (Γ : Tcontext) (wfΓ : TTy.wf_local Σ Γ),
    let P :=
        (fun Σ0 (Γ0 : Tcontext) _ (t T : Tterm) _ ⇒
           trans_global Σ0;;; trans_local Γ0 |- trans t : trans T)
    in
    TTy.All_local_env_over TTy.typing P Σ Γ wfΓ →
    wf_local (trans_global Σ) (trans_local Γ).

Lemma trans_wf_local_env Σ Γ :
  TTy.All_local_env
        (TTy.lift_typing
           (fun (Σ : Ast.global_env_ext) (Γ : Tcontext) (b ty : Tterm) ⇒
              TTy.typing Σ Γ b ty × trans_global Σ;;; trans_local Γ |- trans b : trans ty) Σ)
        Γ →
  wf_local (trans_global Σ) (trans_local Γ).

Lemma typing_wf_wf:
  ∀ (Σ : Template.Ast.global_env_ext),
    TTy.wf Σ →
    TTy.Forall_decls_typing
      (fun (_ : Template.Ast.global_env_ext) (_ : Tcontext) (t T : Tterm) ⇒ Ast.wf t ∧ Ast.wf T) Σ.



Lemma check_correct_arity_trans (Σ : T.global_env_ext) idecl ind u indctx npar args pctx :
  TTy.check_correct_arity (TTy.global_ext_constraints Σ) idecl ind u indctx (firstn npar args) pctx →
  check_correct_arity (global_ext_constraints (trans_global Σ)) (trans_one_ind_body idecl) ind u
                      (trans_local indctx) (firstn npar (map trans args))
                      (trans_local pctx).

Axiom fix_guard_trans :
  ∀ mfix,
    TTy.fix_guard mfix →
    fix_guard (map (map_def trans trans) mfix).

Lemma isWFArity_wf (Σ : Ast.global_env_ext) Γ T : Typing.wf Σ → TTy.isWfArity TTy.typing Σ Γ T → T.wf T.

Theorem template_to_pcuic (Σ : T.global_env_ext) Γ t T :
  TTy.wf Σ → TTy.typing Σ Γ t T →
  typing (trans_global Σ) (trans_local Γ) (trans t) (trans T).