Library MetaCoq.PCUIC.Typing.PCUICNamelessTyp

From Coq Require Import RelationClasses.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction
     PCUICLiftSubst PCUICEquality PCUICReduction PCUICTyping PCUICPosition PCUICUnivSubst
     PCUICNamelessDef PCUICGuardCondition PCUICNamelessConv PCUICConversion
     PCUICWellScopedCumulativity PCUICOnFreeVars PCUICOnFreeVarsConv PCUICConfluence PCUICClosedTyp PCUICClosed
     PCUICSigmaCalculus .
Require Import Equations.Prop.DepElim.
Require Import ssreflect ssrbool.

Implicit Types cf : checker_flags.

Typing does not rely on name annotations of binders.

We prove this by constructing a type-preserving translation to terms where all binders are anonymous. An alternative would be to be parametrically polymorphic everywhere on the binder name type. This would allow to add implicit information too.

Local Set Keyed Unification.

Set Default Goal Selector "!".

Lemma nlg_wf_local {cf : checker_flags} :
  ∀ Σ Γ (hΓ : wf_local Σ Γ),
    All_local_env_over
      typing
      (fun Σ Γ (_ : wf_local Σ Γ) (t T : term) (_ : Σ ;;; Γ |- t : T) ⇒
         nlg Σ ;;; nlctx Γ |- nl t : nl T)
      Σ Γ hΓ →
    wf_local (nlg Σ ) (nlctx Γ ).
Proof.
  intros Σ Γ hΓ h.
  induction h.
  - constructor.
  - simpl. unfold map_decl_anon. cbn. constructor. 1: assumption.
    apply infer_typing_sort_impl with id tu; intros Hty.
    exact Hs.
  - simpl. unfold map_decl_anon. cbn. constructor.
    + assumption.
    + apply infer_typing_sort_impl with id tu; intros Hty. exact Hs.
    + assumption.
Qed.

Lemma nl_check_one_fix d : check_one_fix d = check_one_fix (map_def_anon nl nl d).
Proof.
  destruct d; simpl.
  rewrite (nl_decompose_prod_assum [] dtype).
  destruct decompose_prod_assum.
  rewrite -(nlctx_smash_context []) -map_rev nth_error_map.
  destruct nth_error ⇒ //. cbn.
  rewrite [decompose_app_rec _ _]nl_decompose_app.
  destruct decompose_app ⇒ //.
  destruct t0 ⇒ //.
Qed.

Lemma nl_wf_fixpoint Σ mfix :
  wf_fixpoint Σ .1 mfix = wf_fixpoint (nlg Σ) (map (map_def_anon nl nl) mfix).
Proof.
  unfold wf_fixpoint, wf_fixpoint_gen.
  f_equal.
  { rewrite forallb_map. eapply forallb_ext ⇒ x. cbn. destruct (dbody x) ⇒ //. }
  replace (map check_one_fix mfix) with (map check_one_fix (map (map_def_anon nl nl) mfix)) ⇒ //.
  × destruct map_option_out ⇒ //. destruct l ⇒ //.
    f_equal. rewrite /check_recursivity_kind.
    epose proof (nl_lookup_env Σ.1).
    destruct Σ; cbn in ×. rewrite H.
    destruct lookup_env ⇒ //. cbn.
    destruct g0 ⇒ //.
  × rewrite map_map_compose.
    now setoid_rewrite <-nl_check_one_fix.
Qed.

Lemma nl_check_one_cofix d : check_one_cofix d = check_one_cofix (map_def_anon nl nl d).
Proof.
  destruct d; simpl.
  rewrite (nl_decompose_prod_assum [] dtype).
  destruct decompose_prod_assum.
  rewrite nl_decompose_app.
  destruct decompose_app ⇒ //.
  destruct t0 ⇒ //.
Qed.

Lemma nl_wf_cofixpoint Σ mfix :
  wf_cofixpoint Σ .1 mfix = wf_cofixpoint (nlg Σ) (map (map_def_anon nl nl) mfix).
Proof.
  unfold wf_cofixpoint, wf_cofixpoint_gen.
  replace (map check_one_cofix mfix) with (map check_one_cofix (map (map_def_anon nl nl) mfix)) ⇒ //.
  × destruct map_option_out ⇒ //. destruct l ⇒ //.
    f_equal. rewrite /check_recursivity_kind.
    epose proof (nl_lookup_env Σ.1).
    destruct Σ; cbn in ×. rewrite H.
    destruct lookup_env ⇒ //. cbn.
    destruct g0 ⇒ //.
  × rewrite map_map_compose.
    now setoid_rewrite <- nl_check_one_cofix.
Qed.

Lemma wf_universe_nl Σ u : wf_universe Σ u → wf_universe (nlg Σ) u.
Proof.
  destruct u; simpl; auto.
  intros.
  now rewrite nl_global_ext_levels.
Qed.