Stream: MetaCoq

Topic: ✔ `cored` and `extends_decls`


view this post on Zulip Jason Gross (Dec 06 2022 at 20:51):

I want a theorem proving

  forall (cf : checker_flags) (Σ Σ' : global_env),
  extends_decls Σ Σ' ->
  wf Σ ->
  wf Σ' ->
  forall (Γ : context) (u u' : Universes.universes_decl),
  wf_local (Σ, u) Γ ->
  wf_local (Σ', u') Γ ->
  forall x y : PCUICAst.term,
  PCUICSafeLemmata.cored Σ Γ x y -> PCUICSafeLemmata.cored Σ' Γ x y

Does it exist? If not, where should I add it?

view this post on Zulip Théo Winterhalter (Dec 06 2022 at 21:01):

So it's just weakening of cored for the global environment right? We should have it for red and since cored x y is (logically equivalent to) red y x it should work? I don't see why you would need all these hypotheses though.

view this post on Zulip Jason Gross (Dec 06 2022 at 21:11):

Yes. I don't need all the hypotheses, that's just what I have available.

view this post on Zulip Jason Gross (Dec 06 2022 at 21:12):

It looks like we only have cored logically equivalent to ∥ redp ∥ and redp a subrelation of red, though?

view this post on Zulip Jason Gross (Dec 06 2022 at 21:13):

What's the weakening lemma called for red?

view this post on Zulip Jason Gross (Dec 06 2022 at 21:14):

(I only see one for context weakening, not global env weakening...)

view this post on Zulip Jason Gross (Dec 06 2022 at 21:25):

Ah, found it in PCUICWeakeningEnvConv, weakening_env_red1

view this post on Zulip Meven Lennon-Bertrand (Dec 06 2022 at 21:29):

Looks like it is here for one-step reduction, but there does not seem to be a corresponding lemma for the transitive closure…

view this post on Zulip Meven Lennon-Bertrand (Dec 06 2022 at 21:30):

Oops, my bad, you found it already

view this post on Zulip Jason Gross (Dec 06 2022 at 21:31):

Yeah, but I sent my "found" notice to the wrong stream

view this post on Zulip Théo Winterhalter (Dec 07 2022 at 07:28):

Oh I don't know what redp is. In any case, I don't think it's desirable to have such a lemma in the library since it's just a tool for termination, we don't need to prove more stuff about it.

view this post on Zulip Yannick Forster (Dec 07 2022 at 07:32):

Mh, but we might prove more stuff about termination in future, no? If Jason proved it, I'm in favour of including it in upstream MetaCoq. It won't create issues for other code that's already there, and it might save whoever will need it in the future the time it would take to reprove it

view this post on Zulip Théo Winterhalter (Dec 07 2022 at 07:34):

I would guess not but as you say it does no harm (except in making the development grow in size).

view this post on Zulip Jason Gross (Dec 07 2022 at 22:21):

I'm not using it locally in my development, but in making normalization into a typeclass.

view this post on Zulip Théo Winterhalter (Dec 08 2022 at 09:05):

Oh you need it there? Then I guess we must accept it. :)

view this post on Zulip Jason Gross (Dec 08 2022 at 09:23):

PR at https://github.com/MetaCoq/metacoq/pull/801

The proof is needed because erasure needs normalization not just in the global environment it's passed, but also in the env that results from popping off decls.

view this post on Zulip Théo Winterhalter (Dec 08 2022 at 09:26):

I'm surprised because I thought cored would never appear in a setting where you change the global environment. Anyway we can merge it I guess.

view this post on Zulip Jason Gross (Dec 08 2022 at 09:29):

Thank you!

view this post on Zulip Notification Bot (Dec 08 2022 at 09:29):

Jason Gross has marked this topic as resolved.


Last updated: May 31 2023 at 02:31 UTC