Adds <-, -> and in notation support for the mlRewriteBy tactic.
mlRewriteBy -> ... works the same as mlRewriteBy, it's just for parity.
mlRewriteBy <- ... applies the proof the other way around
mlRewriteBy ... in H applies the proof on a hypothesis instead of the goal. A <- version of this exists as well.
I added a local test to demonstrate the changes.
There is an issue which I'm not sure how to fix: mlRewriteBy ... in H applies the proof on the goal if the hypothesis does not have enough occurrences of the LHS of the proof. Me and @Engreyight tried to experiment with using mlAssert to construct a new hypothesis, but we couldn't find a way to compute the type of the new expression. Another potential solution is checking if H has enough matching subexpressions and failing if it doesn't, but I'm not sure how to do this either.
Adds
<-,->andinnotation support for the mlRewriteBy tactic.mlRewriteBy -> ...works the same asmlRewriteBy, it's just for parity.mlRewriteBy <- ...applies the proof the other way aroundmlRewriteBy ... in Happlies the proof on a hypothesis instead of the goal. A<-version of this exists as well.I added a local test to demonstrate the changes.
There is an issue which I'm not sure how to fix:
mlRewriteBy ... in Happlies the proof on the goal if the hypothesis does not have enough occurrences of the LHS of the proof. Me and @Engreyight tried to experiment with usingmlAssertto construct a new hypothesis, but we couldn't find a way to compute the type of the new expression. Another potential solution is checking ifHhas enough matching subexpressions and failing if it doesn't, but I'm not sure how to do this either.