The Lean-to

Huỳnh Trần Khanh

02:10

lol

emanresu A

04:54

Halp plz

I'm trying to do the naturnal number game

But I'm stuck on addition level 2

I have

induction b with d hd,
rw zero_add,
rw add_zero,
refl,
rw add_succ,
induction a with e hd,
rw zero_add,
rw zero_add,
refl,

hyper-neutrino

if you're ever stuck with seemingly nowhere to go try picking a different induction condition

b is in brackets in both sides so it's probably the hardest one lol

emanresu A

Oof

Thx

Problem is, after:

induction a with d hd,
rw zero_add,
rw zero_add,
refl,

I get succ d + b + c = succ d + (b + c)

Which is the same case, except with d replaced with succ d, and I can't rw anything.

hyper-neutrino

4 mins ago, by hyper-neutrino

if you're ever stuck with seemingly nowhere to go try picking a different induction condition

emanresu A

c then?

hyper-neutrino

well, what else :P

emanresu A

05:05

Nah, c has the same problem. Induction again?

hyper-neutrino

wdym

emanresu A

Wait no, nvm

hyper-neutrino

what do you have right now

emanresu A

induction c with d hd,
rw add_zero,
rw add_zero,
refl,
rw add_succ,

Becomes succ (a + b + d) = a + (b + succ d)

hyper-neutrino

you're on the right track

emanresu A

05:07

Got it!

induction c with d hd,
rw add_zero,
rw add_zero,
refl,
rw add_succ,
rw hd,
rw add_succ,
rw add_succ,
refl,

hyper-neutrino

nice

i had the same thing but with rw hd right before the final refl

emanresu A

On to succ_add

Meanwhile, you should goto sleep

Does lean have anything like gotos?

rw sleep

Huỳnh Trần Khanh

lol

emanresu A

That was a lot easier.

hyper-neutrino

typo lol

emanresu A

05:20

All I've managed to do for add_comm is to get right back to where I started.

hyper-neutrino

05:31

what do you have so far

Huỳnh Trần Khanh

05:57

pinging @emanresuA for good measure

lol

Huỳnh Trần Khanh

06:19

hey could we have like a sync meeting or something to onboard new members? because there are many people who are new to lean and it would be hard to help over chat

maybe we can have a live coding session perhaps

and also it's somewhat hard to install lean so i'd like to help with that too

emanresu A

06:44

Did it!

And in only eight lines too

Huỳnh Trần Khanh

neat lol

congrats

emanresu A

08:00

I somehow got a "type mismatch"

Huỳnh Trần Khanh

@emanresuA wait wait type mismatch? can you post your code and a screenshot of the Natural Number Game website

emanresu A

Oh wait

I forgot the rw

Big brain moment

Huỳnh Trần Khanh

lol

hey @emanresuA can you clear the goal now

hint: just spam rw add_comm, rw zero_add and rw succ_add. and then when the goal is rewritten to something similar to the induction hypothesis, just use the induction hypothesis to clear the goal

emanresu A

I'll try

Huỳnh Trần Khanh

ok

emanresu A

08:09

Apparently with this one I'll at some point need to be more specific with rw so I'll do that when I get to it

Huỳnh Trần Khanh

remember that when you use lean with mathlib, you can use the nth_rewrite tactic to specify where you want to rewrite the equation. mathlib is not available here though, this is just fyi

and most of the time i use that tactic rather than the conv tactic

emanresu A

Done!

Huỳnh Trần Khanh

neat

emanresu A

I'm going to try multiplication now

Huỳnh Trần Khanh

lol

ok

emanresu A

08:18

Hm, refl accepts 0 * 0 = 0...

It seems to accept any true statement with no variables

Huỳnh Trần Khanh

08:33

lol

actually thats incorrect

but then i don't fully understand lean either, like sometimes refl solves trivial goals

but sometimes it fails to do so

and you need more high powered tactics like norm_num or simp or rw or stuff

you don't need to fully understand what a tactic does

i just have an intuition of how "strong" a given tactic is

i don't quite remember the internal workings of the tactics

emanresu A

For mul_add, should I be doing induction with t, or one of a or b?

t seems like a dead end to me...

Wheat Witch

08:50

@emanresuA Nested induction has some strange behaviors, I believe you can get through the natural number game without using it.

emanresu A

Ok

emanresu A

09:21

Ah yes, I do love suc_mull.

Huỳnh Trần Khanh

lol

in the natural number game you don't need to do nested induction at all but you do need to generalize some variables

actually nested induction doesn't have any "strange behaviors" as long as you clear all the hypotheses that are like irrelevant

using the clear or the clear_except tactic

alternatively you can also use have instead of nested induction

@emanresuA can you solve the goal now?

hmm tbh resolving issues over chat is extremely hard

I'm p sure no one in here knows how to actually install lean

emanresu A

@HuỳnhTrầnKhanh Never mind, got it a while ago,.

Huỳnh Trần Khanh

ah ok

emanresu A

Multiplication complete!

Huỳnh Trần Khanh

lol

Wheat Witch

09:41

@HuỳnhTrầnKhanh Yes, but the natural number game doesn't cover this point.

Huỳnh Trần Khanh

