Library MetaCoq.PCUIC.PCUICInversion

Section Inversion.

  Context `{checker_flags}.
  Context (Σ : global_env_ext).
  Context (wfΣ : wf Σ).







  Lemma inversion_Rel :
    ∀ {Γ n T},
      Σ ;;; Γ |- tRel n : T →
      ∑ decl,
        wf_local Σ Γ ×
        (nth_error Γ n = Some decl) ×
        Σ ;;; Γ |- lift0 (S n) (decl_type decl) ≤ T.

  Lemma inversion_Var :
    ∀ {Γ i T},
      Σ ;;; Γ |- tVar i : T → False.

  Lemma inversion_Evar :
    ∀ {Γ n l T},
      Σ ;;; Γ |- tEvar n l : T → False.

  Lemma inversion_Sort :
    ∀ {Γ s T},
      Σ ;;; Γ |- tSort s : T →
      ∑ l,
        wf_local Σ Γ ×
        LevelSet.In l (global_ext_levels Σ) ×
        (s = Universe.make l) ×
        Σ ;;; Γ |- tSort (Universe.super l) ≤ T.

  Lemma inversion_Prod :
    ∀ {Γ na A B T},
      Σ ;;; Γ |- tProd na A B : T →
      ∑ s1 s2,
        Σ ;;; Γ |- A : tSort s1 ×
        Σ ;;; Γ ,, vass na A |- B : tSort s2 ×
        Σ ;;; Γ |- tSort (Universe.sort_of_product s1 s2) ≤ T.

  Lemma inversion_Lambda :
    ∀ {Γ na A t T},
      Σ ;;; Γ |- tLambda na A t : T →
      ∑ s B,
        Σ ;;; Γ |- A : tSort s ×
        Σ ;;; Γ ,, vass na A |- t : B ×
        Σ ;;; Γ |- tProd na A B ≤ T.

  Lemma inversion_LetIn :
    ∀ {Γ na b B t T},
      Σ ;;; Γ |- tLetIn na b B t : T →
      ∑ s1 A,
        Σ ;;; Γ |- B : tSort s1 ×
        Σ ;;; Γ |- b : B ×
        Σ ;;; Γ ,, vdef na b B |- t : A ×
        Σ ;;; Γ |- tLetIn na b B A ≤ T.

  Lemma inversion_App :
    ∀ {Γ u v T},
      Σ ;;; Γ |- tApp u v : T →
      ∑ na A B,
        Σ ;;; Γ |- u : tProd na A B ×
        Σ ;;; Γ |- v : A ×
        Σ ;;; Γ |- B{ 0 := v } ≤ T.

  Lemma inversion_Const :
    ∀ {Γ c u T},
      Σ ;;; Γ |- tConst c u : T →
      ∑ decl,
        wf_local Σ Γ ×
        declared_constant Σ c decl ×
        (consistent_instance_ext Σ decl.(cst_universes) u) ×
        Σ ;;; Γ |- subst_instance_constr u (cst_type decl) ≤ T.

  Lemma inversion_Ind :
    ∀ {Γ ind u T},
      Σ ;;; Γ |- tInd ind u : T →
      ∑ mdecl idecl,
        wf_local Σ Γ ×
        declared_inductive Σ mdecl ind idecl ×
        consistent_instance_ext Σ (ind_universes mdecl) u ×
        Σ ;;; Γ |- subst_instance_constr u idecl.(ind_type) ≤ T.

  Lemma inversion_Construct :
    ∀ {Γ ind i u T},
      Σ ;;; Γ |- tConstruct ind i u : T →
      ∑ mdecl idecl cdecl,
        wf_local Σ Γ ×
        declared_constructor (fst Σ) mdecl idecl (ind, i) cdecl ×
        consistent_instance_ext Σ (ind_universes mdecl) u ×
        Σ;;; Γ |- type_of_constructor mdecl cdecl (ind, i) u ≤ T.

  Lemma inversion_Case :
    ∀ {Γ ind npar p c brs T},
      Σ ;;; Γ |- tCase (ind, npar) p c brs : T →
      ∑ u args mdecl idecl pty indctx pctx ps btys,
        declared_inductive Σ mdecl ind idecl ×
        ind_npars mdecl = npar ×
        let pars := firstn npar args in
        Σ ;;; Γ |- p : pty ×
        types_of_case ind mdecl idecl pars u p pty =
        Some (indctx, pctx, ps, btys) ×
        check_correct_arity (global_ext_constraints Σ)
        idecl ind u indctx pars pctx ×
        existsb (leb_sort_family (universe_family ps)) (ind_kelim idecl) ×
        Σ ;;; Γ |- c : mkApps (tInd ind u) args ×
        All2 (fun x y ⇒
          (fst x = fst y) ×
          (Σ ;;; Γ |- snd x : snd y) ×
          (Σ ;;; Γ |- snd y : tSort ps)
        ) brs btys ×
        Σ ;;; Γ |- mkApps p (skipn npar args ++ [c]) ≤ T.

  Lemma inversion_Proj :
    ∀ {Γ p c T},
      Σ ;;; Γ |- tProj p c : T →
      ∑ u mdecl idecl pdecl args,
        declared_projection Σ mdecl idecl p pdecl ×
        Σ ;;; Γ |- c : mkApps (tInd (fst (fst p)) u) args ×
        #|args| = ind_npars mdecl ×
        let ty := snd pdecl in
        Σ ;;; Γ |- (subst0 (c :: List.rev args)) (subst_instance_constr u ty)
                ≤ T.

  Lemma inversion_Fix :
    ∀ {Γ mfix n T},
      Σ ;;; Γ |- tFix mfix n : T →
      ∑ decl,
        let types := fix_context mfix in
        fix_guard mfix ×
        nth_error mfix n = Some decl ×
        wf_local Σ (Γ ,,, types) ×
        All (fun d ⇒
          Σ ;;; Γ ,,, types |- dbody d : (lift0 #|types|) (dtype d) ×
          isLambda (dbody d) = true
        ) mfix ×
        Σ ;;; Γ |- dtype decl ≤ T.

  Lemma inversion_CoFix :
    ∀ {Γ mfix idx T},
      Σ ;;; Γ |- tCoFix mfix idx : T →
      ∑ decl,
        allow_cofix ×
        let types := fix_context mfix in
        nth_error mfix idx = Some decl ×
        wf_local Σ (Γ ,,, types) ×
        All (fun d ⇒
          Σ ;;; Γ ,,, types |- d.(dbody) : lift0 #|types| d.(dtype)
        ) mfix ×
        Σ ;;; Γ |- decl.(dtype) ≤ T.

  Lemma inversion_it_mkLambda_or_LetIn :
    ∀ {Γ Δ t T},
      Σ ;;; Γ |- it_mkLambda_or_LetIn Δ t : T →
      ∑ A,
        Σ ;;; Γ ,,, Δ |- t : A ×
        Σ ;;; Γ |- it_mkProd_or_LetIn Δ A ≤ T.

End Inversion.

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