implication is not a function

Stream: general

[Kevin Buzzard]

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]

@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]

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]

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]

Yeah, this is the weird bit.

[Kevin Buzzard]

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]

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]

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