Sorry isn't apologetic

Stream: general

[David Ang]

What is going on here?

example : sorry := by
  rw [← Rat.inv_ofNat_den]
  sorry

Puzzle: guess what it does!

[Kyle Miller]

Lol, this is the second time I've seen someone run into this recently (@Eric Wieser pointed it out to me too).

This is the unique/labeled sorry feature's encoding being a little too visible to tactics. When designing it I was thinking "it's going to be rare that people have sorry visible in their goals, they'll just be inside the definitions to prevent accidental non-theorems... right? (... right?)"

Two possible fixes:

• The encoding could put some mdata into the sorries with the source position. This won't fix the "why does rw succeed here" problem though.
• When sorrys are created, they can package up the source position information into an auxiliary definition, so the term might be sorryAx (Lean.Name → Sort ?u.1) false _sorryLabel.22 instead sorryAx (Lean.Name → Sort ?u.1) false Mathlib.Foo.11.10.11.15.10.15._sorry._@.Mathlib.Foo._hyg.5. This would keep Expr.hasSorry` having simple definition too (compared to a version where the whole sorry term is packaged up into an auxiliary definition).

[Kenny Lau]

Kyle Miller said:

Two possible fixes

is there really anything to fix? i don't see a bug here, if you use non-intended features on non-intended features, you get non-intended output

[Kyle Miller]

Yes, of course this is a bug. Why should users know that sorry is encoded in some way that contains hidden naturals? How is it non-intended to use rw on a goal?

[Kyle Miller]

sorry can easily appear in goals in proofs in the goal too, e.g. you might have Option.get o sorry in the goal if you haven't finished writing the full theorem statement, and rw happily rewrites proofs.

[David Ang]

I found this because I had some theorem of the form (some simple thing) = (some complicated thing), but I extracted it to an (some simple thing) = sorry and tried rw? to see if there are any easy rewrites on the left hand side

[Eric Wieser]

As a quick hack can we put the source info into the string?

[Eric Wieser]

It's much less likely that the user will be rewriting by the wrong string by coincidence, especially if it's just one big string

[Kyle Miller]

I don't think that's any quicker of a hack than fixing it. These support "go to definition", and it would need a parser for example.

[Eric Wieser]

Could we generate an inductive SorryType.Mod.Line.Col where | mk type for each sorry?

[Eric Wieser]

That way the name is in the .const term where it can't be rewritten

[Kyle Miller]

The difference between that and the aux definition idea is that inductive guarantees that it will never be rewritten. Do we think that there's a chance that someone will apply a theorem to rewrite an arbitrary _sorryPos.22 : Lean.Name position to something else? At least rw doesn't let the LHS of a theorem to be a variable, so even in a contradictory context with forall n : Name => n = .anonymous, it seems hard to get into trouble.

[Eric Wieser]

Does opaque sorryPos.37 : Unit work, or does eta reduction make that defeq to any other pos?

[Aaron Liu]

That will be defeq to every other element of type Unit