Library MetaCoq.PCUIC.PCUICSN

Section Normalisation.

  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).

  Axiom normalisation :
    ∀ Γ t,
      welltyped Σ Γ t →
      Acc (cored (fst Σ) Γ) t.

  Lemma Acc_cored_Prod Γ n t1 t2 :
    Acc (cored Σ Γ) t1 →
    Acc (cored Σ (Γ,, vass n t1)) t2 →
    Acc (cored Σ Γ) (tProd n t1 t2).

  Lemma Acc_cored_LetIn Γ n t1 t2 t3 :
    Acc (cored Σ Γ) t1 →
    Acc (cored Σ Γ) t2 → Acc (cored Σ (Γ,, vdef n t1 t2)) t3 →
    Acc (cored Σ Γ) (tLetIn n t1 t2 t3).

  Lemma neq_mkApps u l : ∀ t, t ≠ tSort u → mkApps t l ≠ tSort u.

  Corollary normalisation' :
    ∀ Γ t, wf Σ → wellformed Σ Γ t → Acc (cored (fst Σ) Γ) t.

End Normalisation.

Section Alpha.

  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).
  Context (hΣ : ∥ wf Σ ∥).

  Notation eqt u v :=
    (∥ eq_term (global_ext_constraints Σ) u v ∥).

  Definition cored' Γ u v :=
    ∃ u' v', cored Σ Γ u' v' ∧ eqt u u' ∧ eqt v v'.

  Lemma cored_alt :
    ∀ Γ u v,
      cored Σ Γ u v <~> ∥ Relation.trans_clos (red1 Σ Γ) v u ∥.

  Lemma cored'_postpone :
    ∀ Γ u v,
      cored' Γ u v →
      ∃ u', cored Σ Γ u' v ∧ eqt u u'.

  Corollary cored_upto :
    ∀ Γ u v v',
      cored Σ Γ u v →
      eq_term Σ v v' →
      ∃ u', cored Σ Γ u' v' ∧ eqt u u'.

  Lemma Acc_impl :
    ∀ A (R R' : A → A → Prop),
      (∀ x y, R x y → R' x y) →
      ∀ x, Acc R' x → Acc R x.

  Lemma Acc_cored_cored' :
    ∀ Γ u,
      Acc (cored Σ Γ) u →
      ∀ u', eq_term Σ u u' → Acc (cored' Γ) u'.

  Lemma normalisation_upto :
    ∀ Γ u,
      wellformed Σ Γ u →
      Acc (cored' Γ) u.

  Lemma cored_eq_context_upto_names :
    ∀ Γ Δ u v,
      eq_context_upto_names Γ Δ →
      cored Σ Γ u v →
      cored Σ Δ u v.

  Lemma cored_eq_term_upto :
    ∀ Re Rle Γ u v u',
      RelationClasses.Reflexive Re →
      SubstUnivPreserving Re →
      RelationClasses.Reflexive Rle →
      RelationClasses.Symmetric Re →
      RelationClasses.Transitive Re →
      RelationClasses.Transitive Rle →
      RelationClasses.subrelation Re Rle →
      eq_term_upto_univ Re Rle u u' →
      cored Σ Γ v u →
      ∃ v', cored Σ Γ v' u' ∧ ∥ eq_term_upto_univ Re Rle v v' ∥.

  Lemma cored_eq_context_upto :
    ∀ Re Γ Δ u v,
      RelationClasses.Reflexive Re →
      RelationClasses.Symmetric Re →
      RelationClasses.Transitive Re →
      SubstUnivPreserving Re →
      eq_context_upto Re Γ Δ →
      cored Σ Γ u v →
      ∃ u', cored Σ Δ u' v ∧ ∥ eq_term_upto_univ Re Re u u' ∥.

  Lemma eq_context_upto_nlctx :
    ∀ Γ,
      eq_context_upto eq Γ (nlctx Γ).

  Lemma cored_cored'_nl :
    ∀ Γ u v,
      cored Σ Γ u v →
      cored' (nlctx Γ) (nl u) (nl v).

  Lemma cored_cored' :
    ∀ Γ u v,
      cored Σ Γ u v →
      cored' Γ u v.

End Alpha.