Zulip Chat Archive

Stream: general

Topic: proposal for new `simp` syntax


view this post on Zulip Scott Morrison (May 31 2020 at 06:43):

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.

view this post on Zulip Scott Morrison (May 31 2020 at 06:43):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 06:46):

This looks the same as simp, change T

view this post on Zulip Mario Carneiro (May 31 2020 at 06:47):

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

view this post on Zulip Johan Commelin (May 31 2020 at 06:47):

try { simp; change T }?

view this post on Zulip Mario Carneiro (May 31 2020 at 06:47):

why try?

view this post on Zulip Johan Commelin (May 31 2020 at 06:47):

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

view this post on Zulip Johan Commelin (May 31 2020 at 06:47):

fair enough

view this post on Zulip Mario Carneiro (May 31 2020 at 06:48):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 06:48):

so I think simp, change T is correct

view this post on Zulip Mario Carneiro (May 31 2020 at 06:48):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 06:49):

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

view this post on Zulip Scott Morrison (May 31 2020 at 06:58):

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

view this post on Zulip Scott Morrison (May 31 2020 at 06:59):

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.

view this post on Zulip Johan Commelin (May 31 2020 at 07:09):

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

view this post on Zulip Yury G. Kudryashov (May 31 2020 at 07:27):

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.

view this post on Zulip Kenny Lau (May 31 2020 at 07:29):

proposal for new simp syntax: don't

view this post on Zulip Yury G. Kudryashov (May 31 2020 at 07:30):

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.

view this post on Zulip Mario Carneiro (May 31 2020 at 07:35):

you don't know what new_lemma is necessarily though

view this post on Zulip Mario Carneiro (May 31 2020 at 07:35):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 07:36):

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

view this post on Zulip Scott Morrison (May 31 2020 at 07:41):

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.

view this post on Zulip Mario Carneiro (May 31 2020 at 07:42):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 07:43):

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

view this post on Zulip Scott Morrison (May 31 2020 at 07:54):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 07:55):

I guess the nolints file is a precedent for this approach

view this post on Zulip Mario Carneiro (May 31 2020 at 08:00):

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.

view this post on Zulip Yury G. Kudryashov (May 31 2020 at 08:00):

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.

view this post on Zulip Mario Carneiro (May 31 2020 at 08:01):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 08:01):

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

view this post on Zulip Mario Carneiro (May 31 2020 at 08:03):

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

view this post on Zulip Bryan Gin-ge Chen (May 31 2020 at 08:16):

Is this similar to #2300?

view this post on Zulip Scott Morrison (May 31 2020 at 08:22):

#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.

view this post on Zulip Mario Carneiro (May 31 2020 at 08:33):

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

view this post on Zulip Kevin Buzzard (May 31 2020 at 08:43):

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.


Last updated: May 17 2021 at 21:12 UTC