What is "⊢"?

Stream: new members

[Bbbbbbbbba]

This is a MWE (that I know could be proved in many other ways):

import Mathlib

example (a b : Prop) (hab : a → b) : ¬(a ∧ ¬b) := by
  simp
  exact hab

When I try this in my local Lean setup, Lean warns me that

'simp' is a flexible tactic modifying '⊢'. Try 'simp?' and use the suggested 'simp only [...]'. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`

and (as a normal message, not a warning)

'exact hab' uses '⊢'!

I understand that Lean has given me instructions to resolve the warning, but I am just curious what "⊢" means.

[Riccardo Brasca]

⊢ is the goal (the theorem you are proving). The warning is telling you that simp is modifying the goal: the warning exists because your proof is not very robust, maybe one day simp will become smarter and be able to finish the proof, so the line exact hab will give an error.

[Bbbbbbbbba]

Well isn't that technically true for simp only too? Even with a limited set of lemmas it might be possible to use them more effectively.

[Riccardo Brasca]

Yes, technically the lemmas listed in simp only can change in the future, but this is much less likely than a simp lemma being added and simp getting smarter (in your particular case both scenario are more or less impossible). Anyway it is just a warning, you can ignore it or deactivate the linter if it bothers you (it is active in mathlib though).

[Damiano Testa]

Also, if a simp only breaks, there is a very small list of candidates for what could have caused the issue. With a plain simp, the list is potentially the whole simp set.

[Damiano Testa]

So, things can (and will) still break, though hopefully less and in ways that are easier to fix.