ok

Huỳnh Trần Khanh

10:34

ok so as the chat is relatively inactive i would like to bring the sync meeting idea up again

because on the xena project discord server people usually share their screen to get help

so we should do something similar

because lean errors are extremely tricky to debug over chat

this can cost you several days if you try to figure them out on your own

the natural number game is relatively simple. actual lean theorems are much more complicated

installing lean is also next to impossible if you're not familiar with lean, even if you are familiar with how to install software in general

I'm generally p helpful lol

so if you don't find this idea problematic then it might be easier for me to help people lol

emanresu A

@WheatWitch Even pow_pow?

Wheat Witch

I'll check.

But remember you can use lemmata

emanresu A

10:49

?

No idea

Huỳnh Trần Khanh

?

emanresu A

What's lemmata?

Huỳnh Trần Khanh

@emanresuA you're supposed to generalize variables

Wheat Witch

@emanresuA Things you have already proved.

emanresu A

@WheatWitch Oh, those

Wheat Witch

10:51

You can see what's available on the left hand bar.

emanresu A

Yes I use those a lot, I just didn't recongines the name

Huỳnh Trần Khanh

because they're not really called lemmata in the interface lol

Wheat Witch

Well iirc it sometimes declares them with lemma.

Huỳnh Trần Khanh

lol

Wheat Witch

11:15

@emanresuA Yes. It's not only possible but it's probably easier than double induction.

Huỳnh Trần Khanh

yeah

emanresu A

@WheatWitch Oh well, that's how I did it

Wheat Witch

Induction on m works, idk if other inductions work that's the first one I guessed.

induction m,
rw pow_zero,
rw zero_mul,
rw one_pow,
rw pow_zero,
refl,
rw pow_succ,
rw mul_pow,
rw succ_mul,
rw pow_add,
rw m_ih,
refl,

Huỳnh Trần Khanh

in fact, I've never heard of "double induction" before. if you're not golfing, you're supposed to use have or generalize variables. and yeah use existing theorems as well

Wheat Witch

Sometimes you can't generalize the variables.

For example my rev_rev solution uses nested induction and you can't generalize on that one.

Huỳnh Trần Khanh

11:24

yeah normally you would use a have block

Bubbler

If you seem to need induction twice, you probably need a lemma for the inner one

Huỳnh Trần Khanh

yeah

Wheat Witch

lemmata are expensive though.

Bubbler

It doesn't help much with golfing but at least it helps a lot with finding a working answer

Huỳnh Trần Khanh

^

Wheat Witch

11:27

I find it pretty hard to de-saturate your lemmata once you've made them.

Huỳnh Trần Khanh

wdym by desaturate

Wheat Witch

It's easy to find a solution but it doesn't translate very easily into the case I actually want.

@HuỳnhTrầnKhanh Remove the lemma.

Huỳnh Trần Khanh

yeah yeah ITP is very, like, cumulative. for a lot of things you need to prove a lot of silly lemmas (or lemmata) and then maybe tag them with @[simp] before working on the actual proof

that's why mathlib is tremendously useful

emanresu A

Powers done!

Bubbler

The real game starts with the right side ;)

Huỳnh Trần Khanh

11:39

lol

Wheat Witch

The powers sort of seemed like they were starting to get to be busy work. The right side is certainly more interesting.

But making you do a bunch of proofs twice was annoying.

Huỳnh Trần Khanh

tbh i find the inequality level somewhat difficult but other levels are like normal

but this is because I've read about peano arithmetic before doing the NNG

Huỳnh Trần Khanh

11:52

remember: if you're stuck on a level, you can always read the solutions.

natural number game solutions: github.com/ImperialCollegeLondon/natural_number_game

2

can someone pin this link

emanresu A

Argh functions are confusing

Huỳnh Trần Khanh

@emanresuA use apply or have

hmm I'm still here, ping me if you have any questions

emanresu A

12:08

I should probably go to sleep now so o/

Huỳnh Trần Khanh

lol

good night

~~and this is the 4th time i post this message lol~~

6 hours ago, by Huỳnh Trần Khanh

hey could we have like a sync meeting or something to onboard new members? because there are many people who are new to lean and it would be hard to help over chat

I'm not being annoying or anything but lean is a very weird piece of software lol

Huỳnh Trần Khanh

12:22

just ignore the message i posted in tnb

and discuss it here lol

Huỳnh Trần Khanh

13:27

so... when people on the western side of the earth wake up, please: pin the NNG solution link (posted above), and tell me whether its okay for me to hold sync meetings or not

thank you

actually you can star that message

that would be ok too

Wheat Witch

Wake up? It's like 15:32 here. I just forgot to pin.

I'll add you and bubbler as ROs

Feeds

Wheat Witch has added Bubbler to the list of this room's owners.

Wheat Witch has added Huỳnh Trần Khanh to the list of this room's owners.

Wheat Witch

Now y'all can pin stuff when I'm not awake or not paying attention.

Huỳnh Trần Khanh

14:04

thanks

user

22:15

@HuỳnhTrầnKhanh Really? elan was not terribly hard to set up (no Windows installer, but all you do is run some stuff in cmd/pwsh)

Transcript for