sorry trouble

Stream: Carleson

[Floris van Doorn]

Suppose you have a definition that isn't finished yet, so you sorry it and then axiomatize some sorry'd properties about it.

def 𝓩 (I : Grid X) : Set (Θ X) := sorry

What could possibly go wrong?

People might accidentally (ab)use that 𝓩 is a constant function. Luckily not in an essential way

[Yaël Dillies]

Hmm, do we have to use opaque instead then?

[Floris van Doorn]

Or sorry the element of type Grid X → Set (Θ X).

[Ruben Van de Velde]

Maybe lemma Zaux (I : Grid X) : \exists .. and then use Zaux.choose?

[Yaël Dillies]

Looks strictly more complicated than using opaque

[Kevin Buzzard]

Oh if there was a fix for this that would be great! Patrick discovered the problems with sorrying definitions during the perfectoid project and I've been paranoid about doing this ever since. If I could sorry a ton of definitions for FLT without worrying that when they were filled in I'd break a bunch of people's code then I would take Mario's suggestion that he made to me in Bonn ("do this") much more seriously.

[Floris van Doorn]

This shouldn't be hard. We could write a tactic revert_all that reverts every hypothesis, and then have a macro sorry' for by revert_all; sorry. In that case, at least this issue will not occur for sorry'.

There are some issues with variables:

• You might have a theorem that depends on a variable or type-class, but only in the proof. If you sorry the theorem, then this variable will not be included
• Variables could accidentally be added to declarations, even if you don't what a theorem that depends on that variable.