Open
Conversation
Member
|
dlet is a definition wrapper around let in, is it possible there's something that's matching modulo delta? Have you tried seeing if just adding the instances in this file results in the change happening? Alternatively/additionally, if you want to paste a diff of the type class logs, that'll probably reveal something. |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The Rocq PR rocq-prover/rocq#20985 adds support for generalized rewriting in let-bindings. It changes the basic subrelation instances on eq, iff and impl to avoid proof search blowup.
It seems the change is due to
setoid_rewrite lift_dlet.succeeding more? All the Let_Ins are lifted to toplevel in the example. I don't see why the PR would make a difference here, there are no concretelet x := .. in ..constructs as far as I can see in the goals. @JasonGross can you help me understand what happens here?Could it be the new
subrelation eq iff/impl/(flip impl)instances helping here?