Zulip Chat Archive

Stream: general

Topic: sorry does not behave like NaN


view this post on Zulip Kenny Lau (Apr 29 2020 at 03:46):

I expected this to fail:

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 03:46):

should sorry behave like NaN in javascript?

view this post on Zulip Kenny Lau (Apr 29 2020 at 03:47):

> NaN == NaN
< false

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:47):

I was wondering the same thing

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:47):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 03:47):

but sorry shouldn't be equal to sorry right

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 29 2020 at 03:49):

Isn't sorry basically like choice...

view this post on Zulip Reid Barton (Apr 29 2020 at 03:49):

without that pesky nonempty side condition

view this post on Zulip Reid Barton (Apr 29 2020 at 03:49):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 03:50):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2020 at 03:50):

so like those private definitions with those big numbers

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:50):

yes

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:50):

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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:51):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:51):

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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 03:52):

sorry could capture its entire local context

view this post on Zulip Reid Barton (Apr 29 2020 at 03:52):

Yes, that's true.

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 06:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 29 2020 at 09:48):

You can just use constant smooth as well

view this post on Zulip Kenny Lau (Apr 29 2020 at 09:57):

why could he prove that all functions were smooth?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2020 at 10:10):

wow


Last updated: May 10 2021 at 18:22 UTC