Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simp ignores direction of equation lemmas #623

Open
1 task done
eric-wieser opened this issue Sep 21, 2021 · 0 comments
Open
1 task done

simp ignores direction of equation lemmas #623

eric-wieser opened this issue Sep 21, 2021 · 0 comments

Comments

@eric-wieser
Copy link
Member

eric-wieser commented Sep 21, 2021

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

When working with equation lemmas, simp only [←my_add] behaves as if it were simp only [my_add]: the is ignored.

Steps to Reproduce

def my_add (a b : nat) := a + b

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  success_if_fail { simp only },  -- ok, nothing to simplify
  exact nat.sub_self _,
end

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  simp only [my_add],
  guard_target a + b - (a + b) = 0, -- ok
  exact nat.sub_self _,
end

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  simp only [←my_add],
  guard_target my_add a b - my_add a b, -- fail, goal is as if the `←` isn't there
  exac nat.sub_self _,
end

Expected behavior: [What you expect to happen]

The above code should produce no diagostics

Actual behavior: [What actually happens]

The final guard_target fails, as the goal is a + b - (a + b) = 0. Despite being told not to, simp unfolded my_add.

@eric-wieser eric-wieser changed the title simp ignores directly of equation lemmas simp ignores direction of equation lemmas Sep 21, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant