Zulip Chat Archive

Stream: new members

Topic: do tactics change?


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 10 2020 at 19:33):

Yes

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Golol (May 10 2020 at 19:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Alex J. Best (May 10 2020 at 19:48):

What do you mean by lower level?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 10 2020 at 19:53):

and lean 4 is definitely "major breakage"

view this post on Zulip Golol (May 10 2020 at 19:56):

Oh that sounds like transferring will be a mess lol.

view this post on Zulip Mario Carneiro (May 10 2020 at 19:56):

we'll cross that bridge when we come to it

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 10 2020 at 19:58):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 19:59):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 10 2020 at 20:10):

Users can pick up good habits later :P

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 10 2020 at 20:19):

This discussion about { } is cycling again...


Last updated: May 14 2021 at 06:16 UTC