hint simplify registers one rule per conjunct of a lemma - #1110
Merged
Conversation
strub
force-pushed
the
hint-simplify-conj
branch
3 times, most recently
from
September 4, 2026 13:05
7240de1 to
fafb906
Compare
strub
force-pushed
the
hint-simplify-conj
branch
from
September 4, 2026 13:29
fafb906 to
27bda38
Compare
bgregoir
approved these changes
Sep 4, 2026
A lemma whose body is a conjunction of rewrite rules used to compile to a single eq-true rule whose pattern was the whole conjunction, rooted at `(/\)`. It registered without error and never fired: the only way to feed the simplifier a family of equations was one lemma and one hint line per equation. `EcReduction.User.compile` now splits the body recursively and returns a rule list. Implications distribute their condition over every rule beneath them, conjunctions contribute both sides, and a conjunct may carry its own `forall`. Each rule keeps only the binders occurring in its conjunct, so a shared outer binder that one conjunct does not mention no longer trips the missing-variable check. The `Th_reduction` entry carries a rule list per lemma (empty meaning "not compiled"), so printing and cloning replay keep working per lemma name.
strub
force-pushed
the
hint-simplify-conj
branch
2 times, most recently
from
September 4, 2026 13:48
27bda38 to
af48d67
Compare
strub
enabled auto-merge
September 4, 2026 13:53
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.
A lemma whose body is a conjunction of rewrite rules used to compile to
a single eq-true rule whose pattern was the whole conjunction, rooted at
(/\). It registered without error and never fired: the only way tofeed the simplifier a family of equations was one lemma and one hint
line per equation.
EcReduction.User.compilenow splits the body recursively and returnsa rule list. Implications distribute their condition over every rule
beneath them, conjunctions contribute both sides, and a conjunct may
carry its own
forall. Each rule keeps only the binders occurring inits conjunct, so a shared outer binder that one conjunct does not
mention no longer trips the missing-variable check. The
Th_reductionentry carries a rule list per lemma (empty meaning "not compiled"), so
printing and cloning replay keep working per lemma name.