## Stream: new members

### Topic: Numbers Game

#### Philip Vetter (Jul 13 2020 at 08:57):

4:54 PM

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

#### 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)?

#### Kenny Lau (Jul 13 2020 at 09:00):

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

#### Kenny Lau (Jul 13 2020 at 09:00):

well a cannot be applied to 0

#### 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.

#### Johan Commelin (Jul 13 2020 at 09:01):

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

#### Kenny Lau (Jul 13 2020 at 09:03):

it's not a definition :P

#### Philip Vetter (Jul 13 2020 at 09:09):

What would you call it? A type declaration?

#### Philip Vetter (Jul 13 2020 at 09:10):

THIS WORKS: rw add_succ a 0

#### Scott Morrison (Jul 13 2020 at 09:10):

(Note this was Markus' first suggestion above.)

#### 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?

#### 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.

#### 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…

#### 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