Library MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv

From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
  PCUICWeakeningEnv PCUICEquality PCUICReduction PCUICCumulativity PCUICCumulativitySpec
  
   .
From Equations Require Import Equations.

Require Import ssreflect.

Set Default Goal Selector "!".
Implicit Types (cf : checker_flags).

Lemma compare_term_subset {cf} pb Σ φ φ' t t'
  : ConstraintSet.Subset φ φ'
     compare_term pb Σ φ t t' compare_term pb Σ φ' t t'.
Proof.
  intro H. apply eq_term_upto_univ_impl; auto.
  all: change eq_universe with (compare_universe Conv).
  all: change leq_universe with (compare_universe Cumul).
  3: destruct pb.
  4: transitivity (compare_universe Cumul φ).
  4: tc.
  all: intros ??; now eapply cmp_universe_subset.
Qed.

Lemma eq_term_subset {cf} Σ φ φ' t t'
  : ConstraintSet.Subset φ φ' eq_term Σ φ t t' eq_term Σ φ' t t'.
Proof. apply compare_term_subset with (pb := Conv). Qed.

Lemma leq_term_subset {cf:checker_flags} Σ ctrs ctrs' t u
  : ConstraintSet.Subset ctrs ctrs' leq_term Σ ctrs t u leq_term Σ ctrs' t u.
Proof. apply compare_term_subset with (pb := Cumul). Qed.

Lemma compare_decl_subset {cf} pb Σ φ φ' d d'
  : ConstraintSet.Subset φ φ'
     compare_decl pb Σ φ d d' compare_decl pb Σ φ' d d'.
Proof.
  intros Hφ []; constructor; eauto using compare_term_subset.
Qed.

Lemma compare_context_subset {cf} pb Σ φ φ' Γ Γ'
  : ConstraintSet.Subset φ φ'
     compare_context pb Σ φ Γ Γ' compare_context pb Σ φ' Γ Γ'.
Proof.
  intros Hφ. induction 1; constructor; auto; eapply compare_decl_subset; eassumption.
Qed.

Section ExtendsWf.
  Context {cf : checker_flags}.
  Context {Pcmp: global_env_ext context conv_pb term term Type}.
  Context {P: global_env_ext context term typ_or_sort Type}.

  Let wf := on_global_env Pcmp P.

