Library MetaCoq.PCUIC.PCUICElimination

Definition Is_proof `{cf : checker_flags} Σ Γ t := ∑ T u, Σ ;;; Γ |- t : T × Σ ;;; Γ |- T : tSort u × is_prop_sort u.

Lemma declared_inductive_inj `{cf : checker_flags} {Σ mdecl mdecl' ind idecl idecl'} :
  declared_inductive Σ mdecl' ind idecl' →
  declared_inductive Σ mdecl ind idecl →
  mdecl = mdecl' ∧ idecl = idecl'.

Definition SingletonProp `{cf : checker_flags} (Σ : global_env_ext) (ind : inductive) :=
  ∀ mdecl idecl,
    declared_inductive (fst Σ) mdecl ind idecl →
    ∀ Γ args u n (Σ' : global_env_ext),
      wf Σ' →
      PCUICWeakeningEnv.extends Σ Σ' →
      welltyped Σ' Γ (mkApps (tConstruct ind n u) args) →
      ∥Is_proof Σ' Γ (mkApps (tConstruct ind n u) args)∥ ∧
       #|ind_ctors idecl| ≤ 1 ∧
       squash (All (Is_proof Σ' Γ) (skipn (ind_npars mdecl) args)).

Definition Computational `{cf : checker_flags} (Σ : global_env_ext) (ind : inductive) :=
  ∀ mdecl idecl,
    declared_inductive (fst Σ) mdecl ind idecl →
    ∀ Γ args u n (Σ' : global_env_ext),
      wf Σ' →
      PCUICWeakeningEnv.extends Σ Σ' →
      welltyped Σ' Γ (mkApps (tConstruct ind n u) args) →
      Is_proof Σ' Γ (mkApps (tConstruct ind n u) args) → False.

Definition Informative`{cf : checker_flags} (Σ : global_env_ext) (ind : inductive) :=
  ∀ mdecl idecl,
    declared_inductive (fst Σ) mdecl ind idecl →
    ∀ Γ args u n (Σ' : global_env_ext),
      wf Σ' →
      PCUICWeakeningEnv.extends Σ Σ' →
      Is_proof Σ' Γ (mkApps (tConstruct ind n u) args) →
       #|ind_ctors idecl| ≤ 1 ∧
       squash (All (Is_proof Σ' Γ) (skipn (ind_npars mdecl) args)).

Lemma elim_restriction_works_kelim1 `{cf : checker_flags} (Σ : global_env_ext) Γ T ind npar p c brs mind idecl : wf Σ →
  declared_inductive (fst Σ) mind ind idecl →
  Σ ;;; Γ |- tCase (ind, npar) p c brs : T →
  (Is_proof Σ Γ (tCase (ind, npar) p c brs) → False) → In InType (ind_kelim idecl).

Lemma elim_restriction_works_kelim2 `{cf : checker_flags} (Σ : global_env_ext) ind mind idecl : wf Σ →
  declared_inductive (fst Σ) mind ind idecl →
  In InType (ind_kelim idecl) → Informative Σ ind.

Lemma elim_restriction_works `{cf : checker_flags} (Σ : global_env_ext) Γ T ind npar p c brs mind idecl : wf Σ →
  declared_inductive (fst Σ) mind ind idecl →
  Σ ;;; Γ |- tCase (ind, npar) p c brs : T →
  (Is_proof Σ Γ (tCase (ind, npar) p c brs) → False) → Informative Σ ind.

Lemma declared_projection_projs_nonempty `{cf : checker_flags} {Σ : global_env_ext} { mind ind p a} :
  wf Σ →
  declared_projection Σ mind ind p a →
  ind_projs ind ≠ [].

Lemma elim_restriction_works_proj_kelim1 `{cf : checker_flags} (Σ : global_env_ext) Γ T p c mind idecl :
  wf Σ →
  declared_inductive (fst Σ) mind (fst (fst p)) idecl →
  Σ ;;; Γ |- tProj p c : T →
  (Is_proof Σ Γ (tProj p c) → False) → In InType (ind_kelim idecl).

Lemma elim_restriction_works_proj `{cf : checker_flags} (Σ : global_env_ext) Γ p c mind idecl T :
  wf Σ →
  declared_inductive (fst Σ) mind (fst (fst p)) idecl →
  Σ ;;; Γ |- tProj p c : T →
  (Is_proof Σ Γ (tProj p c) → False) → Informative Σ (fst (fst p)).

Lemma length_of_btys {ind mdecl' idecl' args' u' p pty indctx pctx ps btys} :
  types_of_case ind mdecl' idecl' (firstn (ind_npars mdecl') args') u' p pty = Some (indctx, pctx, ps, btys) →
  #|btys| = #|ind_ctors idecl'|.

Lemma map_option_Some X (L : list (option X)) t : map_option_out L = Some t → All2 (fun x y ⇒ x = Some y) L t.

Lemma tCase_length_branch_inv `{cf : checker_flags} (Σ : global_env_ext) Γ ind npar p n u args brs T m t :
  wf Σ →
  Σ ;;; Γ |- tCase (ind, npar) p (mkApps (tConstruct ind n u) args) brs : T →
  nth_error brs n = Some (m, t) →
  (#|args| = npar + m)%nat.

Section no_prop_leq_type.

Context `{cf : checker_flags}.
Variable Hcf : prop_sub_type = false.

Lemma cumul_prop1 (Σ : global_env_ext) Γ A B u :
  wf Σ →
  is_prop_sort u → Σ ;;; Γ |- B : tSort u →
                                 Σ ;;; Γ |- A ≤ B → Σ ;;; Γ |- A : tSort u.

Lemma cumul_prop2 (Σ : global_env_ext) Γ A B u :
  wf Σ →
  is_prop_sort u → Σ ;;; Γ |- A ≤ B →
                             Σ ;;; Γ |- A : tSort u → Σ ;;; Γ |- B : tSort u.

Lemma leq_universe_prop (Σ : global_env_ext) u1 u2 :
  @check_univs cf = true →
  
  wf Σ →
  @leq_universe cf (global_ext_constraints Σ) u1 u2 →
  (is_prop_sort u1 ∨ is_prop_sort u2) →
  (is_prop_sort u1 ∧ is_prop_sort u2).

End no_prop_leq_type.