Zulip Chat Archive

Stream: new members

Topic: why does an anonymous assume need extra colon?


view this post on Zulip Fames Yasd (Sep 09 2020 at 09:12):

There is an explanation in theorems proving in lean:
"In contrast to the usage with have, an anonymous assume needs an extra colon. The reason is that Lean allows us to write assume h to introduce a hypothesis without specifying it, and without the colon it would be ambiguous as to whether the h here is meant as the label or the assumption."
but I didn't get it. I feel like anonymous assume should not have an extra colon because it seems to be the same as have and the last one does not have an extra colon when used anonymously.

view this post on Zulip Ruben Van de Velde (Sep 09 2020 at 09:13):

How do you use have without a colon?

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:16):

variable f :   
variable h :  x : , f x  f (x + 1)

example : f 0  f 1  f 1  f 2  f 0 = f 2 :=
assume : f 0  f 1,
assume t₀ : f 1  f 2,
have  t₁ : f 0  f 2, from le_trans f 2  f 1 f 1  f 0,
have f 0  f 2, from le_trans (h 0) (h 1),
show f 0 = f 2, from le_antisymm this f 0  f 2

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:16):

In term mode you can use have without colon

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:16):

yes

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:17):

@Fames Yasd Pro tip: #backticks

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:17):

but for some reason I can't use assume without colon

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:17):

Johan Commelin thank you

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:19):

assume f x

What would this mean?
Are you assuming this : f x or is it assume (f : _) (x : _)?

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:22):

so the ambiguity rises because we can assume several statements?

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:22):

I did not know that we can assume several statements in a row

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:23):

could have made it in a separate keyword like assumptions

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:24):

maybe not, anyway thanks for the info

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:25):

But assume x y z reads more natural, right?

view this post on Zulip Fames Yasd (Sep 09 2020 at 09:25):

yes

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:25):

So, personally, I think the extra colon is the better tradeoff


Last updated: May 18 2021 at 16:25 UTC