Library MetaCoq.PCUIC.PCUICSR

Lemma mkApps_inj f a f' l :
  tApp f a = mkApps f' l → l ≠ [] →
  f = mkApps f' (removelast l) ∧ (a = last l a).

Lemma type_mkApps_inv {cf:checker_flags} (Σ : global_env_ext) Γ f u T : wf Σ →
  Σ ;;; Γ |- mkApps f u : T →
  { T' & { U & ((Σ ;;; Γ |- f : T') × (typing_spine Σ Γ T' u U) × (Σ ;;; Γ |- U ≤ T))%type } }.


Lemma type_tFix_inv {cf:checker_flags} (Σ : global_env_ext) Γ mfix idx T : wf Σ →
  Σ ;;; Γ |- tFix mfix idx : T →
  { T' & { rarg & {f & (unfold_fix mfix idx = Some (rarg, f)) × (Σ ;;; Γ |- f : T') × (Σ ;;; Γ |- T' ≤ T) }}}%type.

Definition SR_red1 {cf:checker_flags} (Σ : global_env_ext) Γ t T :=
  ∀ u (Hu : red1 Σ Γ t u), Σ ;;; Γ |- u : T.


Lemma sr_red1 {cf:checker_flags} : env_prop SR_red1.

Definition sr_stmt {cf:checker_flags} (Σ : global_env_ext) Γ t T :=
  ∀ u, red Σ Γ t u → Σ ;;; Γ |- u : T.

Theorem subject_reduction {cf:checker_flags} : ∀ (Σ : global_env_ext) Γ t u T,
  wf Σ → Σ ;;; Γ |- t : T → red Σ Γ t u → Σ ;;; Γ |- u : T.

Lemma subject_reduction1 {cf:checker_flags} {Σ Γ t u T}
  : wf Σ.1 → Σ ;;; Γ |- t : T → red1 Σ.1 Γ t u → Σ ;;; Γ |- u : T.

Section SRContext.
  Context {cf:checker_flags}.

  Definition wf_local_app' {Σ Γ1 Γ2} :
    wf_local Σ Γ1 → wf_local_rel Σ Γ1 Γ2
    → wf_local Σ (Γ1 ,,, Γ2).

  Definition cumul_red_l' `{checker_flags} :
    ∀ Σ Γ t u,
      wf Σ.1 →
      red (fst Σ) Γ t u →
      Σ ;;; Γ |- t ≤ u.


  Lemma red1_ctx_app Σ Γ Γ' Δ :
    red1_ctx Σ Γ Γ' →
    red1_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ).

  Lemma red1_red_ctx Σ Γ Γ' :
    red1_ctx Σ Γ Γ' →
    red_ctx Σ Γ Γ'.

  Lemma nth_error_red1_ctx Σ Γ Γ' n decl :
    wf Σ →
    nth_error Γ n = Some decl →
    red1_ctx Σ Γ Γ' →
    ∑ decl', nth_error Γ' n = Some decl'
              × red Σ Γ' (lift0 (S n) (decl_type decl))
              (lift0 (S n) (decl_type decl')).

  Lemma wf_local_isType_nth Σ Γ n decl :
    wf Σ.1 →
    wf_local Σ Γ →
    nth_error Γ n = Some decl →
    ∑ s, Σ ;;; Γ |- lift0 (S n) (decl_type decl) : tSort s.


  Lemma subject_reduction_ctx :
    env_prop (fun Σ Γ t A ⇒ ∀ Γ', red1_ctx Σ Γ Γ' → Σ ;;; Γ' |- t : A).

  Lemma wf_local_red1 {Σ Γ Γ'} :
    wf Σ.1 →
    red1_ctx Σ.1 Γ Γ' → wf_local Σ Γ → wf_local Σ Γ'.

  Lemma eq_context_upto_names_upto_names Γ Δ :
    eq_context_upto_names Γ Δ → Γ ≡Γ Δ.

  Lemma wf_local_red {Σ Γ Γ'} :
    wf Σ.1 →
    red_ctx Σ.1 Γ Γ' → wf_local Σ Γ → wf_local Σ Γ'.

  Lemma wf_local_subst1 Σ (wfΣ : wf Σ.1) Γ na b t Γ' :
      wf_local Σ (Γ ,,, [],, vdef na b t ,,, Γ') →
      wf_local Σ (Γ ,,, subst_context [b] 0 Γ').

  Lemma red_ctx_app_context_l {Σ Γ Γ' Δ}
    : red_ctx Σ Γ Γ' → red_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ).

   Lemma isWfArity_red1 {Σ Γ A B} :
     wf Σ.1 →
       red1 (fst Σ) Γ A B →
       isWfArity typing Σ Γ A →
       isWfArity typing Σ Γ B.

   Lemma isWfArity_red {Σ Γ A B} :
     wf Σ.1 →
     red (fst Σ) Γ A B →
     isWfArity typing Σ Γ A →
     isWfArity typing Σ Γ B.

   Lemma isWfArity_or_Type_red {Σ Γ A B} :
     wf Σ.1 →
     red (fst Σ) Γ A B →
     isWfArity_or_Type Σ Γ A →
     isWfArity_or_Type Σ Γ B.

  Lemma type_reduction {Σ Γ t A B}
    : wf Σ.1 → wf_local Σ Γ → Σ ;;; Γ |- t : A → red (fst Σ) Γ A B → Σ ;;; Γ |- t : B.

End SRContext.