Natural Numbers Game question

Stream: new members

[Andreas Steiger]

Hi all, newbie here. I'm trying my luck with the Natural Numbers Game and I'm having a lot of fun with it, thanks for that already!

Now, I just solved Level 8 of Advanced Proposition world, and_or_distrib_left, but it took me 25 lines to write the proof. That feels... long? Anybody willing to look at it and give me some feedback if I'm doing this right?

[Johan Commelin]

Sure, copy paste the proof here, using triple #backticks

[Andreas Steiger]

Thanks!

split,
intro h,
cases h with p qr,
cases qr with q r,
left,
split,
exact p,
exact q,
right,
split,
exact p,
exact r,
intro f,
cases f with pq pr,
split,
cases pq with p q,
exact p,
cases pq with p q,
left,
exact q,
split,
cases pr with p r,
exact p,
right,
cases pr with p r,
exact r,

[Andreas Steiger]

So this works, but I felt like not really understanding how to use any structure except breaking it down into the very basic parts

[Johan Commelin]

Can you please paste a link to the level?

[Andreas Steiger]

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=8

[Johan Commelin]

@Andreas Steiger I'm not sure what kind of solution you are looking for. Do you want a "hammer" that does the basic logic for you?

[Andreas Steiger]

@Johan Commelin No, not really. I'm mostly wondering if a more experienced user would solve this very differently or if this is just the way you have to do this

[Kevin Buzzard]

You can solve it in term mode. I posted a video of the difference on the Xena project YouTube channel

[Johan Commelin]

But you can't do term mode in the Natural Number Game, right?

[Kevin Buzzard]

Basically lean will let you solve this in one line, but you have to know a different way of interacting with it, outside the tactic monad

[Kevin Buzzard]

No, but you can do it in the online web editor

[Johan Commelin]

@Andreas Steiger An experienced user would solve this totally differently, using tools that you don't have in NNG

[Kevin Buzzard]

I would post links but I'm on mobile and in a rush

[Johan Commelin]

Here is an NNG proof:

  split,
  all_goals { intro h },
  all_goals { repeat { cases h with h h } },
  all_goals {
    try { left; split; assumption },
    try { right; split; assumption } },
  all_goals { split },
  all_goals { try { assumption } },
  try { left; assumption },
  try { right; assumption},

[Johan Commelin]

It gives a hint towards what you could do with more powerful tools

[Shing Tak Lam]

NNG does introduce cc, so I guess that could be used here?

[Kevin Buzzard]

If all code looked like that then Johan and Patrick and I wouldn't have been able to make all the complex algebraic objects we made

[Shing Tak Lam]

  split,
  { cc },
  { intros hpqr,
    cases hpqr with hpq hpr,
    { cc },
    { cc } }

[Johan Commelin]

Aah, I didn't know that cc was available

[Andreas Steiger]

Kevin Buzzard said:

You can solve it in term mode. I posted a video of the difference on the Xena project YouTube channel

Thanks, I think I've found them, I'll check it out!

[Kevin Buzzard]

What is available is a closely guarded secret :-)

[Kevin Buzzard]

You can try this yourself in the web editor

[Kenny Lau]

@Mario Carneiro request: #nng-7-8 = http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=8

[Gabriel Ebner]

cases classical.prop_decidable P; cc. I'm surprised that there is no open_locale classical.

[Kevin Buzzard]

@Andreas Steiger you can try making a term mode proof following the techniques of this video using the Lean web editor

[Kevin Buzzard]

Ha, Freek complained about the same thing: but how do I add open_locale classical to the entire game?

[Patrick Massot]

you can make classical.prop_decidable an instance in a file imported by all others.

[Kevin Buzzard]

With priority 10 or so? I don't even know how to see what open_locale classical does. Freek complained that equality wasn't decidable on mynat but this I could fix myself.

[Mario Carneiro]

Kenny Lau said:

Mario Carneiro request: #nng-7-8 = http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=8

Apparently I starred this ages ago and forgot to come back to it. Testing: #nng-7-8

[Kevin Buzzard]

I still can't get my head around the fact that both $\lor$ and $\land$ distribute over each other.

[Mario Carneiro]

dUaLiTy

[Bjørn Remseth]

I just learned about Lean three days ago, so I'm a total N00b at it. Working through the natural numbers game, but right now I'm completely stuck at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=3&level=4. Any hints at all about how to prove this one would be highly appreciated.

[Kevin Buzzard]

Induction?

[Bjørn Remseth]

(deleted)

[Bjørn Remseth]

many of them, and extensive use of repeat {} not to confuse myself and eventually I got there :-) Thanks again.

[Damiano Testa]

Actually, a single induction can be enough.

[Bjørn Remseth]

I am sure it can. I suck at this :-) (but thanks for the tip. I will review all of this again once I'm through it once).

[Damiano Testa]

Sometimes, there is some maths in shortening a proof, sometimes, it is knowing how concepts are built in Lean.

[Kevin Buzzard]

A general tip: do induction on the right-most variable, because addition and multiplication are defined by recursion on the right-most variable.