Zulip Chat Archive

Stream: general

Topic: sorry weirdness


Patrick Massot (Feb 22 2022 at 16:17):

I recently became convinced to replace my habit of commenting out pieces of working proofs in a long proof by use the sorry ; {} trick. For instance let's look at:

example : 1 = 1  2 = 2 :=
begin
  split,
  { refl },
  { refl },
end

Say the first proof is too long to check for my taste when I'm working on the second proof. I used to do

example : 1 = 1  2 = 2 :=
begin
  split,
  /- { refl } -/sorry,
  { refl },
end

while working on the second part. But people told me I should switch to

example : 1 = 1  2 = 2 :=
begin
  split,
  sorry ; { refl },
  { refl },
end

However doing that make the second goal disappear when the cursor is at the end of the first line (or the beginning of the second line), which is very weird and confusing.

Patrick Massot (Feb 22 2022 at 16:18):

Does anyone has an explanation and some way to save that sorry ; trick?

Eric Rodriguez (Feb 22 2022 at 16:24):

huh, this is really annoying; I think it's because the ; combinator mode is so bugged in lean3. skip, sorry; seems to recover better behaviour, but it just delays the annoyance to after skip.

Eric Rodriguez (Feb 22 2022 at 16:24):

i am told that in lean4 this sort of stuff is going away, so hopefully

Reid Barton (Feb 22 2022 at 16:25):

Can we make a don't tactic that takes a block, and just does sorry?

Alex J. Best (Feb 22 2022 at 16:27):

Looks like this works :octopus:

example : 1 = 1  2 = 2 :=
begin
  split,
  sorry <|> { refl },
  { refl },
end

Patrick Massot (Feb 22 2022 at 16:34):

I'd be very curious to know whether @Gabriel Ebner has an explanation.

Bryan Gin-ge Chen (Feb 22 2022 at 16:36):

I suspect this is the same as lean#201

Kyle Miller (Feb 22 2022 at 16:37):

Reid Barton said:

Can we make a don't tactic that takes a block, and just does sorry?

Yep!

import tactic

namespace tactic
namespace interactive
setup_tactic_parser

/- Ignore a tactic block and use `sorry` instead, to help speed up a
proof under construction. -/
meta def skip_proof (t : itactic) : tactic unit :=
tactic.admit

/- Ignore the tactic block completely. -/
meta def ignore (t : itactic) : tactic unit :=
tactic.skip

end interactive
end tactic

example : 1 = 1  2 = 2 :=
begin
  split,
  skip_proof { refl },
  { refl },
end

Reid Barton (Feb 22 2022 at 16:37):

Or since sorry already exists, it could take an optional block and ignore it (assuming optional blocks are possible)

Gabriel Ebner (Feb 22 2022 at 16:38):

I'd be very curious to know whether @Gabriel Ebner has an explanation.

As others have already pointed out, this is the "intended" behavior of the semicolon. That is, it shows all goals that the block would be applied to (i.e., none in this case).

Patrick Massot (Feb 22 2022 at 16:39):

Bryan Gin-ge Chen said:

I suspect this is the same as lean#201

Indeed!

Patrick Massot (Feb 22 2022 at 16:39):

It's so weird that the semi-colon affects the tactic state before using it!

Patrick Massot (Feb 22 2022 at 16:40):

Anyway, I think we could have the skip_proof tactic (maybe with a shorter name).

Kyle Miller (Feb 22 2022 at 16:41):

Would it be too far out there to upgrade sorry to take an optional itactic? That way it could just be sorry { ... }

Kyle Miller (Feb 22 2022 at 16:41):

Oh, Reid already said that

Yakov Pechersky (Feb 22 2022 at 16:43):

Except if you accidentally forget the comma after sorry, you might be sorrying the wrong thing.

Yakov Pechersky (Feb 22 2022 at 16:45):

sorry is already overloaded since it is a homonym for the term and the tactic. Putting more things on it to now possibly affect other blocks is scary to me. But I can learn to deal with it.

Kyle Miller (Feb 22 2022 at 16:47):

I couldn't get optional itactic blocks to work, and there aren't any tactics that have them, so they might not be possible.

Reid Barton (Feb 22 2022 at 16:49):

what are the odds that an optional expression would match the same syntax?

Reid Barton (Feb 22 2022 at 16:50):

One advantage of reusing sorry is that we already know that writing sorry means you didn't prove the theorem. But if it doesn't work (without weird hacks), then not worth it.

Kyle Miller (Feb 22 2022 at 16:52):

Other possible names: cut, ignore, overlook, trust, approve, defer, relent, or a one-letter name like c or s

Mario Carneiro (Feb 22 2022 at 16:54):

itactic is a bit weird, but IIRC Ed added a regular parser combinator for tactic blocks

Stuart Presnell (Feb 22 2022 at 16:59):

Would it be easy to ensure that VS Code formats this new name in red as it does with sorry, to make it easier to find?

Mario Carneiro (Feb 22 2022 at 17:01):

import tactic

namespace tactic.interactive
setup_tactic_parser
meta def foo (x : parse parser.itactic?) : tactic unit := skip
end tactic.interactive

example : true :=
begin
  foo { skip },
  foo,
end

Kyle Miller (Feb 22 2022 at 17:04):

Ok, so this could replace sorry:

meta def «sorry» (t : parse parser.itactic?) : tactic unit :=
tactic.admit

Kyle Miller (Feb 22 2022 at 17:04):

I didn't realize begin/end work, too, for these:

example : 1 = 1  2 = 2 :=
begin
  split,
  sorry' begin refl end,
  { refl },
end

Mario Carneiro (Feb 22 2022 at 17:08):

yes, begin and end are synonyms for { } in tactic mode (and outside it in a few places)

Patrick Massot (Feb 22 2022 at 17:09):

I like this. Indeed there is some risk of being confusing if used accidentally, but it doesn't sound like a huge risk to me.

Eric Rodriguez (Feb 22 2022 at 17:56):

why not just make a different name to avoid all possible mistakes?

Reid Barton (Feb 22 2022 at 17:58):

Because people (and IDEs and other tools) already know that sorry has an important meaning

Kyle Miller (Feb 22 2022 at 18:00):

I think that also, even if there's a mistake people make with this, it won't take long to figure out what happened.

Kyle Miller (Feb 22 2022 at 18:15):

lean#689

One thing I'm not sure about is using with_desc for parser.itactic to give it a better documentation string. To get it to work, I added a reflectable instance for with_desc, but I'm not really sure what the class is for.

Eric Rodriguez (Feb 22 2022 at 18:17):

I think it'd be nice if this could be tested with sorry'd code, such as LTE and flt-regular, before merging into mathlib main; it could wreak havoc if it works differently to what we think

Kyle Miller (Feb 22 2022 at 18:19):

Here's what the in-tactic docstring looks like in context (in Emacs):

image.png

Gabriel Ebner (Feb 22 2022 at 18:24):

Kyle Miller said:

One thing I'm not sure about is using with_desc for parser.itactic to give it a better documentation string. To get it to work, I added a reflectable instance for with_desc, but I'm not really sure what the class is for.

I'm not 100% sure, but I believe the reason is that the return value of the parser (the α in parser α) must be serialized between calling the custom parser and calling the user notation, and expressions are the only available format for that. Your implementation looks correct, since with_desc has the same return value as the wrapped value.


Last updated: Dec 20 2023 at 11:08 UTC