Is your feature request related to a problem?
This issue pitches the implementation of a feature described in the following Zulip thread.
In the thread linked, @mattam82 pitches a new rewrite strategy combinator, solve to do explicitly what rewrite_strat currently does implicitly. Given a rewrite strategy, rewrite_strat first traverses the term it needs to rewrite in the order specified by the provided strategy and as many time as specified, finding subterms to rewrite as it goes along. Second, once the traversals are done and the equivalence proofs are gathered for the subterms, rewrite_strat looks instances of Proper that will help it combine the proofs of equivalence of subterms into a single proof.
We would like to make this phase separation optional. In some cases, it may be preferable to find Proper instances during the term traversal. It may, for instance, cut out the traversal of subterms if the no Proper instance were to allow us to combine a rewriting of the subterms with the rewriting of other subterms.
With the current version of rewrite_strat, when Proper instances are missing, rewrite_strat as a whole fails. If the right instance of Proper cannot be proven for whatever reason (e.g. the available rules use equiv but Proper instances can only be proven when using eq as rewrite relation), this prevents us from using rewrite_strat altogether.
Proposed solution
We propose to change rewrite_strat in the following ways.
- When traversing a term for the first time, we build appropriate
Proper instances as we go. This means that most rewriting problems can now be formulated as the pair form of a term to rewrite and the relation that the rewrite rule needs to use.
- Define the new rewrite strategy combinator
solve: solve foo separates the traversal phase from the resolution of Proper constraints.
- Combinators
subterm and subterms:
a. used in a context where the expected rewrite relation is known, propagates that information downward by solving Proper constraints; any subterm for which no rewrite relation is provided by the available Proper instances is not traversed;
b. in a context where the expected rewrite relation is not known, or right under a solve combinator, behave the same as in the current version of rewrite_strat.
Alternative solutions
When Proper instances are missing but provable, Set Rewrite Output Constraints can be used to find out which one is missing. If the requires instances cannot be proven, we need to remove from the rewrite database the set of equations that could be applicable in subterms whose rewriting cannot be supported.
Additional context
No response
Is your feature request related to a problem?
This issue pitches the implementation of a feature described in the following Zulip thread.
In the thread linked, @mattam82 pitches a new rewrite strategy combinator,
solveto do explicitly whatrewrite_stratcurrently does implicitly. Given a rewrite strategy,rewrite_stratfirst traverses the term it needs to rewrite in the order specified by the provided strategy and as many time as specified, finding subterms to rewrite as it goes along. Second, once the traversals are done and the equivalence proofs are gathered for the subterms,rewrite_stratlooks instances ofProperthat will help it combine the proofs of equivalence of subterms into a single proof.We would like to make this phase separation optional. In some cases, it may be preferable to find
Properinstances during the term traversal. It may, for instance, cut out the traversal of subterms if the noProperinstance were to allow us to combine a rewriting of the subterms with the rewriting of other subterms.With the current version of
rewrite_strat, whenProperinstances are missing,rewrite_stratas a whole fails. If the right instance ofPropercannot be proven for whatever reason (e.g. the available rules useequivbutProperinstances can only be proven when usingeqas rewrite relation), this prevents us from usingrewrite_strataltogether.Proposed solution
We propose to change
rewrite_stratin the following ways.Properinstances as we go. This means that most rewriting problems can now be formulated as the pair form of a term to rewrite and the relation that the rewrite rule needs to use.solve:solve fooseparates the traversal phase from the resolution ofProperconstraints.subtermandsubterms:a. used in a context where the expected rewrite relation is known, propagates that information downward by solving
Properconstraints; any subterm for which no rewrite relation is provided by the availableProperinstances is not traversed;b. in a context where the expected rewrite relation is not known, or right under a
solvecombinator, behave the same as in the current version ofrewrite_strat.Alternative solutions
When
Properinstances are missing but provable,Set Rewrite Output Constraintscan be used to find out which one is missing. If the requires instances cannot be proven, we need to remove from the rewrite database the set of equations that could be applicable in subterms whose rewriting cannot be supported.Additional context
No response