Stream: MetaCoq

Topic: Why `extends_decls` in `PCUICElimination.Informative`

Jason Gross (Dec 09 2022 at 21:49):

Why is there extends_decls (rather than extends) in

Definition Informative `{cf : checker_flags} (Σ : global_env_ext) (ind : inductive) :=
  forall mdecl idecl,
    declared_inductive (fst Σ) ind mdecl idecl ->
    forall Γ args u n (Σ' : global_env_ext),
      wf_ext Σ' ->
      extends_decls Σ Σ' ->
      Is_proof Σ' Γ (mkApps (tConstruct ind n u) args) ->
       #|ind_ctors idecl| <= 1 /\
       squash (All (Is_proof Σ' Γ) (skipn (ind_npars mdecl) args)).

?

I'm trying to figure out what the semantic content of this definition is, so that in my weakening of extends to allow reordering, I can understand whether I'm supposed to be weakening or strengthening extends_decls here (or, if it's important that it's exactly extends_decls and not anything weaker nor stronger, I'd like to understand why that is).

Yannick Forster (Dec 13 2022 at 11:56):

I think it is extends_decls because that's what I needed in proofs. So consequently, it could probably anything else that still makes the proofs around erasure work

Last updated: Jun 04 2023 at 22:30 UTC