Zulip Chat Archive

Stream: new members

Topic: Numbers Game


view this post on Zulip Philip Vetter (Jul 13 2020 at 08:57):

4:54 PM

In Numbers Game, Level 4/4, I can specify a in
rw add_zero(a),
but why do I get an error from
rw add_succ(a 0),
despite the definition
add_succ (a d : mynat) : a + succ(d) = succ (a + d) ?

view this post on Zulip Markus Himmel (Jul 13 2020 at 08:58):

What happens if you write rw add_succ a 0 instead of rw add_succ(a 0)?

view this post on Zulip Kenny Lau (Jul 13 2020 at 09:00):

add_succ (a 0) means apply add_succ to the result of applying a to 0

view this post on Zulip Kenny Lau (Jul 13 2020 at 09:00):

well a cannot be applied to 0

view this post on Zulip Johan Commelin (Jul 13 2020 at 09:01):

I guess the syntax def add_succ (a d : mynat) : a + succ(d) = succ (a + d) can be confusing.

view this post on Zulip Johan Commelin (Jul 13 2020 at 09:01):

You should read it as def add_succ (a : mynat) (d : mynat) : etc...

view this post on Zulip Kenny Lau (Jul 13 2020 at 09:03):

it's not a definition :P

view this post on Zulip Philip Vetter (Jul 13 2020 at 09:09):

What would you call it? A type declaration?

view this post on Zulip Philip Vetter (Jul 13 2020 at 09:10):

THIS WORKS: rw add_succ a 0

view this post on Zulip Scott Morrison (Jul 13 2020 at 09:10):

(Note this was Markus' first suggestion above.)

view this post on Zulip Karolin Varner (Sep 30 2020 at 20:41):

Hi! I am trying to learn lean right now using the numbers game (insert verbose thanks for creating & providing support for lean :) ):

I've noticed that there a couple of proofs taking the form a + b = a + c -> a = b (where + is a stand in for arbitrary operators); Is there any deeper reason why we can't just proof a = b <=> f(a) = f(b) and be done with it?

As the game explained, lean allows me to treat equivalence a <=> b as a tuple of two functions a -> b and b -> a; I know equality and equivalence are subtly different; but is there any underlying reason why lean won't allow me to treat equality as a tuple of functions, forcing me instead to use rw and rw \l to transform my expression?

I've noticed \circ will let me do function composition. Is there an equivalent to the haskell $ operator (reduced binding strength function application) so I can rewrite my expressions exact (foo \circ bar) baz as exact foo \circ bar $ baz?

view this post on Zulip Kyle Miller (Sep 30 2020 at 20:48):

a = b ↔ f a = f b is true iff f is injective, and the statements you're proving are that the corresponding function is injective -- in your example, that would be λ x, a + x.

view this post on Zulip Yakov Pechersky (Sep 30 2020 at 20:48):

Re the last question, yes, and the deferred application is also $

view this post on Zulip Karolin Varner (Sep 30 2020 at 20:50):

oO I've tried $ so I guess it's disabled for the numbers game?

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 20:50):

I'm afraid you can't use $ in tactic mode :-(

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 20:50):

It's something to do with the parser.

view this post on Zulip Kyle Miller (Sep 30 2020 at 20:52):

I think you can use $, but you just have to wrap the whole expression in parentheses, potentially defeating the purpose of using $.

view this post on Zulip Karolin Varner (Sep 30 2020 at 20:55):

Yes wrapping the statement in parentheses works! Still a bit easier to read imo so that's nice…

view this post on Zulip Yakov Pechersky (Sep 30 2020 at 20:57):

From what I've seen, it isn't the mathlib style to use \circ, but rather expand out the full g (f x). I could be wrong.


Last updated: May 14 2021 at 21:11 UTC