Lemma global_variance_sigma_mon {Σ Σ' gr napp v} :
  wf Σ' extends Σ Σ'
  global_variance Σ gr napp = Some v
  global_variance Σ' gr napp = Some v.
Proof using P Pcmp cf.
  intros wfΣ' ext.
  rewrite /global_variance /lookup_constructor /lookup_inductive /lookup_minductive.
  destruct gr as [|ind|[ind i]|] ⇒ /= //.
  - destruct (lookup_env Σ ind) eqn:look ⇒ //.
    eapply extends_lookup in look; eauto. rewrite look //.
  - destruct (lookup_env Σ (inductive_mind i)) eqn:look ⇒ //.
    eapply extends_lookup in look; eauto. rewrite look //.
Qed.

The definition of R_global_instance is defined so that it is weakenable.
Lemma R_global_instance_weaken_env Σ Σ' Re Re' Rle Rle' gr napp :
  wf Σ' extends Σ Σ'
  RelationClasses.subrelation Re Re'
  RelationClasses.subrelation Rle Rle'
  RelationClasses.subrelation Re Rle'
  subrelation (R_global_instance Σ Re Rle gr napp) (R_global_instance Σ' Re' Rle' gr napp).
Proof using P Pcmp cf.
  intros wfΣ ext he hle hele t t'.
  rewrite /R_global_instance /R_opt_variance.
  destruct global_variance as [v|] eqn:look.
  - rewrite (global_variance_sigma_mon wfΣ ext look).
    induction t in v, t' |- *; destruct v, t'; simpl; auto.
    intros []; split; auto.
    destruct t0; simpl; auto.
  - destruct (global_variance Σ' gr napp) ⇒ //.
    × induction t in l, t' |- *; destruct l, t'; simpl; intros H; inv H; auto.
      split; auto. destruct t0; simpl; auto.
    × eauto using R_universe_instance_impl'.
Qed.

#[global]
Instance eq_term_upto_univ_weaken_env Σ Σ' Re Re' Rle Rle' napp :
  wf Σ' extends Σ Σ'
  RelationClasses.subrelation Re Re'
  RelationClasses.subrelation Rle Rle'
  RelationClasses.subrelation Re Rle'
  CRelationClasses.subrelation (eq_term_upto_univ_napp Σ Re Rle napp)
    (eq_term_upto_univ_napp Σ' Re' Rle' napp).
Proof using P Pcmp cf.
  intros wfΣ ext he hele hle t t'.
  induction t in napp, t', Rle, Rle', hle, hele |- × using PCUICInduction.term_forall_list_ind;
    try (inversion 1; subst; constructor;
         eauto using R_universe_instance_impl'; fail).
  - inversion 1; subst; constructor.
    eapply All2_impl'; tea.
    eapply All_impl; eauto.
  - inversion 1; subst; constructor.
    eapply R_global_instance_weaken_env. 6:eauto. all:eauto.
  - inversion 1; subst; constructor.
    eapply R_global_instance_weaken_env. 6:eauto. all:eauto.
  - inversion 1; subst; destruct X as [? [? ?]]; constructor; eauto.
    × destruct X2 as [? [? ?]].
      constructor; intuition auto; solve_all.
      + eauto using R_universe_instance_impl'.
    × eapply All2_impl'; tea.
      eapply All_impl; eauto.
      cbn. intros x [? ?] y [? ?]. split; eauto.
  - inversion 1; subst; constructor.
    eapply All2_impl'; tea.
    eapply All_impl; eauto.
    cbn. intros x [? ?] y [[[? ?] ?] ?]. repeat split; eauto.
  - inversion 1; subst; constructor.
    eapply All2_impl'; tea.
    eapply All_impl; eauto.
    cbn. intros x [? ?] y [[[? ?] ?] ?]. repeat split; eauto.
Qed.

Lemma weakening_env_red1 Σ Σ' Γ M N :
  wf Σ'
  extends Σ Σ'
  red1 Σ Γ M N
  red1 Σ' Γ M N.
Proof using P Pcmp cf.
  induction 3 using red1_ind_all;
    try solve [econstructor; eauto with extends; solve_all].
Qed.

Lemma weakening_env_cumul_gen pb Σ Σ' φ Γ M N :
  wf Σ'
  extends Σ Σ'
  cumulAlgo_gen (Σ, φ) Γ pb M N
  cumulAlgo_gen (Σ', φ) Γ pb M N.
Proof using P Pcmp.
  intros wfΣ ext.
  induction 1; simpl.
  - econstructor. eapply compare_term_subset.
    + now eapply global_ext_constraints_app.
    + simpl in ×. eapply eq_term_upto_univ_weaken_env in c; simpl; eauto.
      all:typeclasses eauto.
  - econstructor 2; eauto. eapply weakening_env_red1; eauto.
  - econstructor 3; eauto. eapply weakening_env_red1; eauto.
Qed.

Lemma weakening_env_conv Σ Σ' φ Γ M N :
  wf Σ'
  extends Σ Σ'
  convAlgo (Σ, φ) Γ M N
  convAlgo (Σ', φ) Γ M N.
Proof using P Pcmp. apply weakening_env_cumul_gen with (pb := Conv). Qed.

Lemma weakening_env_cumul Σ Σ' φ Γ M N :
  wf Σ'
  extends Σ Σ'
  cumulAlgo (Σ, φ) Γ M N
  cumulAlgo (Σ', φ) Γ M N.
Proof using P Pcmp. apply weakening_env_cumul_gen with (pb := Cumul). Qed.

Lemma weakening_env_cumulSpec0 Σ Σ' φ Γ pb M N :
  wf Σ'
  extends Σ Σ'
  cumulSpec0 (Σ, φ) Γ pb M N
  cumulSpec0 (Σ', φ) Γ pb M N.
Proof.
  intros HΣ' Hextends Ind.
  pose proof (subrelations_leq_extends _ _ φ Hextends). revert H.
  assert (RelationClasses.subrelation
          (eq_universe (global_ext_constraints (Σ,φ)))
          (leq_universe (global_ext_constraints (Σ',φ)))).
  { typeclasses eauto. } revert H.
  generalize (leq_universe (global_ext_constraints (Σ',φ))); intros Rle Hlee Hle .
  revert pb Γ M N Ind Σ' Rle Hle Hlee HΣ' Hextends.
  apply: (cumulSpec0_ind_all (Σ,φ)).
  all:intros; try solve [econstructor; eauto with extends; intuition auto].
  - eapply cumul_Evar. solve_all.
  - eapply cumul_Case.
    × destruct X as (Hparams & Hinst & Hctx & Hret & IHret). repeat split; tas.
      + solve_all.
      + eapply R_universe_instance_impl'; eauto; apply subrelations_extends; eauto.
      + eapply IHret; eauto.
    × solve_all.
    × solve_all.
  - eapply cumul_Fix; solve_all.
  - eapply cumul_CoFix; solve_all.
  - eapply cumul_Ind; eauto. 2:solve_all.
    eapply @R_global_instance_weaken_env. 1,2,6:eauto. all: tc.
  - eapply cumul_Construct; eauto. 2:solve_all.
    eapply @R_global_instance_weaken_env. 1,2,6:eauto. all: tc.
  - eapply cumul_Sort. eapply subrelations_compare_extends; tea.
  - eapply cumul_Const. eapply R_universe_instance_impl'; eauto; tc.
Defined.

Lemma weakening_env_convSpec Σ Σ' φ Γ M N :
  wf Σ'
  extends Σ Σ'
  convSpec (Σ, φ) Γ M N
  convSpec (Σ', φ) Γ M N.
Proof using P Pcmp. apply weakening_env_cumulSpec0 with (pb := Conv). Qed.

Lemma weakening_env_cumulSpec Σ Σ' φ Γ M N :
  wf Σ'
  extends Σ Σ'
  cumulSpec (Σ, φ) Γ M N
  cumulSpec (Σ', φ) Γ M N.
Proof using P Pcmp. apply weakening_env_cumulSpec0 with (pb := Cumul). Qed.

Lemma weakening_env_conv_decls {Σ φ Σ' Γ Γ'} :
  wf Σ' extends Σ Σ'
  CRelationClasses.subrelation (conv_decls cumulSpec0 (Σ, φ) Γ Γ') (conv_decls cumulSpec0 (Σ', φ) Γ Γ').
Proof using P Pcmp.
  intros wfΣ' ext d d' Hd; depelim Hd; constructor; tas;
    eapply weakening_env_convSpec; tea.
Qed.

Lemma weakening_env_cumul_decls {Σ φ Σ' Γ Γ'} :
  wf Σ' extends Σ Σ'
  CRelationClasses.subrelation (cumul_decls cumulSpec0 (Σ, φ) Γ Γ') (cumul_decls cumulSpec0 (Σ', φ) Γ Γ').
Proof using P Pcmp.
  intros wfΣ' ext d d' Hd; depelim Hd; constructor; tas;
    (eapply weakening_env_convSpec || eapply weakening_env_cumulSpec); tea.
Qed.

Lemma weakening_env_conv_ctx {Σ Σ' φ Γ Δ} :
  wf Σ'
  extends Σ Σ'
  conv_context cumulSpec0 (Σ, φ) Γ Δ
  conv_context cumulSpec0 (Σ', φ) Γ Δ.
Proof using P Pcmp.
  intros wfΣ' ext.
  intros; eapply All2_fold_impl; teaΓ0 Γ' d d'.
  now eapply weakening_env_conv_decls.
Qed.

Lemma weakening_env_cumul_ctx {Σ Σ' φ Γ Δ} :
  wf Σ'
  extends Σ Σ'
  cumul_context cumulSpec0 (Σ, φ) Γ Δ
  cumul_context cumulSpec0 (Σ', φ) Γ Δ.
Proof using P Pcmp.
  intros wfΣ' ext.
  intros; eapply All2_fold_impl; teaΓ0 Γ' d d'.
  now eapply weakening_env_cumul_decls.
Qed.

End ExtendsWf.

#[global] Hint Resolve weakening_env_conv_ctx : extends.
#[global] Hint Resolve weakening_env_cumul_ctx : extends.