simp with left arrow

Stream: general

[Jeremy Avigad]

In the middle of a complicated proof, I have come across a situation where a tactic of the form

    simp only [h0, h1.symm, h2]

succeeds but

   simp only [h0, ←h1, h2]

fails. All the arguments are explicit equations between elements of a field. The expressions aren't very complicated; they involve +, -, and function application, and as far as I can tell there are no implicit arguments except for the field and has_add and friends.

I am having a hard time producing a small counterexample. Absurdly, if I use extract_goal to extract a lemma with exactly the same (very large) context, both versions work.

Using symm is fine as a workaround, but I am curious: has anyone seen something like this before?

[Mario Carneiro]

The two are not exactly equivalent. simp [← thm] should be roughly equivalent to simp [thm.symm, -thm], but using thm.symm means only one set of metavariables is created so it can only be applied at one substitution. Without more details about the example it's hard to say which of those things is making the difference

[Mario Carneiro]

Oh, another reason for a difference in the other direction is if h1 is an instantiated metavariable then simp might not think it is an equality, but h1.symm is an equality

[Jeremy Avigad]

Aha! The second one explains it. Here's a small example:

lemma this_works (a b c d : nat) (h0 : a = b) (h1 : b = c) (h2 : c = d) : a = d :=
begin
  have h3 : b = _,
  { exact eq.trans h1 h2 },
  simp only [h0, h3.symm],
end

lemma this_fails (a b c d : nat) (h0 : a = b) (h1 : b = c) (h2 : c = d) : a = d :=
begin
  have h3 : b = _,
  { exact eq.trans h1 h2 },
  simp only [h0, ←h3],
end

Many thanks for clearing that up. I was really curious as to what was going on. It's good to know that simp doesn't see the instantiations.