Recent Changes

Stream: general

[Rosie Baish]

I've got some code from 2022 which mostly uses the syntax/style of

theorem foo f <-> g := by {
  apply Iff.intro;
  case mp => {
    sorry;
  }
  case mpr => {
    sorry;
  }
}

I've reopened this code to make a couple of minor changes, and the whole thing is throwing syntax errors
If I take out all the braces and all the semicolons it works.
ChatGPT says there was a recent breaking change around this, but I can't figure out where in the docs that is.
Can anyone point me in the right direction, or is ChatGPT hallucinating again?

[Jon Eugster]

maybe

https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users

and

https://lean-lang.org/lean4/doc/lean3changes.html

?

[Rosie Baish]

I had a look at that, but neither offers a conclusive answer
This is the closest: https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users#:~:text=If%20you%20have%20multiple%20goals%2C%20you%20can%20work%20on%20the%20first%20goal%20using%20%C2%B7%20%3Ctactics%3E%20instead%20of%20%7B%3Ctactics%3E%7D.%20Note%20that%20%C2%B7%20is%20%5C.%2C%20not%20%5Ccdot.

[Rosie Baish]

The thing that particularly confuses me is that this code worked in Lean4 3ish years ago, but now doesn't

[Yury G. Kudryashov]

Can you post a #mwe?

[Yury G. Kudryashov]

(in this case, a minimal non-working example)

[Rosie Baish]

theorem test_lemma {x : Prop} : ¬ x ↔ x = False :=
by {
  apply Iff.intro;
  case mp => {
    intro temp;
    apply eq_false;
    exact temp;
  }
  case mpr => {
    intro temp;
    rw[temp];
    simp;
  }
}

This code was committed to my repo in May 2023 and the proof succeeded. (So presumable there were no syntax errors
When opening it again today, VS code gives me the following 3 errors, all on the "case mp" line:
unexpected syntax
case mp => {intro temp; apply eq_false; exact temp;
}

this tactic is never executed
note: this linter can be disabled with set_option linter.unreachableTactic false

'case mp => {intro temp; apply eq_false; exact temp;
}' tactic does nothing
note: this linter can be disabled with set_option linter.unusedTactic false

It also gives me the "tactic does nothing" and "never executed" warnings on the "case mpr" line, but no syntax error. (Presumably because it can't continue finding errors after a parse fail?)

[Shreyas Srinivas]

theorem test_lemma {x : Prop} : ¬ x ↔ x = False :=
by {
  apply Iff.intro;
  · {
    intro temp;
    apply eq_false;
    exact temp;
  }

  · {
    intro temp;
    rw[temp];
    simp;
  }
}

[Shreyas Srinivas]

Basically for reasons beyond me, apply Iff.intro introduced two unnamed goals

[Shreyas Srinivas]

thus case mp and case mpr are not selecting these goals. Otherwise your syntax is fine, although not typical.

[Shreyas Srinivas]

Of course, if you only want to select the goals, you can also just skip the \. selectors:

theorem test_lemma {x : Prop} : ¬ x ↔ x = False :=
by {
  apply Iff.intro;
  {
    intro temp;
    apply eq_false;
    exact temp;
  }

  {
    intro temp;
    rw[temp];
    simp;
  }
}

[Shreyas Srinivas]

Opening braces seems to focus proof mode on the first goal

[Rosie Baish]

Once I remove all the brackets and semicolons it works, and has 2 named goals as mp and mpr
I've just accepted that I don't understand what's going on and re-syntaxed my entire proof

[Sebastian Ullrich]

Essentially no-one is using the braced syntax so I'm not too surprised it broke at some point without anyone noticing. You can file an issue, but switching to indentation-based syntax is the much better option, yes.

[Bhavik Mehta]

A simpler fix would just be to remove the braces from your code, then it works:

theorem test_lemma {x : Prop} : ¬ x ↔ x = False :=
by
  apply Iff.intro;
  case mp =>
    intro temp;
    apply eq_false;
    exact temp;
  case mpr =>
    intro temp;
    rw[temp];
    simp;

[Bhavik Mehta]

Shreyas Srinivas said:

Basically for reasons beyond me, apply Iff.intro introduced two unnamed goals

I don't think this is true, it's introducing two named goals, and I can select them as above. But perhaps you got misled (by the same thing that's misled me in the past): #general > lean4.infoview.showGoalNames is false in the web editor

[Rosie Baish]

Sebastian Ullrich said:

switching to indentation-based syntax is the much better option, yes.

I did exactly this, and removed all the semicolons at the end of lines, which I believe were also unnecessary and did nothing

[Shreyas Srinivas]

Bhavik Mehta said:

I don't think this is true, it's introducing two named goals, and I can select them as above. But perhaps you got misled (by the same thing that's misled me in the past): #general > lean4.infoview.showGoalNames is false in the web editor

Yes I think this was the issue. But I was able to get the braces syntax working after removing the explicit case mp and case mpr selectors as shown above.

The braced syntax still works

[Shreyas Srinivas]

Specifically here :

Shreyas Srinivas said:

Of course, if you only want to select the goals, you can also just skip the \. selectors:

theorem test_lemma {x : Prop} : ¬ x ↔ x = False :=
by {
  apply Iff.intro;
  {
    intro temp;
    apply eq_false;
    exact temp;
  }

  {
    intro temp;
    rw[temp];
    simp;
  }
}

[Mario Carneiro]

Poking into this issue a bit more specifically, it appears that case x => {} is the part that fails. It's not a syntax error, but rather there is no elaborator found for the syntax. It's the same message you get from

macro "foo" : tactic => Lean.Macro.throwUnsupported
#check by foo
-- unexpected syntax
--   foo

[Mario Carneiro]

And when looking at the elaborator it's pretty clear why this happens:

@[builtin_tactic «case», builtin_incremental]
def evalCase : Tactic
  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
    ...
  | _ => throwUnsupportedSyntax

[Mario Carneiro]

this seems to be the only direct use of tacticSeq1Indented in the codebase, so I don't think there are any other errors like it lurking

[Mario Carneiro]

the bug was introduced in lean4#3940 (cc: @Sebastian Ullrich ) as part of incremental tactic elaboration for case

[Mario Carneiro]

I think it was just done so that the argIdx := 3 part is correct (the index is different for bracketed syntax), so the fix should be easy

[Patrick Massot]

Mario means lean4#3940