You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Should we add a check that all binded variables occurs in lhs and fail or at least add a warning if it is not the case.
Context
Since #1110, EcReduction.User.compile compiles a lemma into one rule per conjunct. For each conjunct, mkleaf (src/ecReduction.ml, module User) silently drops the binders of the enclosing forall that the conjunct does not mention at all (in its left-hand side, right-hand side, or conditions). This is sound, and it is what makes
axiom rsE (x y : int) : r x = x + 3 /\ s y = y + 4.
hint simplify rsE.
register two rules instead of failing with MissingVarInLhs on each conjunct.
The existing check is unchanged for binders that do occur in the conjunct: a binder found in the right-hand side or in a condition but not in the left-hand side still raises MissingVarInLhs.
Question
Should a binder that occurs nowhere in a conjunct be reported, either as an error or as a warning, rather than dropped silently? Arguments:
For: a quantified variable unused by a conjunct is usually a sign the lemma is not stated the way the user intended, and the pre-hint simplify registers one rule per conjunct of a lemma #1110 behaviour for a single-equation lemma with an unused binder was to fail.
Against: the stated goldbach use case (forall x y, r x = … /\ s y = …) is a legitimate way to group rules under one quantifier prefix, and an error there would force users back to one lemma per equation.
A warning (with a per-command option to silence it, or only when the binder is unused by every conjunct) may be the right middle ground.
From a review comment by @bgregoir on PR #1110 (#1110 (comment)):
Context
Since #1110,
EcReduction.User.compilecompiles a lemma into one rule per conjunct. For each conjunct,mkleaf(src/ecReduction.ml,module User) silently drops the binders of the enclosingforallthat the conjunct does not mention at all (in its left-hand side, right-hand side, or conditions). This is sound, and it is what makesregister two rules instead of failing with
MissingVarInLhson each conjunct.The existing check is unchanged for binders that do occur in the conjunct: a binder found in the right-hand side or in a condition but not in the left-hand side still raises
MissingVarInLhs.Question
Should a binder that occurs nowhere in a conjunct be reported, either as an error or as a warning, rather than dropped silently? Arguments:
hint simplifyregisters one rule per conjunct of a lemma #1110 behaviour for a single-equation lemma with an unused binder was to fail.forall x y, r x = … /\ s y = …) is a legitimate way to group rules under one quantifier prefix, and an error there would force users back to one lemma per equation.A warning (with a per-command option to silence it, or only when the binder is unused by every conjunct) may be the right middle ground.