Zulip Chat Archive

Stream: general

Topic: sorry does not behave like NaN


Kenny Lau (Apr 29 2020 at 03:46):

I expected this to fail:

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

Kenny Lau (Apr 29 2020 at 03:46):

should sorry behave like NaN in javascript?

Kenny Lau (Apr 29 2020 at 03:47):

> NaN == NaN
< false

Mario Carneiro (Apr 29 2020 at 03:47):

I was wondering the same thing

Mario Carneiro (Apr 29 2020 at 03:47):

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

Kenny Lau (Apr 29 2020 at 03:47):

but sorry shouldn't be equal to sorry right

Mario Carneiro (Apr 29 2020 at 03:48):

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 (Apr 29 2020 at 03:49):

Isn't sorry basically like choice...

Reid Barton (Apr 29 2020 at 03:49):

without that pesky nonempty side condition

Reid Barton (Apr 29 2020 at 03:49):

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

Reid Barton (Apr 29 2020 at 03:50):

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

Mario Carneiro (Apr 29 2020 at 03:50):

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

Kenny Lau (Apr 29 2020 at 03:50):

so like those private definitions with those big numbers

Mario Carneiro (Apr 29 2020 at 03:50):

yes

Mario Carneiro (Apr 29 2020 at 03:50):

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

Mario Carneiro (Apr 29 2020 at 03:51):

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

Reid Barton (Apr 29 2020 at 03:51):

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 (Apr 29 2020 at 03:51):

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

Mario Carneiro (Apr 29 2020 at 03:52):

sorry could capture its entire local context

Reid Barton (Apr 29 2020 at 03:52):

Yes, that's true.

Kevin Buzzard (Apr 29 2020 at 06:38):

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

Mario Carneiro (Apr 29 2020 at 06:47):

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 (Apr 29 2020 at 06:48):

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

Mario Carneiro (Apr 29 2020 at 06:48):

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

Chris Hughes (Apr 29 2020 at 09:48):

You can just use constant smooth as well

Kenny Lau (Apr 29 2020 at 09:57):

why could he prove that all functions were smooth?

Mario Carneiro (Apr 29 2020 at 10:06):

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 (Apr 29 2020 at 10:10):

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

Kenny Lau (Apr 29 2020 at 10:10):

wow


Last updated: Dec 20 2023 at 11:08 UTC