Template <-> PCUIC proofs #533
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mattam82
force-pushed
the
template-pcuic-proofs
branch
from
7b967c5 to
21e77a0
Compare
…than anticipated: one really has to do surgeryon the binary applications derivation to produce onewhere applications are n-ary *without* relying on transitivity of cumulativityanywhere. This requires to use induction on the size of derivations (includingnon-principal/paranoid hypotheses).
mattam82
force-pushed
the
template-pcuic-proofs
branch
from
dddefdc to
f8ab08d
Compare
|
Suprise surprise: when I thought PCUIC -> Template was finished I realized the application case was actually not done. It really requires a stronger induction principle on typing derivations, and a way to measure a special type of application spines to get the induction going. It's all written down in comments and proven now. I will leave the Template -> PCUIC proof as is, that is missing the proof that translation of case predicates and branches is correct, as this is currently very ugly and should get better with the upcoming new case representation. @jakobbotsch I'll handle that part when we settle on the Ast/Typing rule. |
mattam82
force-pushed
the
template-pcuic-proofs
branch
from
ef23702 to
5b34d94
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR fills the remaining holes in these proofs, mainly by updating the Template Typing definitions from what's in PCUIC now. Currently, I only finished the (easier) PCUIC -> Template proof but the other one is just boring passing of well-formedness conditions (I hope 🤞 ).
Two notable differences appeared:
PCUIC needs an additional G |- tProd na A B : tSort s assumption in applications, otherwise it's impossible to produce the corresponding assumption in Template's typing (where application is based on spines, and every product type appearing there must have a sorting judgment). Not to worry, by PCUICValidity we can get rid of this paranoid assumption.
I finally removed the
isLambdaside condition on bodies of (inductive) fixpoints as is is not needed anywhere. (And would be problematic with eta-conversion/reduction)