Two kinds of sorries

Stream: general

[Martin Dvořák]

I started working on a new conjecture today. I'm thinking of forbidding myself from using pen and paper so that I have to write everything in Lean. Maybe I'll define a custom alias for sorry so I will have two kinds of sorries. First kind of sorry for "I don't know whether this holds". Second kind of sorry for "I believe this can be done — I just don't want to spend time on it". Any recommendations?

[Johan Commelin]

Sounds good. Do you want computers to do anything with that distinction?

[Johan Commelin]

If it's just for yourself, you can of course already get very far by just adding a comment.

[Martin Dvořák]

No. They will be different only for me. However, I think two words will be better than comments; I can set different background colors for them.

[Yaël Dillies]

Do you know about synthetic vs non-synthetic sorries?

[Martin Dvořák]

No idea!

[Yaël Dillies]

See docs#sorryAx

[Eric Wieser]

You could also use axiom

[Eric Wieser]

Which has the advantage that you can easily check whether your theorem depends on things you're not sure about

[Kevin Buzzard]

Note that we still have the admit tactic which seems to be a synonym for sorry and you could arbitrarily give it a semantic meaning of one of the two things you want to express above

[Kevin Buzzard]

In the very old Lean 3 days, I think one of sorry/admit was the tactic, and the other one was the term (I forgot which was which), like rfl (the term) v refl (the tactic). But now the push is to unify these (I think because it was confusing for the users -- certainly many undergrads asked me the difference between refl and rfl pre Lean 4)

[Adam Topaz]

universe u
axiom sorryWithConfidenceAx (α : Sort u) (confidence : Nat := 100) : α

macro "sorryWithConfidence" n:num : term => do
  `(sorryWithConfidenceAx _ $n)

example : 1 = 2 := sorryWithConfidence 0
example : 1 = 2 := sorryWithConfidence 100

[Adam Topaz]

One could take this even further by combining the confidence of various sorryWithConfidence's in some declaration in some way to get a "global" confidence.

[Richard Copley]

I'd like it if, just occasionally, Lean said sorry to me

[Mario Carneiro]

just double checked, "sorry" is not among the things lean will ever say in error messages unless it is referring to your code like declaration uses 'sorry' or cannot evaluate code because 'foo' uses 'sorry' and/or contains errors. On the other hand, sometimes one sorry is not enough to appease lean...

[Mario Carneiro]

I am reminded of INTERCAL, the language which refuses to compile your code if you say please not enough or too much

[Marc Huisinga]

Lean just uses different words to say "sorry" than we do. For example, one of the expressions it uses to ask for forgiveness is "Server process for <file path> crashed, likely due to a stack overflow or a bug".

[Adam Topaz]

That's a very passive aggressive way of saying "sorry".

[Kyle Miller]

Mario Carneiro said:

I am reminded of INTERCAL

I like how Qq has a comefrom macro. It's not quite the same as INTERCAL's come from statement, but I can't help but be reminded of it.

[Jon Eugster]

In the NNG, we did the same thing as Adam, i.e. duplicate sorryAx to distinguish the two. Kevin called the tactic zyxxy which proves everything but does not trigger the check wether the user used sorry.

[Damiano Testa]

Some of the files in test also use a test_sorry so as to avoid emitting noise when built, but still close unwanted goals.

[Tomas Skrivan]

Similarly when programming in Lean, I found it useful to have sorry_proof that is sorry only in Prop and does not emit a warning. Normal sorry is reserved for data that would prevent program execution.

[Johan Commelin]

xyzzy! https://en.wikipedia.org/wiki/Colossal_Cave_Adventure

[Kevin Buzzard]

Spoiler alert!