Library MetaCoq.PCUIC.PCUICNameless

Definition anon (na : name) : bool :=
  match na with
  | nAnon ⇒ true
  | nNamed s ⇒ false
  end.

Fixpoint nameless (t : term) : bool :=
  match t with
  | tRel n ⇒ true
  | tVar n ⇒ true
  | tEvar n l ⇒ forallb nameless l
  | tSort s ⇒ true
  | tProd na A B ⇒ anon na && nameless A && nameless B
  | tLambda na A b ⇒ anon na && nameless A && nameless b
  | tLetIn na b B t ⇒ anon na && nameless b && nameless B && nameless t
  | tApp u v ⇒ nameless u && nameless v
  | tConst c u ⇒ true
  | tInd i u ⇒ true
  | tConstruct i n u ⇒ true
  | tCase indn p c brs ⇒
    nameless p && nameless c && forallb (test_snd nameless) brs
  | tProj p c ⇒ nameless c
  | tFix mfix idx ⇒
    forallb (fun d ⇒ anon d.(dname)) mfix &&
    forallb (test_def nameless nameless) mfix
  | tCoFix mfix idx ⇒
    forallb (fun d ⇒ anon d.(dname)) mfix &&
    forallb (test_def nameless nameless) mfix
  end.

Definition map_def_anon {A B : Set} (tyf bodyf : A → B) (d : def A) := {|
  dname := nAnon ;
  dtype := tyf d.(dtype) ;
  dbody := bodyf d.(dbody) ;
  rarg := d.(rarg)
|}.

Fixpoint nl (t : term) : term :=
  match t with
  | tRel n ⇒ tRel n
  | tVar n ⇒ tVar n
  | tEvar n l ⇒ tEvar n (map nl l)
  | tSort s ⇒ tSort s
  | tProd na A B ⇒ tProd nAnon (nl A) (nl B)
  | tLambda na A b ⇒ tLambda nAnon (nl A) (nl b)
  | tLetIn na b B t ⇒ tLetIn nAnon (nl b) (nl B) (nl t)
  | tApp u v ⇒ tApp (nl u) (nl v)
  | tConst c u ⇒ tConst c u
  | tInd i u ⇒ tInd i u
  | tConstruct i n u ⇒ tConstruct i n u
  | tCase indn p c brs ⇒ tCase indn (nl p) (nl c) (map (on_snd nl) brs)
  | tProj p c ⇒ tProj p (nl c)
  | tFix mfix idx ⇒ tFix (map (map_def_anon nl nl) mfix) idx
  | tCoFix mfix idx ⇒ tCoFix (map (map_def_anon nl nl) mfix) idx
  end.





