possible `rewrite` bug

Stream: general

[Scott Howard]

I think I may have found a weird bug while messing about with rewrite.

Specifically, I was going through @Kevin Buzzard's ImperialCollegeLondon/formalising-mathematics repo and wanted to be cute with a solution in the file ./src/week_1/Part_A_logic.lean. The "cute" solution in question was:

Spoilered for those who want to go through the repo exercises

theorem or.left_comm : P ∨ Q ∨ R ↔ Q ∨ P ∨ R :=
begin
  split;
  intro h;
  rw ←or.assoc at *;
  rw or.comm Q at *;
  rw or.assoc at *;
  exact h,
end

The above is just fine (if a bit obtuse, which I guess was my intent...). The problem arises when trying to use sequential syntax, like so:

theorem or.left_comm : P ∨ Q ∨ R ↔ Q ∨ P ∨ R :=
begin
  split;
  intro h;
  rw [←or.assoc, or.comm Q, or.assoc] at *;
  exact h,
end

This now fails to rw or.assoc at h on the → case, but succeeds on the conclusion, and succeeds on both statements in the ← case.

This project was on an older version of Lean/mathlib, but I leanproject up'd it just to make sure, and it still fails. I was wondering if this was actually a bug, or if there's something I'm missing. I suspect there might just be some weirdness as to how rw [...] interacts with the semicolon or something; I can't say for sure, though.

[Mario Carneiro]

Could you make a self-contained example?

[Scott Howard]

I can try, give me a moment.

[Mario Carneiro]

I would blame rw at * here, this is a rather weird operation since it requires that the rewrite sequence applies to everything in the context

[Mario Carneiro]

that is, rw a at *; rw b at * is not equivalent to rw [a, b] at * because both a and b have to apply to every hypothesis that is rewritten, while in the separated version they can rewrite a different set of assumptions

[Mario Carneiro]

if you replace * with the appropriate set of hypotheses it should work

[Scott Howard]

I guess the thing I'm finding strange is that h in the first case is identical to the conclusion in the second, but the problem only shows up with the h. I'll try what you said, however, that might indeed be the problem.

[Mario Carneiro]

without an #mwe it's hard to follow along here, I'm speculating based on the proof script

[Scott Howard]

I'll get something together. Just juggling a thing or two, shouldn't be too long

[Mario Carneiro]

If you are just interested in a slick proof, there is no need to split in the first place. rw [← or.assoc, or.comm Q, or.assoc] should work

[Scott Howard]

MWE:

Spoilered for those who want to go through the repo exercises

import tactic

namespace test

variables (P Q R : Prop)

theorem or.assoc : (P ∨ Q) ∨ R ↔ P ∨ Q ∨ R :=
begin
  split,
  { rintro ((hp | hq) | hr),
    { left, exact hp },
    { right, left, exact hq },
    { right, right, exact hr }},
  { rintro (hp | hq | hr),
    { left, left, exact hp },
    { left, right, exact hq },
    { right, exact hr }},
end

theorem or.comm : P ∨ Q ↔ Q ∨ P :=
begin
  split,
  { rintro (hp | hq),
    { right, exact hp },
    { left, exact hq }},
  { rintro (hq | hp),
    { right, exact hq },
    { left, exact hp }},
end

theorem or.left_comm : P ∨ Q ∨ R ↔ Q ∨ P ∨ R :=
begin
  split;
  intro h;
  rw [←or.assoc, or.comm Q, or.assoc] at *;
  exact h,
end

end test

Same behavior shows up, but the error hits earlier, in the way you describe, if I instead use the default or.assoc and or.comm from base Lean.

So I'm satisfied it shouldn't work anyway, but I'm confused why this difference in behavior.

[Scott Howard]

Thanks for taking a look and letting me know about that, by the way---I didn't know that subtlety of rw.

[Mario Carneiro]

I'm not sure whether it is considered a bug, but I have narrowed down the unusual behavior here to the try_lst function:

meta def try_lst : list (tactic unit) → tactic unit
| []            := failed
| (tac :: tacs) := λ s,
  match tac s with
  | success _ s' := try (try_lst tacs) s'
  | exception e p s' :=
    match try_lst tacs s' with
    | exception _ _ _ := exception e p s'
    | r := r
    end
  end

The odd part here is that in the exception e p s' case we continue with the rest of the tactics using the exception state: try_lst tacs s'. This is a weird thing to do, because the exception state is usually some intermediate state and continuing from there can lead to unpredictable behavior. Most of the time you would roll back the state, i.e. using try_lst tacs s in this function.

It manifests in the example like so:

example {P Q R} (h : P ∨ Q ∨ R) : Q ∨ P ∨ R :=
begin
  rw [← or.assoc, @or.comm Q, or.assoc] at *,
  -- h: (P ∨ Q) ∨ R
  -- ⊢ P ∨ Q ∨ R
end

What happens here is that we try to run rw [← or.assoc, @or.comm Q, or.assoc] at h and rw [← or.assoc, @or.comm Q, or.assoc] together using try_lst. For the first call, we do rw ← or.assoc at h, turning h into (P ∨ Q) ∨ R, and then attempt to rw @or.comm Q at h which fails. The try_lst catches the failure, using the partially rewritten h, and then continues with rw ← or.assoc, rw @or.comm Q, and rw or.assoc which all succeed, resulting in the state h: (P ∨ Q) ∨ R ⊢ P ∨ Q ∨ R.

[Scott Howard]

I see. A good reason to make sure that the list really does match against everything you want to hit with it. Thanks a bunch!