Library MetaCoq.PCUIC.PCUICGlobalEnv

From Coq Require Import ProofIrrelevance.
From MetaCoq.Template Require Import config utils uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
     PCUICReflect PCUICTyping.

Injectivity of declared*, inversion lemmas on declared global references and universe consistency of the global environment.

Lemma declared_constant_inj {Σ c} decl1 decl2 :
  declared_constant Σ c decl1 declared_constant Σ c decl2 decl1 = decl2.
  intros. unfold declared_constant in ×. rewrite H in H0.
  now inv H0.

Lemma declared_inductive_inj {Σ mdecl mdecl' ind idecl idecl'} :
  declared_inductive Σ ind mdecl' idecl'
  declared_inductive Σ ind mdecl idecl
  mdecl = mdecl' idecl = idecl'.
  intros [] []. unfold declared_minductive in ×.
  rewrite H in H1. inversion H1. subst. rewrite H2 in H0. inversion H0. eauto.

Lemma declared_constructor_inj {Σ mdecl mdecl' idecl idecl' cdecl cdecl' c} :
  declared_constructor Σ c mdecl' idecl' cdecl
  declared_constructor Σ c mdecl idecl cdecl'
  mdecl = mdecl' idecl = idecl' cdecl = cdecl'.
  intros [] [].
  destruct (declared_inductive_inj H H1); subst.
  rewrite H0 in H2. intuition congruence.

Lemma declared_projection_inj {Σ mdecl mdecl' idecl idecl' cdecl cdecl' pdecl pdecl' p} :
  declared_projection Σ p mdecl idecl cdecl pdecl
  declared_projection Σ p mdecl' idecl' cdecl' pdecl'
  mdecl = mdecl' idecl = idecl' cdecl = cdecl' pdecl = pdecl'.
  intros [] [].
  destruct (declared_constructor_inj H H1) as [? []]; subst.
  destruct H0, H2.
  rewrite H0 in H2. intuition congruence.

Lemma declared_inductive_minductive {Σ ind mdecl idecl} :
  declared_inductive Σ ind mdecl idecl declared_minductive Σ (inductive_mind ind) mdecl.
Proof. now intros []. Qed.
Hint Resolve declared_inductive_minductive : pcuic core.

Coercion declared_inductive_minductive : declared_inductive >-> declared_minductive.

Lemma declared_constructor_inductive {Σ ind mdecl idecl cdecl} :
  declared_constructor Σ ind mdecl idecl cdecl
  declared_inductive Σ ind.1 mdecl idecl.
Proof. now intros []. Qed.
Coercion declared_constructor_inductive : declared_constructor >-> declared_inductive.

Lemma declared_projection_constructor {Σ ind mdecl idecl cdecl pdecl} :
  declared_projection Σ ind mdecl idecl cdecl pdecl
  declared_constructor Σ (ind.(proj_ind), 0) mdecl idecl cdecl.
Proof. now intros []. Qed.
Coercion declared_projection_constructor : declared_projection >-> declared_constructor.

Section DeclaredInv.
  Context {cf:checker_flags} {Σ} {wfΣ : wf Σ}.

  Lemma declared_minductive_ind_npars {mdecl ind} :
    declared_minductive Σ ind mdecl
    ind_npars mdecl = context_assumptions mdecl.(ind_params).
  Proof using wfΣ.
    intros h.
    unfold declared_minductive in h.
    eapply lookup_on_global_env in h; tea.
    destruct h as [Σ' [ext wfΣ' decl']].
    red in decl'. destruct decl' as [h ? ? ?].
    now rewrite onNpars.

End DeclaredInv.

Definition wf_global_uctx_invariants {cf:checker_flags} {P} Σ :
  on_global_env cumulSpec0 P Σ
  global_uctx_invariants (global_uctx Σ).
 intros . split.
 - cbn. apply global_levels_InSet.
 - unfold global_uctx.
   simpl. intros [[l ct] l'] Hctr. simpl in ×.
   induction Σ in , l, ct, l', Hctr |- ×.
   destruct . cbn in ×.
   destruct o as [decls cu].
   now specialize (decls _ Hctr).

Lemma LevelSet_in_union_global Σ l ls :
  LevelSet.In l (LevelSet.union ls (universes Σ).1)
  LevelSet.In l (LevelSet.union ls (global_levels (universes Σ))).
  intros H % LevelSet.union_spec.
  apply LevelSet.union_spec. intuition auto.
  right. now apply LevelSet.union_spec.

Definition wf_ext_global_uctx_invariants {cf:checker_flags} {P} Σ :
  on_global_env_ext cumulSpec0 P Σ
  global_uctx_invariants (global_ext_uctx Σ).
 intros . split.
 - apply global_ext_levels_InSet.
 - destruct Σ as [Σ φ]. destruct as [ Hφ].
   destruct (wf_global_uctx_invariants _ ) as [_ XX].
   unfold global_ext_uctx, global_ext_levels, global_ext_constraints.
   simpl. intros [[l ct] l'] Hctr. simpl in ×. apply ConstraintSet.union_spec in Hctr.
   destruct Hctr as [Hctr|Hctr].
   + destruct Hφ as [_ [HH _]]. specialize (HH _ Hctr). cbn in HH.
     intuition auto using LevelSet_in_union_global.
   + specialize (XX _ Hctr).
     split; apply LevelSet.union_spec; right; apply XX.

Lemma wf_consistent {cf:checker_flags} Σ {P} :
  on_global_env cumulSpec0 P Σ consistent (global_constraints Σ).
  destruct Σ.
  intros [cu ong]. apply cu.

Definition global_ext_uctx_consistent {cf:checker_flags} {P} Σ
 : on_global_env_ext cumulSpec0 P Σ consistent (global_ext_uctx Σ).2.
  intros . cbn. unfold global_ext_constraints.
  unfold wf_ext, on_global_env_ext in .
  destruct as (_ & _ & _ & HH & _). apply HH.