do tactics change?

Stream: new members

[Golol]

Are tactics ever modified? Could a tactics proof become invalid after an update that changes a detail about simp?

[Kevin Buzzard]

Yes

[Kevin Buzzard]

The simp algorithm itself is not modified, but tagging lemmas with simp happens all the time, and changes the way simp behaves. This is why it is not recommended to use simp in the middle of a proof, but only to close a goal, because the philosophy is that simp should only get better.

[Golol]

Okay. So form a perfectionist view a library should at least store the term-style proofs, because these can never become invalid.

[Jalex Stark]

Golol said:

Okay. So form a perfectionist view a library should at least store the term-style proofs, because these can never become invalid.

Tactics aren't the only things that change

but in practice I think mathlib likes to have compact term-mode proofs because they run faster

[Golol]

Ah okay, then nevermind. There probably isnt a risk to "break everything".

[Mario Carneiro]

It's certainly possible to "break everything". For example if you changed the definition of eq you could probably get over 90% of mathlib to break

[Mario Carneiro]

The way we deal with this is "if you break it you fix it". So you are incentivized not to make changes that cause large breakage unless you are personally motivated enough about the change to fix the breakage

[Mario Carneiro]

(also, obviously there should be some kind of consensus that the change is a good one, especially if there is large breakage)

[Mario Carneiro]

Much more commonly, a minor change breaks some 2 or 10 theorems and it's not a big deal to repair them as part of the PR that makes the change

[Golol]

What kind of changes are we talking about here, changes to the lean code itself or changes to lower level definitions and theorems?

[Alex J. Best]

What do you mean by lower level?

[Mario Carneiro]

But it's not really true that term mode proofs are less prone to breakage than tactic proofs. One advantage of tactic proofs, especially those using "heavy" tactics like simp, ring or finish is that they don't care too much about the form of the goal statement, and can ride along with many kinds of simple changes to the library, while term proofs are pretty directly tied to the exact form of all the statements that were used. So something like changing the order of arguments, changing typeclass instances, removing an unnecessary argument are all more likely to break a term mode proof than a tactic proof

[Mario Carneiro]

The price "heavy" tactics pay for their flexibility is that they tend to be slower, because you don't know in advance what the proof is going to look like

[Golol]

Alex J. Best said:

What do you mean by lower level?

Maybe someone changes a detail about the definition of a Ring (bad example) and some theorem breaks. But I was more interested in changes to the code that verifies a term-style proof.

[Mario Carneiro]

Golol said:

What kind of changes are we talking about here, changes to the lean code itself or changes to lower level definitions and theorems?

Changes to mathlib (the library of proven results in lean) are much more common than changes to elaboration or C++ details like that

[Mario Carneiro]

and we have to be pretty conservative about C++ changes exactly because they tend to have large breakage

[Mario Carneiro]

It "helps" that the person who was mostly responsible for writing that code has left to work on lean 4 so no one else wants to touch it

[Mario Carneiro]

and lean 4 is definitely "major breakage"

[Golol]

Oh that sounds like transferring will be a mess lol.

[Mario Carneiro]

we'll cross that bridge when we come to it

[Golol]

I just noticed I was basically spamming tactics till it clicks in the natural number game. If the way tactics apply themselves changed slightly my proofs could be wrong :D.

[Mario Carneiro]

that's because NNG doesn't teach how to write structured proofs

[Mario Carneiro]

if you submitted a proof like that to mathlib it would be excoriated (probably by me)

[Mario Carneiro]

The easiest thing to start with is to always use { } around the branches after a tactic that creates multiple subgoals

[Kevin Buzzard]

Users can pick up good habits later :P

[Mario Carneiro]

Actually, it shouldn't be too bad to introduce it early in NNG, emphasizing that it's optional; I'm sure there are some people who like their proofs to look professional but they can't use { } if it is never even mentioned to exist.

[Patrick Massot]

This discussion about { } is cycling again...