Cache reified lemmas with LetIn #77
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
JasonGross
force-pushed
the
cache-reify-let-in
branch
4 times, most recently
from
52443e6
to
91bf2db
Compare
Implementing a strategy devised in discussion with Andres: > Like, maybe we want to reify the cache using LetIn instead of let in, > have a variant of interp that takes a list of definitions (either > untyped or with types lifted from the syntax or maybe just with reified > types so that we can transport easily enough) that are supposed to be > equal to the cache, and proving equality with interp leaves over > subgoals for cache equality? > Have a version of interp that takes in a nat and asks for arguments > for the first n LetIns, and then does normal interp, and a lemma that > takes in n and the interps for the first n LetIns and proofs that the > values are correct, and proves that special interp equal to the normal > interp. Then we prove equality overall by App special_interp_eq [t; e; > constant1; eq_refl; constant1; eq_refl; ... ; constantn; eq_refl; > eq_refl] We use a slight variant of this, making use of the UnderLets monad to avoid the use of `nat`.
|
The CI needs to be re-run once the new docker dev image is pushed in light of the merge of coq/coq#16619 |
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.
Implementing a strategy devised in discussion with Andres:
We use a slight variant of this, making use of the UnderLets monad to
avoid the use of
nat.