feat(library/init/meta/simp_tactic) simp with reversed lemmas
#100
Conversation
|
I'm currently compiling the full |
Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
…mpatible The problem is that some tactics in `mathlib` extending `simp` do not handle the `symm` argument, so by introducing the new behavior under a new name and erroring out when `symm` is found in the old behavior, calls (but not pattern-matching) shouldn't break too much.
In `mathlib`, a similar function was used by `squeeze_simp`, but changes in the definition for `simp_arg_type` will break this. This solution adds a polyfill instance in `mathlib` with low priority and the "real" instance with high priority in the new version of core Lean.
If there is a `lemma @[simp] foo` and we call `simp [<-foo]`, this would give a timeout because it will start rewriting back and forth from LHS to RHS. To avoid this, we delete all `foo`s coming from annotations when collecting lemmas for `simp [<-foo]`.
|
After updating to the master branch, mathlib builds with no errors! I've added some code to prevent conflicts between forwards and backwards rewriting rules (preventing an infinite loop of rewriting back-and-forth): if there is a But I just realized that this doesn't solve all conflicts: if for whatever reason there is a |
Yes, I think this is up to the user. You can already very easily make simp loop by calling |
Yes, I think this is up to the user. You can already very easily make simp loop by calling LGTM. |
|
What's going on with the build? |
|
@cipher1024 From what I can tell, something went wrong here causing |
|
This is a bit surprising, the CI worked on the PR. |
|
See #116. |
Pull Request Description
Allow the
simptactic to apply reverse direction, analogously torw: ifh : a = b, thensimp [<-h]will replace all instances ofbin the goal witha.This implementation is inspired by
rewrite: we store a flag for eachexprlemma passed tosimp, indicating whether to reverse it. When all parameters to the lemma have been instantiated (so that the lemma has the formh _ ... _ : R _ _,mk_symmis applied to it to get the reverse relation.