Library MetaCoq.PCUIC.PCUICValidity

Section Validity.
  Context `{cf : config.checker_flags}.

  Lemma isWfArity_or_Type_lift (Σ : global_env_ext) n Γ ty (isdecl : n ≤ #|Γ|):
    wf Σ → wf_local Σ Γ →
    isWfArity_or_Type Σ (skipn n Γ) ty →
    isWfArity_or_Type Σ Γ (lift0 n ty).

  Lemma destArity_it_mkProd_or_LetIn ctx ctx' t :
    destArity ctx (it_mkProd_or_LetIn ctx' t) =
    destArity (ctx ,,, ctx') t.




  Definition weaken_env_prop_full
             (P : global_env_ext → context → term → term → Type) :=
    ∀ (Σ : global_env_ext) (Σ' : global_env), wf Σ' → extends Σ.1 Σ' →
                                                   ∀ Γ t T, P Σ Γ t T → P (Σ', Σ.2) Γ t T.

  Lemma isWfArity_or_Type_weaken_full : weaken_env_prop_full (fun Σ Γ t T ⇒ isWfArity_or_Type Σ Γ T).

  Lemma isWfArity_or_Type_weaken :
    weaken_env_prop
      (lift_typing (fun Σ Γ (_ T : term) ⇒ isWfArity_or_Type Σ Γ T)).

  Lemma isWfArity_or_Type_subst_instance:
    ∀ (Σ : global_env_ext) (Γ : context) (u : list Level.t) univs (ty : term),
      wf_local Σ Γ →
      consistent_instance_ext Σ univs u →
      isWfArity_or_Type (Σ.1, univs) [] ty →
      isWfArity_or_Type Σ Γ (PCUICUnivSubst.subst_instance_constr u ty).

  Lemma invert_type_mkApps Σ Γ f fty u T :
    Σ ;;; Γ |- mkApps f u : T →
    
    Σ ;;; Γ |- f : fty →
    isWfArity_or_Type Σ Γ fty →
    ∑ T' U,
      Σ ;;; Γ |- f : T' ×
      typing_spine Σ Γ T' u U ×
      Σ ;;; Γ |- U ≤ T.

  Theorem validity :
    env_prop (fun Σ Γ t T ⇒ isWfArity_or_Type Σ Γ T).

End Validity.

Lemma validity_term {cf:checker_flags} {Σ Γ t T} :
  wf Σ.1 → wf_local Σ Γ → Σ ;;; Γ |- t : T → isWfArity_or_Type Σ Γ T.

Corollary validity' :
  ∀ `{checker_flags} {Σ Γ t T},
    wf Σ.1 →
    Σ ;;; Γ |- t : T →
    isWfArity_or_Type Σ Γ T.

Lemma inversion_mkApps :
  ∀ `{checker_flags} {Σ Γ t l T},
    wf Σ.1 →
    Σ ;;; Γ |- mkApps t l : T →
    ∑ A U,
      Σ ;;; Γ |- t : A ×
      typing_spine Σ Γ A l U ×
      Σ ;;; Γ |- U ≤ T.