mattam82
commented
2 years ago While putting PR #625 together, I had to go again through most of PCUIC trying to understand the logic of each file, and while I was doing so I collected quite some things that I felt were strange/hard to grasp/unclear, here they are! I’ll try and take care of this soon.
| PCUIC File | Issues |
|---|---|
| Syntax/PCUICTactics.v | can be in utils? |
| utils/PCUICUtils.v | nothing to do here, move to template utils ✅ |
| utils/PCUICOnOne.v | same, move to template utils (merge with All_Forall?) ✅ |
| I think all the follow three could be merged but separately from AstUtils PCUIC File | Issues |
|---|---|
| utils/PCUICSize.v | merge with AstUtils? |
| Syntax/PCUICInduction.v | merge with AstUtils? |
| Syntax/PCUICDepth.v | merge with AstUtils? |
| PCUIC File | Issues |
|---|---|
| utils/PCUICPretty.v | merge with AstUtils? Why do we have print_term and string_of_term? |
I prefer having pretty printing separate from general AstUtils. print_term is more complex and requires an environment, string_of_term is really for the raw syntax.
| PCUIC File | Issues |
|---|---|
| Syntax/PCUICPosition.v | Equality should depend on position, not the other way around? ✅ |
| Syntax/PCUICNamelessDef.v | subsumed by PCUICAlpha, to be removed ✅ |
| Syntax/PCUICClosed.v | what is the point of this given that we have OnFreeVars? Should we try and merge them? |
The two definitions are useful, Closed is closer to what Coq implements (and uses first-order datastructures, more efficient than the on_free_vars predicate). Ideally we should move all the "closed" calls to the safe-checker and use only on_free_vars in the specs/PCUIC. But much of the metatheory would need to be adapted (it uses subst/subst_context a lot in lemma statements).
| PCUIC File | Issues |
|---|---|
| Syntax/PCUICRenameDef.v | this is only 60 lines, and has a weird dependency on typing for something in "syntax", we should probably do something (at least change the name). Also, there is a concurrent notion in PCUICParallelReduction. |
| Syntax/PCUICInstDef.v | similar to PCUICRenameDef.v |
There is no longer a concurrent notion, AFAICT. Maybe we should have a general file PCUICOperations or something with the definitions of renaming and substitution(s)?
Syntax/PCUICLiftSubst.v | how much of this should go into files
I think we should rather move general technical lemmas about lift/subst there.
| PCUIC File | Issues |
|---|---|
| Syntax/PCUICContextRelation.v | made this a part of BasicAst, where context_decl is first defined ✅ |
| PCUICContextSubst.v | Is this worth keeping? |
This could go with the subslet/untyped_subslet theory. Merging these would be nice but will take some time.
| PCUIC File | Issues |
|---|---|
| PCUICCasesContexts.v | similar to PCUICContextSubst.v |
This should be split into PCUICCases for defs and PCUICAlpha for lemmas about alpha conversion
| PCUIC File | Issues |
|---|---|
| Conversion/PCUICNamelessConv.v | subsumed by PCUICAlpha, to be removed ✅ |
| Typing/PCUICNamelessTyp.v | subsumed by PCUICAlpha, to be removed ✅ |
| Conversion/PCUICWeakeningEnvConv.v | should contain the right lemmas which are for now in PCUICWeakeningEnvTyp.v |
| Conversion/PCUICUnivSubstitutionConv.v | same as for PCUICWeakeningEnvConv.v |
I don't understand here, wasn't the idea to split the conversion/typing lemmas or do we want to backtrack on that?
| PCUIC File | Issues |
|---|---|
| Conversion/PCUICOnFreeVarsConv.v | should be renamed/moved into other files |
| Conversion/PCUICClosedConv.v | should be renamed/moves into other files |
| PCUIC File | Issues |
|---|---|
| Typing/PCUICClosedTyp.v | this is not about stability of typing, does putting it with the others still make sense? |
It shows that typable terms are properly closed (and wf global env decls also), so I think it belongs in Typing/. But there is red_on_free_vars as well that could be moved.
| PCUIC File | Issues |
|---|---|
| Typing/PCUICContextConversionTyp.v | there is no PCUICContextConversionConv counterpart, this is weird |
Right, for conversion context-conversion is in PCUICContextConversion (equality_equality_ctx etc...)
| PCUIC File | Issues |
|---|---|
| PCUICReduction.v | needs a bit of cleaning up to present the congruence lemmas properly |
| PCUICGlobalEnv.v | should this be integrated to EnvironmentTyping.v? Nothing specific to typing here ✅ |
| PCUICGeneration.v | very short, should it be merged into Typing.v? ✅ |
| PCUICInversion.v | how much is this redundant with the equivalence bidirectional <-> undirected? should we mention this is a consequence of confluence? |
Don't we need SR for the equivalence? I have a doubt :)
| PCUIC File | Issues |
|---|---|
| PCUICEqualityDec.v | does this belong here or in the safe-checker? |
Probably the safe checker indeed.
| PCUIC File | Issues |
|---|---|
| PCUICSN.v | try and minimize dependencies? ✅ |
| PCUICSafeLemmata.v | should these lemmas be moved to other files where they belong? ✅ |
| PCUICSubstitution.v | there seems to be a lot of mess in this file, does all of it belong here? |
It's certainly waiting to be factored with the sigma-calculus proofs and there are unused notions now (like well-typed conversion paths) that should be used to simplify the later metatheory proofs. That's a TODO for me.
| PCUIC File | Issues |
|---|---|
| PCUICCumulativity.v | maybe change the name to be clearer? |
that would be CumulativityAlgo no?
| PCUIC File | Issues |
|---|---|
| PCUICParallelReductionConfluence.v | should we change rho’s name? it is very uninformative as is |
What would you prefer? parred?
| PCUIC File | Issues |
|---|---|
| PCUICConfluence.v | also contains properties relating eq_term and reduction (eq_term is a simulation for confluence), should we split that apart? ✅ |
| PCUIC File | Issues |
|---|---|
| PCUICWellScopedCumulativity.v | the name equality is very confusing here imho |
Yes, maybe a variant like cumul_gen would be better?
| PCUIC File | Issues |
|---|---|
| PCUICConversion.v | There’s a lot here, putting forward the interesting bits or splitting the file might make sense ✅ |
| PCUIC File | Issues |
|---|---|
| PCUICContexts.v | Not sure what the coherence is here |
| PCUICArities.v | There’s not much about arities here, maybe could be integrated into PCUICSpine (and maybe other places)? |
No coherence here :) This are pot-pourri files, lemmas should be moved to the appropriate files. My TODO
| PCUIC File | Issues |
|---|---|
| PCUICSpine.v | Not sure what’s happening here |
That's all about subslet/spine_subst/context_subst, should be uniformized. On my TODO as well.
| PCUIC File | Issues |
|---|---|
| PCUICCanonicity.v | Does not prove canonicity at all… Should we still prove a form of progress here? Use other forms that are proven elsewhere more or less implicitely? |
Mostly about spines indeed, and the end is about wh_normal/closed values. We should chose a different name for that part.
| PCUIC File | Issues |
|---|---|
| PCUICConvCumInversion.v | This looks like something we should do otherwise using the relations we already have |
The squashing is probably not needed in this file but in the callers, but there is some interesting lemmas about conversion of whnfs that's not elsewhere AFAICT.
| PCUIC File | Issues |
|---|---|
| PCUICPrincipality.v | Should we keep this now that we have the proof using bidirectional typing? |
Nope, if we can stage things easily to replace it.
| PCUIC File | Issues |
|---|---|
| Bidirectional/BDEnvironmentTyping.v | should ideally be integrated into EnvironmentTyping ✅ |
While putting PR #625 together, I had to go again through most of PCUIC trying to understand the logic of each file, and while I was doing so I collected quite some things that I felt were strange/hard to grasp/unclear, here they are! I’ll try and take care of this soon.
equalityis very confusing here imho