Library MetaCoq.PCUIC.PCUICCumulativity

Reserved Notation " Σ ;;; Γ |- t == u " (at level 50, Γ, t, u at next level).

Lemma cumul_alt `{cf : checker_flags} Σ Γ t u :
  Σ ;;; Γ |- t ≤ u <~> { v & { v' & (red Σ Γ t v × red Σ Γ u v' × leq_term (global_ext_constraints Σ) v v')%type } }.
Lemma cumul_refl' {cf : checker_flags} Σ Γ t : Σ ;;; Γ |- t ≤ t.

Lemma conv_refl' {cf : checker_flags} Σ Γ t : Σ ;;; Γ |- t = t.

Lemma red_cumul `{cf : checker_flags} {Σ : global_env_ext} {Γ t u} :
  red Σ Γ t u →
  Σ ;;; Γ |- t ≤ u.

Lemma red_cumul_inv `{cf : checker_flags} {Σ : global_env_ext} {Γ t u} :
  red Σ Γ t u →
  Σ ;;; Γ |- u ≤ t.

Lemma red_cumul_cumul `{cf : checker_flags} {Σ : global_env_ext} {Γ t u v} :
  red Σ Γ t u → Σ ;;; Γ |- u ≤ v → Σ ;;; Γ |- t ≤ v.

Lemma red_cumul_cumul_inv `{cf : checker_flags} {Σ : global_env_ext} {Γ t u v} :
  red Σ Γ t v → Σ ;;; Γ |- u ≤ v → Σ ;;; Γ |- u ≤ t.

Lemma red_conv {cf:checker_flags} (Σ : global_env_ext) Γ t u : red Σ Γ t u → Σ ;;; Γ |- t = u.

Lemma conv_cumul {cf:checker_flags} Σ Γ t u :
  Σ ;;; Γ |- t = u → (Σ ;;; Γ |- t ≤ u) × (Σ ;;; Γ |- u ≤ t).

Lemma All_All2_refl {A : Type} {R} {l : list A} : All (fun x : A ⇒ R x x) l → All2 R l l.

Lemma eq_term_App `{checker_flags} φ f f' :
  eq_term φ f f' →
  isApp f = isApp f'.

Lemma eq_term_mkApps `{checker_flags} φ f l f' l' :
  eq_term φ f f' →
  All2 (eq_term φ) l l' →
  eq_term φ (mkApps f l) (mkApps f' l').

Lemma leq_term_App `{checker_flags} φ f f' :
  leq_term φ f f' →
  isApp f = isApp f'.

Lemma leq_term_mkApps `{checker_flags} φ f l f' l' :
  leq_term φ f f' →
  All2 (eq_term φ) l l' →
  leq_term φ (mkApps f l) (mkApps f' l').

Inductive conv_alt `{checker_flags} (Σ : global_env_ext) (Γ : context) : term → term → Type :=
| conv_alt_refl t u : eq_term (global_ext_constraints Σ) t u → Σ ;;; Γ |- t == u
| conv_alt_red_l t u v : red1 Σ Γ t v → Σ ;;; Γ |- v == u → Σ ;;; Γ |- t == u
| conv_alt_red_r t u v : Σ ;;; Γ |- t == v → red1 (fst Σ) Γ u v → Σ ;;; Γ |- t == u
where " Σ ;;; Γ |- t == u " := (@conv_alt _ Σ Γ t u) : type_scope.

Lemma red_conv_alt `{cf : checker_flags} Σ Γ t u :
  red (fst Σ) Γ t u →
  Σ ;;; Γ |- t == u.


Lemma red_conv_conv `{cf : checker_flags} Σ Γ t u v :
  red (fst Σ) Γ t u → Σ ;;; Γ |- u == v → Σ ;;; Γ |- t == v.

Lemma red_conv_conv_inv `{cf : checker_flags} Σ Γ t u v :
  red (fst Σ) Γ t u → Σ ;;; Γ |- v == u → Σ ;;; Γ |- v == t.

Lemma conv_alt_sym `{cf : checker_flags} (Σ : global_env_ext) Γ t u :
  wf Σ →
  Σ ;;; Γ |- t == u → Σ ;;; Γ |- u == t.

Lemma conv_alt_red {cf : checker_flags} {Σ : global_env_ext} {Γ : context} {t u : term} :
  Σ;;; Γ |- t == u <~> (∑ v v' : term, (red Σ Γ t v × red Σ Γ u v') × eq_term (global_ext_constraints Σ) v v').

Lemma conv_alt_cumul `{cf : checker_flags} (Σ : global_env_ext) Γ t u : wf Σ →
  Σ ;;; Γ |- t == u → Σ ;;; Γ |- t ≤ u.

Lemma conv_alt_conv `{cf : checker_flags} (Σ : global_env_ext) Γ t u : wf Σ →
  Σ ;;; Γ |- t == u → Σ ;;; Γ |- t = u.

Inductive conv_pb :=
| Conv
| Cumul.

Definition conv `{cf : checker_flags} leq Σ Γ u v :=
  match leq with
  | Conv ⇒ ∥ Σ ;;; Γ |- u == v ∥
  | Cumul ⇒ ∥ Σ ;;; Γ |- u ≤ v ∥
  end.

Lemma conv_conv_l `{cf : checker_flags} :
  ∀ (Σ : global_env_ext) leq Γ u v, wf Σ →
      Σ ;;; Γ |- u == v →
      conv leq Σ Γ u v.

Lemma conv_conv_r `{cf : checker_flags} :
  ∀ (Σ : global_env_ext) leq Γ u v, wf Σ →
      Σ ;;; Γ |- u == v →
      conv leq Σ Γ v u.

Lemma cumul_App_l `{cf : checker_flags} :
  ∀ {Σ Γ f g x},
    Σ ;;; Γ |- f ≤ g →
    Σ ;;; Γ |- tApp f x ≤ tApp g x.