Ntural number game advanced addition world / 13

Stream: general

[Daniel Papp]

So the problem is the following: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=13 And this proof works:

symmetry,
intro p,
induction n with d hd,
exact succ_ne_zero(0)(p),
exact hd(succ_inj(p)),

My question is if I want to introduce a new variable for succ_inj(p) before the last line how should I parametrize the succ_inj function/theorem to make this work. I tried something like have tmp := (succ_inj (succ d) d)(p) but that didn't seem to work. Not sure if such lisp-like syntax is allowed here or not.

[Daniel Papp]

Note that I would like to be explicit about the parameters for the theorem I know have tmp := succ_inj(p) would work just fine.

[Yakov Pechersky]

Because the definition of succ_inj is:

succ_inj {a b : mynat} :
    succ(a) = succ(b) → a = b

those curly braces mean that the arguments are implicit. To prove arguments explicitly to succ_inj for the a b, you can use @ like so:

have := @succ_inj (succ d) d p,

But in any case, a proper p hypothesis will always allow both a b to be inferred.

[Daniel Papp]

I see. so does this also mean that the above case I can use hd(succ_inj (succ d) d p) as well?

What do you mean by proper hypothesis? Also could you give me some link on how lean infers this?

Thanks for your help btw!

[Yakov Pechersky]

You can read this section of TPIL: https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html and TPIL in general is a good resource.

[Yakov Pechersky]

You would have to say hd (@succ_inj (succ d) d p) if you really wanted to be explicit

[Yakov Pechersky]

Your p is a hypothesis that says p : succ (succ d) = succ d. And you have a theorem that says that for any a b such that succ a = succ b then a = b.
What does that look like?

succ_inj {a b : mynat} :
    succ(a) = succ(b) → a = b

The implicit arguments mean -- infer which a and b I'm talking about from the hypothesis given. So, when you say succ_inj p, that is succ_inj over a hypothesis that succ (succ d) = succ d, then of course it is obvious that the only a and b being discussed here are succ d and d, respectively.

[Daniel Papp]

Thanks Yakov!

I think I more or less understand it. I mean I was going through the exercises in the natural number game. Sometimes it feels a bit like magic. I have to get used to this language I guess.

Thanks for the link too!

[Kevin Buzzard]

Lean does not do magic. After a while you can start asking yourself how it just did what it did, and finding the logical explanation.

[Daniel Papp]

Yes, I get that. I really like this tool. I hope it will be more widespread in the future. It would be interesting to see sites similar to math.stackexchange.com to use lean or having competition sites like codeforces but for math.

[Alex Peattie]

Daniel Papp said:

Yes, I get that. I really like this tool. I hope it will be more widespread in the future. It would be interesting to see sites similar to math.stackexchange.com to use lean or having competition sites like codeforces but for math.

In case it's of interest there are some Lean challenges on Codewars :smile: - https://www.codewars.com/kata?language=lean

[Daniel Papp]

Thanks Alex! I check that out in the evening.