Lemma eq_univ_make :
  ∀ u u',
    Forall2 eq (map Universe.make u) (map Universe.make u') →
    u = u'.

Lemma nameless_eq_term_spec :
  ∀ u v,
    nameless u →
    nameless v →
    eq_term_upto_univ eq eq u v →
    u = v.

Lemma nl_spec :
  ∀ u, nameless (nl u).

Lemma nl_eq_term_upto_univ :
  ∀ Re Rle t t',
    eq_term_upto_univ Re Rle t t' →
    eq_term_upto_univ Re Rle (nl t) (nl t').

Lemma nl_leq_term {cf:checker_flags} :
  ∀ φ t t',
    leq_term φ t t' →
    leq_term φ (nl t) (nl t').

Lemma nl_eq_term {cf:checker_flags} :
  ∀ φ t t',
    eq_term φ t t' →
    eq_term φ (nl t) (nl t').

Corollary eq_term_nl_eq :
  ∀ u v,
    eq_term_upto_univ eq eq u v →
    nl u = nl v.


Lemma eq_term_upto_univ_nl_inv :
  ∀ Re Rle u v,
    eq_term_upto_univ Re Rle (nl u) (nl v) →
    eq_term_upto_univ Re Rle u v.

Definition map_decl_anon f (d : context_decl) := {|
  decl_name := nAnon ;
  decl_body := option_map f d.(decl_body) ;
  decl_type := f d.(decl_type)
|}.

Definition nlctx (Γ : context) : context :=
  map (map_decl_anon nl) Γ.

Definition test_option {A} f (o : option A) : bool :=
  match o with
  | None ⇒ true
  | Some x ⇒ f x
  end.

Definition nameless_ctx (Γ : context) : bool :=
  forallb (fun d ⇒
    anon d.(decl_name) &&
    test_option nameless d.(decl_body) &&
    nameless d.(decl_type)
  ) Γ.

Lemma nlctx_spec :
  ∀ Γ, nameless_ctx (nlctx Γ).

Lemma eq_term_upto_univ_tm_nl :
  ∀ Re Rle u,
    Reflexive Re →
    Reflexive Rle →
    eq_term_upto_univ Re Rle u (nl u).

Corollary eq_term_tm_nl :
  ∀ `{checker_flags} G u, eq_term G u (nl u).

Definition nl_constant_body c :=
  Build_constant_body
    (nl c.(cst_type)) (option_map nl c.(cst_body)) c.(cst_universes).

Definition nl_one_inductive_body o :=
  Build_one_inductive_body
    o.(ind_name)
    (nl o.(ind_type))
    o.(ind_kelim)
    (map (fun '((x,y),n) ⇒ ((x, nl y), n)) o.(ind_ctors))
    (map (fun '(x,y) ⇒ (x, nl y)) o.(ind_projs)).

Definition nl_mutual_inductive_body m :=
  Build_mutual_inductive_body
    m.(ind_finite)
    m.(ind_npars)
    (nlctx m.(ind_params))
    (map nl_one_inductive_body m.(ind_bodies))
    m.(ind_universes).

Definition nl_global_decl (d : global_decl) : global_decl :=
  match d with
  | ConstantDecl kn cb ⇒ ConstantDecl kn (nl_constant_body cb)
  | InductiveDecl kn mib ⇒ InductiveDecl kn (nl_mutual_inductive_body mib)
  end.

Definition nlg (Σ : global_env_ext) : global_env_ext :=
  let '(Σ, φ) := Σ in
  (map nl_global_decl Σ, φ).

Fixpoint nlstack (π : stack) : stack :=
  match π with
  | ε ⇒ ε
  | App u ρ ⇒
    App (nl u) (nlstack ρ)
  | Fix f n args ρ ⇒
    Fix (map (map_def_anon nl nl) f) n (map nl args) (nlstack ρ)
  | CoFix f n args ρ ⇒
    CoFix (map (map_def_anon nl nl) f) n (map nl args) (nlstack ρ)
  | Case indn p brs ρ ⇒
    Case indn (nl p) (map (on_snd nl) brs) (nlstack ρ)
  | Proj p ρ ⇒
    Proj p (nlstack ρ)
  | Prod_l na B ρ ⇒
    Prod_l nAnon (nl B) (nlstack ρ)
  | Prod_r na A ρ ⇒
    Prod_r nAnon (nl A) (nlstack ρ)
  | Lambda_ty na b ρ ⇒
    Lambda_ty nAnon (nl b) (nlstack ρ)
  | Lambda_tm na A ρ ⇒
    Lambda_tm nAnon (nl A) (nlstack ρ)
  | coApp t ρ ⇒
    coApp (nl t) (nlstack ρ)
  end.

Lemma nlstack_appstack :
  ∀ args ρ,
    nlstack (appstack args ρ) = appstack (map nl args) (nlstack ρ).

Lemma nlstack_cat :
  ∀ ρ θ,
    nlstack (ρ +++ θ) = nlstack ρ +++ nlstack θ.

Lemma stack_position_nlstack :
  ∀ ρ,
    stack_position (nlstack ρ) = stack_position ρ.

Lemma nl_it_mkLambda_or_LetIn :
  ∀ Γ t,
    nl (it_mkLambda_or_LetIn Γ t) =
    it_mkLambda_or_LetIn (nlctx Γ) (nl t).

Lemma nl_mkApps :
  ∀ t l,
    nl (mkApps t l) = mkApps (nl t) (map nl l).

Lemma nlctx_app_context :
  ∀ Γ Δ,
    nlctx (Γ ,,, Δ) = nlctx Γ ,,, nlctx Δ.

Lemma nlctx_stack_context :
  ∀ ρ,
    nlctx (stack_context ρ) = stack_context (nlstack ρ).

Lemma nl_subst_instance_constr :
  ∀ u b,
    nl (subst_instance_constr u b) = subst_instance_constr u (nl b).

Lemma context_position_nlctx :
  ∀ Γ,
    context_position (nlctx Γ) = context_position Γ.

Lemma xposition_nlctx :
  ∀ Γ π,
    xposition (nlctx Γ) π = xposition Γ π.

Lemma xposition_nlstack :
  ∀ Γ π,
    xposition Γ (nlstack π) = xposition Γ π.

Lemma nl_zipc :
  ∀ t π,
    nl (zipc t π) = zipc (nl t) (nlstack π).

Lemma nl_zipx :
  ∀ Γ t π,
    nl (zipx Γ t π) = zipx (nlctx Γ) (nl t) (nlstack π).

Lemma global_ext_levels_nlg :
  ∀ Σ,
    global_ext_levels (nlg Σ) = global_ext_levels Σ.

Lemma global_ext_constraints_nlg :
  ∀ Σ,
    global_ext_constraints (nlg Σ) = global_ext_constraints Σ.

Lemma nl_lookup_env :
  ∀ Σ c,
    lookup_env (map nl_global_decl Σ) c
    = option_map nl_global_decl (lookup_env Σ c).

Lemma lookup_env_nlg :
  ∀ Σ c decl,
    lookup_env Σ.1 c = Some decl →
    lookup_env (nlg Σ) c = Some (nl_global_decl decl).

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 Γ).

Lemma nl_lift :
  ∀ n k t,
    nl (lift n k t) = lift n k (nl t).

Lemma nl_subst :
  ∀ s k u,
    nl (subst s k u) = subst (map nl s) k (nl u).

Lemma nl_eq_decl {cf:checker_flags} :
  ∀ φ d d',
    eq_decl φ d d' →
    eq_decl φ (map_decl nl d) (map_decl nl d').

Lemma nl_eq_decl' {cf:checker_flags} :
  ∀ φ d d',
    eq_decl φ d d' →
    eq_decl φ (map_decl_anon nl d) (map_decl_anon nl d').

Lemma nl_eq_context {cf:checker_flags} :
  ∀ φ Γ Γ',
    eq_context φ Γ Γ' →
    eq_context φ (nlctx Γ) (nlctx Γ').

Lemma nl_decompose_app :
  ∀ t,
    decompose_app (nl t)
    = let '(u, vs) := decompose_app t in (nl u, map nl vs).

Lemma nl_fix_context :
  ∀ mfix,
    nlctx (fix_context mfix) = fix_context (map (map_def_anon nl nl) mfix).

Lemma nl_red1 :
  ∀ Σ Γ M N,
    red1 Σ Γ M N →
    red1 (map nl_global_decl Σ) (nlctx Γ) (nl M) (nl N).

Lemma nl_cumul {cf:checker_flags} :
  ∀ Σ Γ A B,
    Σ ;;; Γ |- A ≤ B →
    nlg Σ ;;; nlctx Γ |- nl A ≤ nl B.

Lemma nl_destArity :
  ∀ Γ A Δ s,
    destArity Γ A = Some (Δ, s) →
    destArity (nlctx Γ) (nl A) = Some (nlctx Δ, s).

Lemma nl_instantiate_params :
  ∀ params args ty,
    option_map nl (instantiate_params params args ty) =
    instantiate_params (nlctx params) (map nl args) (nl ty).

Lemma nl_inds :
  ∀ kn u bodies,
    map nl (inds kn u bodies) = inds kn u (map nl_one_inductive_body bodies).

Lemma nl_decompose_prod_assum :
  ∀ Γ t,
    decompose_prod_assum (nlctx Γ) (nl t)
    = let '(Γ, t) := decompose_prod_assum Γ t in (nlctx Γ, nl t).

Lemma nl_it_mkProd_or_LetIn :
  ∀ Γ A,
    nl (it_mkProd_or_LetIn Γ A) = it_mkProd_or_LetIn (nlctx Γ) (nl A).

Lemma nl_to_extended_list:
  ∀ indctx : list context_decl,
    map nl (to_extended_list indctx) = to_extended_list (nlctx indctx).

Lemma subst_instance_context_nlctx u ctx :
  subst_instance_context u (nlctx ctx) = nlctx (subst_instance_context u ctx).

Lemma typing_nlg {cf : checker_flags} :
  env_prop (fun Σ Γ t T ⇒ nlg Σ ;;; nlctx Γ |- nl t : nl T).

Corollary reflect_nleq_term :
  ∀ t t',
    reflect (nl t = nl t') (nleq_term t t').

Lemma nleq_term_it_mkLambda_or_LetIn :
  ∀ Γ u v,
    nleq_term u v →
    nleq_term (it_mkLambda_or_LetIn Γ u) (it_mkLambda_or_LetIn Γ v).

Lemma nl_two M :
  nl (nl M) = nl M.





Lemma nl_red1' Σ Γ M N :
    red1 Σ Γ M N →
    ∑ N', red1 Σ (nlctx Γ) (nl M) N' × nl N = nl N'.