# Zulip Chat Archive

## 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.

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: Aug 03 2023 at 10:10 UTC