Stream: general

Topic: implication is not a function

Kevin Buzzard (Oct 30 2019 at 10:52):

Levels 2-6 and 3-8 represent branch points in [the natural number game v1.0]. The truth of the matter is that @Mohammad Pedramfar 's game maker currently will only let me let the user create a certain kind of structure, and basically I can't get the user to get from 2-6 to 3-1 without forcing other levels on them to add to their left hand box -- stuff I don't want them to see. I have only just realised that one can guide a mathematician to a tactic mode proof that the natural numbers are a commutative semiring -- this is "mathematician collectible #6" -- without ever being introduced to the concept of a function. It's just all manipulations of equalities, you can prove everything with rw. They never once prove P implies Q. @Emily Riehl -- you got confused because I accidentally left in an intro in and introduced you to the fact that Lean thinks of $P\implies Q$ as a function without any warning.

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/natural.20number.20game.20%28https.3A.2F.2Ftinyurl.2Ecom.2Fnatgame1234%29/near/179295674

The groupings of the levels are (2-1 to 2.6), (2-7 to 2-16), (3-1 to 3,8), ... Currently I want to write "Level 6 and a half -- you are not going to believe this -- they think that succ_inj is a function! rofl. Here, let me tell about this thing called intro.". What is going on here?

Kevin Buzzard (Oct 30 2019 at 10:57):

@Sian Carey was a UROP student with me from Leeds over the summer, and I gave her a really technically difficult problem about constructing a theory of quotient monoids and I found it absolutely fascinating teaching her, but there were some concepts which I could see I was teaching her poorly. And then I showed her the natural number game and said I needed a power world and she just knocked one off. There are secret collectibles in the natural number game, which I couldn't figure out how to add to the system in its current form but you can see them in the source code. Mathematicians like collecting them.

Emily Riehl (Oct 30 2019 at 11:41):

This explains a lot of the errors I've been getting! Let me try to remember where they were.

In 3.11 after the split I wanted to just type "exact eq_zero_or_eq_zero_of_mul_eq_zero,"

When that didn't work I tried "exact eq_zero_or_eq_zero_of_mul_eq_zero a b," (with various combinations of parentheses).

Finally I realized I could "apply the function" with something like:

intro hyp,
apply eq_zero_or_eq_zero_of_mul_eq_zero,
exact hyp,


Emily Riehl (Oct 30 2019 at 11:53):

Similarly I was hoping to compose succ_inj with the inductive hypothesis "hn : n + b = n + c → b = c," in 2.9 but instead had to settle for

intro hyp,
apply hn,
apply succ_inj,
exact hyp,


Kevin Buzzard (Oct 30 2019 at 12:07):

Yeah, this is the weird bit.

Kevin Buzzard (Oct 30 2019 at 12:09):

I need to tell you about have. You want to reason forwards because that's the way your $\implies$ goes. But their →goes backwards!

Kevin Buzzard (Oct 30 2019 at 15:30):

I have made things worse by trying to do something super-clever with fancy {{ brackets and breaking the thing which you instinctively want to do.

Luca Seemungal (Oct 30 2019 at 15:47):

This happened to me in world2! I had to put an @ before the theorem so I could move forward

Last updated: May 10 2021 at 00:31 UTC