Library MetaCoq.PCUIC.PCUICPrincipality

Section Principality.
  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).
  Context (wfΣ : wf Σ).

  Definition Is_conv_to_Arity Σ Γ T := ∃ T', ∥red Σ Γ T T'∥ ∧ isArity T'.

  Lemma Is_conv_to_Arity_inv Γ T :
    Is_conv_to_Arity Σ Γ T →
    (∃ na A B, ∥red Σ Γ T (tProd na A B)∥) ∨ (∃ u, ∥red Σ Γ T (tSort u)∥).

  Lemma invert_red_sort Γ u v :
    red Σ Γ (tSort u) v → v = tSort u.

  Lemma invert_cumul_sort_r Γ C u :
    Σ ;;; Γ |- C ≤ tSort u →
               ∑ u', red Σ Γ C (tSort u') × leq_universe (global_ext_constraints Σ) u' u.

  Lemma invert_cumul_sort_l Γ C u :
    Σ ;;; Γ |- tSort u ≤ C →
               ∑ u', red Σ Γ C (tSort u') × leq_universe (global_ext_constraints Σ) u u'.

  Lemma invert_red_prod Γ na A B v :
    red Σ Γ (tProd na A B) v →
    ∑ A' B', (v = tProd na A' B') ×
             (red Σ Γ A A') ×
             (red Σ (vass na A :: Γ) B B').

  Lemma invert_cumul_prod_r Γ C na A B :
    Σ ;;; Γ |- C ≤ tProd na A B →
    ∑ na' A' B', red Σ.1 Γ C (tProd na' A' B') ×
                 (Σ ;;; Γ |- A == A') ×
                 (Σ ;;; (Γ ,, vass na A) |- B' ≤ B).

  Lemma invert_cumul_arity_r (Γ : context) (C : term) T :
    wf_local Σ Γ →
    isArity T →
    Σ;;; Γ |- C ≤ T → Is_conv_to_Arity Σ Γ C.

  Lemma invert_cumul_prod_l Γ C na A B :
    Σ ;;; Γ |- tProd na A B ≤ C →
               ∑ na' A' B', red Σ.1 Γ C (tProd na' A' B') ×
                            (Σ ;;; Γ |- A == A') ×
                            (Σ ;;; (Γ ,, vass na A) |- B ≤ B').

  Lemma invert_cumul_arity_l (Γ : context) (C : term) T :
    wf_local Σ Γ →
    isArity C →
    Σ;;; Γ |- C ≤ T → Is_conv_to_Arity Σ Γ T.

  Lemma invert_red_letin Γ C na d ty b :
    red Σ.1 Γ (tLetIn na d ty b) C →
    (∑ na' d' ty' b',
     (red Σ.1 Γ C (tLetIn na' d' ty' b') ×
      (Σ ;;; Γ |- d = d') ×
      (Σ ;;; Γ |- ty = ty') ×
      (Σ ;;; (Γ ,, vdef na d ty) |- b ≤ b'))) +
    (red Σ.1 Γ (subst10 d b) C)%type.

  Lemma invert_cumul_letin_l Γ C na d ty b :
    Σ ;;; Γ |- tLetIn na d ty b ≤ C →
               
               
               
               
                                                          
               (Σ ;;; Γ |- subst10 d b ≤ C).



  Lemma app_mkApps :
    ∀ u v t l,
      isApp t = false →
      tApp u v = mkApps t l →
      ∑ l',
        (l = l' ++ [v])%list ×
        u = mkApps t l'.

  Lemma invert_red_ind :
    ∀ Γ ind ui l T,
      red Σ.1 Γ (mkApps (tInd ind ui) l) T →
      ∑ l',
        T = mkApps (tInd ind ui) l' ×
        All2 (red Σ Γ) l l'.

  Lemma invert_cumul_ind_l :
    ∀ Γ ind ui l T,
      Σ ;;; Γ |- mkApps (tInd ind ui) l ≤ T →
      ∑ ui' l',
        red Σ.1 Γ T (mkApps (tInd ind ui') l') ×
        R_universe_instance (eq_universe Σ) ui ui' ×
        All2 (fun a a' ⇒ Σ ;;; Γ |- a = a') l l'.

  Lemma invert_cumul_ind_r :
    ∀ Γ ind ui l T,
      Σ ;;; Γ |- T ≤ mkApps (tInd ind ui) l →
      ∑ ui' l',
        red Σ.1 Γ T (mkApps (tInd ind ui') l') ×
        R_universe_instance (eq_universe Σ) ui' ui ×
        All2 (fun a a' ⇒ Σ ;;; Γ |- a == a') l l'.







  Lemma cumul_sort_confluence {Γ A u v} :
    Σ ;;; Γ |- A ≤ tSort u →
    Σ ;;; Γ |- A ≤ tSort v →
    ∑ v', (Σ ;;; Γ |- A == tSort v') ×
          (leq_universe (global_ext_constraints Σ) v' u ∧
           leq_universe (global_ext_constraints Σ) v' v).

  Lemma leq_universe_product_mon u u' v v' :
    leq_universe (global_ext_constraints Σ) u u' →
    leq_universe (global_ext_constraints Σ) v v' →
    leq_universe (global_ext_constraints Σ) (Universe.sort_of_product u v) (Universe.sort_of_product u' v').

  Lemma isWfArity_sort Γ u :
    wf_local Σ Γ →
    isWfArity typing Σ Γ (tSort u).



  Instance conv_alt_transitive Γ : Transitive (fun x y ⇒ Σ ;;; Γ |- x == y).

  Theorem principal_typing {Γ u A B} : Σ ;;; Γ |- u : A → Σ ;;; Γ |- u : B →
    ∑ C, Σ ;;; Γ |- C ≤ A × Σ ;;; Γ |- C ≤ B × Σ ;;; Γ |- u : C.

End Principality.