sorry weirdness

Stream: general

[Patrick Massot]

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]

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

[Eric Rodriguez]

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]

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

[Reid Barton]

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

[Alex J. Best]

Looks like this works :octopus:

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

[Patrick Massot]

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

[Bryan Gin-ge Chen]

I suspect this is the same as lean#201

[Kyle Miller]

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]

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

[Gabriel Ebner]

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]

Bryan Gin-ge Chen said:

I suspect this is the same as lean#201

Indeed!

[Patrick Massot]

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

[Patrick Massot]

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

[Kyle Miller]

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

[Kyle Miller]

Oh, Reid already said that

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Stuart Presnell]

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]

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]

Ok, so this could replace sorry:

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

[Kyle Miller]

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]

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

[Patrick Massot]

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]

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

[Reid Barton]

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

[Kyle Miller]

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]

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]

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]

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

image.png

[Gabriel Ebner]

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.