## Stream: general

### Topic: proposal for new simp syntax

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

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

#### Mario Carneiro (May 31 2020 at 06:46):

This looks the same as simp, change T

#### Mario Carneiro (May 31 2020 at 06:47):

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

#### Johan Commelin (May 31 2020 at 06:47):

try { simp; change T }?

#### Mario Carneiro (May 31 2020 at 06:47):

why try?

#### Johan Commelin (May 31 2020 at 06:47):

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

fair enough

#### Mario Carneiro (May 31 2020 at 06:48):

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

#### Mario Carneiro (May 31 2020 at 06:48):

so I think simp, change T is correct

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

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

#### Scott Morrison (May 31 2020 at 06:58):

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

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

#### Johan Commelin (May 31 2020 at 07:09):

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

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

#### Kenny Lau (May 31 2020 at 07:29):

proposal for new simp syntax: don't

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

#### Mario Carneiro (May 31 2020 at 07:35):

you don't know what new_lemma is necessarily though

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

#### Mario Carneiro (May 31 2020 at 07:36):

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

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

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

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

#### Scott Morrison (May 31 2020 at 07:54):

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

#### Mario Carneiro (May 31 2020 at 07:55):

I guess the nolints file is a precedent for this approach

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

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

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

#### Mario Carneiro (May 31 2020 at 08:01):

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

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


#### Bryan Gin-ge Chen (May 31 2020 at 08:16):

Is this similar to #2300?

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

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

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