Zulip Chat Archive

Stream: general

Topic: Ntural number game advanced addition world / 13


view this post on Zulip Daniel Papp (Jan 10 2021 at 17:19):

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.

view this post on Zulip Daniel Papp (Jan 10 2021 at 17:20):

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.

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 17:38):

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.

view this post on Zulip Daniel Papp (Jan 10 2021 at 18:00):

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!

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 18:45):

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.

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 18:45):

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

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 18:48):

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.

view this post on Zulip Daniel Papp (Jan 10 2021 at 19:07):

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!

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 19:21):

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.

view this post on Zulip Daniel Papp (Jan 11 2021 at 10:55):

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.

view this post on Zulip Alex Peattie (Jan 11 2021 at 12:10):

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

view this post on Zulip Daniel Papp (Jan 11 2021 at 12:19):

Thanks Alex! I check that out in the evening.


Last updated: May 11 2021 at 22:14 UTC