Zulip Chat Archive

Stream: new members

Topic: do tactics change?


Golol (May 10 2020 at 19:33):

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

Kevin Buzzard (May 10 2020 at 19:33):

Yes

Kevin Buzzard (May 10 2020 at 19:34):

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 (May 10 2020 at 19:35):

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

Jalex Stark (May 10 2020 at 19:36):

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 (May 10 2020 at 19:37):

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

Mario Carneiro (May 10 2020 at 19:41):

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 (May 10 2020 at 19:42):

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 (May 10 2020 at 19:43):

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

Mario Carneiro (May 10 2020 at 19:44):

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 (May 10 2020 at 19:47):

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 (May 10 2020 at 19:48):

What do you mean by lower level?

Mario Carneiro (May 10 2020 at 19:48):

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 (May 10 2020 at 19:49):

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 (May 10 2020 at 19:50):

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 (May 10 2020 at 19:51):

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 (May 10 2020 at 19:51):

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

Mario Carneiro (May 10 2020 at 19:53):

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 (May 10 2020 at 19:53):

and lean 4 is definitely "major breakage"

Golol (May 10 2020 at 19:56):

Oh that sounds like transferring will be a mess lol.

Mario Carneiro (May 10 2020 at 19:56):

we'll cross that bridge when we come to it

Golol (May 10 2020 at 19:57):

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 (May 10 2020 at 19:58):

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

Mario Carneiro (May 10 2020 at 19:59):

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

Mario Carneiro (May 10 2020 at 20:00):

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

Kevin Buzzard (May 10 2020 at 20:10):

Users can pick up good habits later :P

Mario Carneiro (May 10 2020 at 20:17):

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 (May 10 2020 at 20:19):

This discussion about { } is cycling again...


Last updated: Dec 20 2023 at 11:08 UTC