proposal for new `simp` syntax

Stream: general

[Scott Morrison]

How about being able to write:

simp : T

which fails unless the resulting goal unifies with the type T? This would allow some flexibility with non-terminal simps. It's possible to arrange this already with suffices, but it takes two lines and some boilerplate.

[Scott Morrison]

We could also have simp at h : T to indicate the expected type of the new hypothesis.

[Mario Carneiro]

This looks the same as simp, change T

[Mario Carneiro]

I don't think this makes the simp any less brittle though

[Johan Commelin]

try { simp; change T }?

[Mario Carneiro]

why try?

[Johan Commelin]

Aah, you say that it's enough if the change T fails

[Johan Commelin]

fair enough

[Mario Carneiro]

If simp closes the goal, I guess this would also be a simp : T failure

[Mario Carneiro]

so I think simp, change T is correct

[Mario Carneiro]

except that change T can also do defeq changes, which may or may not be a good idea here, hard to tell

[Mario Carneiro]

I think there is a assert_goal tactic, usually used for tests, that does no defeq changes

[Scott Morrison]

Good points: simp, change T is indeed all that I wanted.

[Scott Morrison]

It's true that this breaks just as often as just a non-terminal simp: the point is that hopefully it's fixable, because even when it's broken you know what state you need to get back to for the rest of the proof to go through.

[Johan Commelin]

I think suffices : T, simpa is a bit more stable

[Yury G. Kudryashov]

The main downside of suffices : T, simpa is that when a new lemma is added to the default simp set, you miss an opportunity to make your proof use it.

[Kenny Lau]

proposal for new simp syntax: don't

[Yury G. Kudryashov]

And with simp, change T or simp, guard_target T you (a) see which simp failed, (b) can choose whether to fix it with simp [-new_lemma] or adjust the proof.

[Mario Carneiro]

you don't know what new_lemma is necessarily though

[Mario Carneiro]

worst case you could squeeze_simp it and then start deleting lemmas until it matches the claim again

[Mario Carneiro]

better is just to use simp only so that this doesn't happen

[Scott Morrison]

simp only still makes me sad, that us poor humans are writing out (even if it's just point and click these days) irrelevant details. I'll live.

[Mario Carneiro]

It's more verbose than it could be, but I think this is what we should be aiming for: a slow but powerful tactic that rewrites itself to a fast but maybe less comprehensible certificate

[Mario Carneiro]

It would be even better if the certificate could be out of the source itself, but it needs to be version controlled which makes things tricky

[Scott Morrison]

certificates in an unobtrusive parallel file would be fantastic :-)

[Mario Carneiro]

I guess the nolints file is a precedent for this approach

[Mario Carneiro]

Here's an architecture that could work without too much in the way of changes to lean: Certificates are kept in some file, indexed by declaration name, like

foo.mythm: CERT
foo.otherthm: CERT2

Then there is a command like load_certificates "foo.cert" that will use IO to read the file and create declarations foo.mythm.cert1 : string := "CERT" (or whatever the appropriate data structure is for the certificate). Finally, fancy_tactic, when used in foo.mythm, checks if definition foo.mythm.cert1 exists, and if so uses the certificate. For this last part I think we need extra support because tactics don't have access to the currently elaborating definition IIUC.

[Yury G. Kudryashov]

Mario Carneiro said:

you don't know what new_lemma is necessarily though

If we're talking about code in mathlib, then the one who adds a lemma fixes all compile failures.

[Mario Carneiro]

assuming the change is small enough that it is easy to locate which new lemma is the culprit

[Mario Carneiro]

if the code is being rehabilitated, the problem is much worse

[Mario Carneiro]

The certificate file could also be a machine generated lean source file, like

theorem foo.mythm.cert1 : technical lemma := by fancy_tactic using incomprehensible_sequence_of_characters

[Bryan Gin-ge Chen]

Is this similar to #2300?

[Scott Morrison]

#2300 is doing something related, but a bit crazy. It is (I think) serialising the proof term generated by each begin ... end block into a file on disk, and the next time the begin ... end block is compiled it intercepts that and attempts to just load the previous term from disk and typecheck it.

[Mario Carneiro]

You could use exprs as the certificate but I'm assuming that particular tactics can do a lot better with smaller certificates, like the lemma list in simp only

[Kevin Buzzard]

The advantage of simp : T over suffices : T, by simpa using this is that when the proof breaks it's easy to fix (by switching back to suffices) but there's also the option to improve the proof.