Numbers Game

Stream: new members

[Philip Vetter]

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

[Markus Himmel]

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

[Kenny Lau]

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

[Kenny Lau]

well a cannot be applied to 0

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

it's not a definition :P

[Philip Vetter]

What would you call it? A type declaration?

[Philip Vetter]

THIS WORKS: rw add_succ a 0

[Scott Morrison]

(Note this was Markus' first suggestion above.)

[Karolin Varner]

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]

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.

[Yakov Pechersky]

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

[Karolin Varner]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's something to do with the parser.

[Kyle Miller]

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

[Karolin Varner]

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

[Yakov Pechersky]

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.