Library MetaCoq.PCUIC.PCUICSN

From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import
  PCUICAst PCUICAstUtils PCUICTyping PCUICSafeLemmata PCUICValidity
  PCUICReduction PCUICEquality PCUICConfluence PCUICUnivSubstitutionConv
  PCUICUnivSubstitutionTyp.

Require Import Equations.Prop.DepElim.

We assume normalisation of the reduction. We state is as well-foundedness of the reduction.

Record normalizing_flags {cf : checker_flags} : Prop :=
  { nor_check_univs :> check_univs }.

Existing Class normalizing_flags.

#[local] Instance default_normalizing :
  @normalizing_flags default_checker_flags.
Proof.
  now constructor.
Qed.

#[local] Instance extraction_normalizing :
  @normalizing_flags extraction_checker_flags.
Proof.
  now constructor.
Qed.

Section Normalisation.

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

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

End Normalisation.

Since we are working with name annotations, reduction is sensitive to names. In this section we provide cored' which corresponds to reduction up to α-renaming, as well as the necessary lemmata to show it is well-founded and can be used instead of the usual reduction as a measure.

Section Alpha.

  Context {cf : checker_flags} {no : normalizing_flags}.
  Context (Σ : global_env_ext).
  Context (hΣ : ∥ wf_ext Σ ∥).

  Notation eqt u v := (∥ upto_names 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 ∥.
  Proof using Type.
    intros Γ u v.
    split.
    - intro h. induction h.
      + constructor. constructor. assumption.
      + destruct IHh as [ih]. constructor.
        eapply Relation.t_trans.
        × eassumption.
        × constructor. assumption.
    - intros [h]. induction h.
      + constructor. assumption.
      + eapply cored_trans'. all: eassumption.
  Qed.

  Local Instance substu_pres_eq : SubstUnivPreserving eq.
  Proof using Type.
    red. intros s u u'.
    unfold R_universe_instance.
    intros f. eapply Forall2_map_inv in f.
    assert (u = u') as →.
    { induction f; cbn; auto. f_equal; auto.
      now eapply Universe.make_inj in H. }
    reflexivity.
  Qed.

  Lemma cored'_postpone :
    ∀ Γ u v,
      cored' Γ u v →
      ∃ u', cored Σ Γ u' v ∧ eqt u u'.
  Proof using Type.
    intros Γ u v [u' [v' [r [[hu] [hv]]]]].
    apply cored_alt in r.
    destruct r as [r].
    induction r in u, v, hu, hv.
    - eapply red1_eq_term_upto_univ_r in r. 10: eassumption.
      all:tc.
      destruct r as [u' [r e]].
      ∃ u'. split.
      × constructor. assumption.
      × constructor. etransitivity. 1: eauto.
        now symmetry.
    - specialize (IHr1 y v).
      destruct IHr1 as [y' [h1 [e1]]]; auto. reflexivity.
      specialize (IHr2 u y').
      destruct IHr2 as [u' [h2 ?]]; auto. now symmetry.
      ∃ u'. split.
      + eapply cored_trans'. all: eauto.
      + assumption.
  Qed.

  Corollary cored_upto :
    ∀ Γ u v v',
      cored Σ Γ u v →
      eqt v v' →
      ∃ u', cored Σ Γ u' v' ∧ eqt u u'.
  Proof using Type.
    intros Γ u v v' h e.
    eapply cored'_postpone.
    ∃ u, v. intuition eauto.
    - constructor. reflexivity.
    - destruct e; constructor; now symmetry.
  Qed.

  Lemma Acc_impl :
    ∀ A (R R' : A → A → Prop),
      (∀ x y, R x y → R' x y ) →
      ∀ x, Acc R' x → Acc R x.
  Proof using Type.
    intros A R R' h x hx.
    induction hx as [x h1 h2].
    constructor. intros y hy.
    eapply h2. eapply h. assumption.
  Qed.

  Lemma Acc_cored_cored' :
    ∀ Γ u,
      Acc (cored Σ Γ) u →
      ∀ u', eqt u u' → Acc (cored' Γ) u'.
  Proof using Type.
    intros Γ u h. induction h as [u h ih].
    intros u' e. constructor. intros v [v' [u'' [r [[e1] [e2]]]]].
    assert (ee : eqt u'' u).
    { destruct e. constructor. symmetry; etransitivity; tea. }
    eapply cored_upto in r as hh. 2: exact ee.
    destruct hh as [v'' [r' [e']]].
    eapply ih.
    - eassumption.
    - destruct ee. constructor. symmetry; etransitivity; eassumption.
  Qed.

  Lemma normalisation_upto :
    ∀ Γ u,
      welltyped Σ Γ u →
      Acc (cored' Γ) u.
  Proof using hΣ.
    destruct hΣ.
    intros Γ u h.
    apply normalisation in h.
    2: assumption.
    eapply Acc_cored_cored'.
    - eassumption.
    - constructor; reflexivity.
  Qed.

  Lemma cored_eq_context_upto_names :
    ∀ Γ Δ u v,
      eq_context_upto_names Γ Δ →
      cored Σ Γ u v →
      cored Σ Δ u v.
  Proof using Type.
    intros Γ Δ u v e h.
    apply cored_alt in h as [h].
    induction h in Δ, e |- ×.
    - constructor. eapply red1_eq_context_upto_names. all: eauto.
    - eapply cored_trans'.
      + eapply IHh2. assumption.
      + eapply IHh1. assumption.
  Qed.

  Lemma cored_eq_term_upto :
    ∀ Σ' Re Rle Γ u v u',
      RelationClasses.Reflexive Re →
      SubstUnivPreserving Re →
      RelationClasses.Reflexive Rle →
      SubstUnivPreserving 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' ∥.
  Proof using Type.
    intros Σ' Re Rle Γ u v u' X X0 X1 X2 X3 X4 X5 X6 e h.
    apply cored_alt in h as [h].
    induction h in u', e |- ×.
    - eapply red1_eq_term_upto_univ_l in r. 9: eauto. all: auto.
      destruct r as [? [? ?]].
      eexists. split.
      + constructor. eassumption.
      + constructor. assumption.
    - specialize (IHh1 _ e). destruct IHh1 as [y' [r1 [e1]]].
      specialize (IHh2 _ e1). destruct IHh2 as [z' [r2 [e2]]].
      ∃ z'. split.
      + eapply cored_trans'. all: eassumption.
      + constructor. assumption.
  Qed.

  Lemma cored_eq_context_upto :
    ∀ Σ' Re Γ Δ u v,
      RelationClasses.Reflexive Re →
      RelationClasses.Symmetric Re →
      RelationClasses.Transitive Re →
      SubstUnivPreserving Re →
      eq_context_upto Σ' Re Re Γ Δ →
      cored Σ Γ u v →
      ∃ u', cored Σ Δ u' v ∧ ∥ eq_term_upto_univ Σ' Re Re u u' ∥.
  Proof using Type.
    intros Σ' Re Γ Δ u v hRe1 hRe2 hRe3 hRe4 e h.
    apply cored_alt in h as [h].
    induction h.
    - eapply red1_eq_context_upto_l in r. all: eauto. 2:tc.
      destruct r as [? [? ?]].
      eexists. split.
      + constructor. eassumption.
      + constructor. assumption.
    - destruct IHh1 as [x' [r1 [e1]]].
      destruct IHh2 as [y' [r2 [e2]]].
      eapply cored_eq_term_upto in r2. 10: exact e1. all: auto.
      2:tc.
      destruct r2 as [y'' [r2' [e2']]].
      ∃ y''. split.
      × eapply cored_trans'. all: eassumption.
      × constructor. eapply eq_term_upto_univ_trans. all: eauto.
  Qed.

  Lemma cored_cored' :
    ∀ Γ u v,
      cored Σ Γ u v →
      cored' Γ u v.
  Proof using Type.
    intros Γ u v h.
    ∃ u, v. intuition eauto.
    - constructor. reflexivity.
    - constructor. reflexivity.
  Qed.

End Alpha.