sorry does not behave like NaN

Stream: general

[Kenny Lau]

I expected this to fail:

#check (rfl : (sorry : ℕ) = sorry)

[Kenny Lau]

should sorry behave like NaN in javascript?

[Kenny Lau]

> NaN == NaN
< false

[Mario Carneiro]

I was wondering the same thing

[Mario Carneiro]

please don't make that comparison, javascript is not something we should aspire to

[Kenny Lau]

but sorry shouldn't be equal to sorry right

[Mario Carneiro]

That depends on what you mean. I think that the way it currently works a sorry is marked only with its expected type, so of course it should be equal to itself in the same way that choice nat is equal to choice nat

[Reid Barton]

Isn't sorry basically like choice...

[Reid Barton]

without that pesky nonempty side condition

[Reid Barton]

or at least, that seems like a reasonable way for it to work

[Reid Barton]

You might want distinct occurrences of sorry to turn into different constants

[Mario Carneiro]

A reasonable alternative implementation has the sorry macro get a tag that is renewed every time the word sorry is parsed

[Kenny Lau]

so like those private definitions with those big numbers

[Mario Carneiro]

yes

[Mario Carneiro]

I don't know if the numbers would be public in this case though

[Mario Carneiro]

if they are internal to the macro then they can't be forged

[Reid Barton]

But it would not fix that time Patrick wrote something like def smooth (f : real -> real) : Prop := sorry and lemma smooth_constant (r) : smooth (\lam _, r) and then found he could prove that all functions were smooth.

[Mario Carneiro]

they would be part of the macro_def object that is not inspectable from lean

[Mario Carneiro]

sorry could capture its entire local context

[Reid Barton]

Yes, that's true.

[Kevin Buzzard]

I don't think I ever sorried data from the day I saw Patrick's example

[Mario Carneiro]

note that there is an easy workaround for patrick's example, which is to sorry the function after reverting everything, i.e. def smooth : (real -> real) -> Prop := sorry

[Mario Carneiro]

In fact, it would be an easy fix to the sorry tactic to make it call revert_all first

[Mario Carneiro]

and then at least def smooth (f : real -> real) : Prop := by sorry would have the right behavior

[Chris Hughes]

You can just use constant smooth as well

[Kenny Lau]

why could he prove that all functions were smooth?

[Mario Carneiro]

When you write def smooth (f : real -> real) : Prop := sorry, sorry is basically like choice Prop. So in particular it does not depend on f, and so this function, whatever it is, is a constant function.

[Kenny Lau]

def smooth (f : ℕ → ℕ) : Prop := sorry
lemma smooth_constant (n) : smooth (λ _, n) := sorry
lemma smooth_all (f) : smooth f := smooth_constant 0

[Kenny Lau]

wow