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?
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.
Yes. I don't need all the hypotheses, that's just what I have available.
It looks like we only have
cored logically equivalent to
∥ redp ∥ and
redp a subrelation of
What's the weakening lemma called for
(I only see one for context weakening, not global env weakening...)
Ah, found it in
Looks like it is here for one-step reduction, but there does not seem to be a corresponding lemma for the transitive closure…
Oops, my bad, you found it already
Yeah, but I sent my "found" notice to the wrong stream
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.
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
I would guess not but as you say it does no harm (except in making the development grow in size).
I'm not using it locally in my development, but in making normalization into a typeclass.
Last updated: Feb 04 2023 at 02:03 UTC