# Zulip Chat Archive

## Stream: new members

### Topic: new member

#### Shaun Modipane (Jun 09 2021 at 06:01):

hey im new

#### Julian Berman (Jun 09 2021 at 06:25):

Hi! Welcome! There are some learning materials on the community site if you haven't already seen those. The natural number game listed first there is super good to get started.

(And people here are really nice, so feel free to just ask questions whenever you have them.)

#### Shaun Modipane (Jun 09 2021 at 06:29):

hey man thanks, my problem is I'm stuck on a level in the natural number game and i dont know how to ask/show the problem here in zulip

#### Mario Carneiro (Jun 09 2021 at 06:30):

post the link to the level

#### Mario Carneiro (Jun 09 2021 at 06:31):

and what you have done so far

#### Shaun Modipane (Jun 09 2021 at 06:31):

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

like this

#### Mario Carneiro (Jun 09 2021 at 06:34):

and where are you stuck?

#### Shaun Modipane (Jun 09 2021 at 07:11):

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=

im trying to solve this lemma

#### Kevin Buzzard (Jun 09 2021 at 07:27):

I can't remember what NNG explains but I guess you can either use zero_ne_succ or succ_ne_zero or whatever you have, or you can just attack an `x ≠ 0`

directly with `intro hx`

#### Huỳnh Trần Khanh (Jun 09 2021 at 07:38):

First off you have to introduce the hypotheses. Have you done that? Run `intro h1, intro h2,`

.

#### Huỳnh Trần Khanh (Jun 09 2021 at 07:40):

Then you have to do `cases`

on `a`

and `b`

. You will get two cases: zero and succ. Ah, there are two variables, so you will get four cases.

#### Huỳnh Trần Khanh (Jun 09 2021 at 07:40):

And then with some exfalso and the existing theorems, you can clear the goal.

#### Huỳnh Trần Khanh (Jun 09 2021 at 07:44):

This is the solution:

```
intros h1 h2,
cases a,
have : zero = zero := by refl,
exfalso,
exact h1 this,
cases b,
have : zero = zero := by refl,
exfalso,
exact h2 this,
rw mul_succ,
rw add_succ,
apply succ_ne_zero,
```

#### Shaun Modipane (Jun 09 2021 at 07:54):

okay thanks, the this keyword is new, and is a game changer. is it possible to explain it's function.

#### Scott Morrison (Jun 09 2021 at 08:05):

When you write `have : T := V`

, (where `T`

is a type and `V`

is a term of that type), you create a new hypothesis which is named `this`

by default.

#### Scott Morrison (Jun 09 2021 at 08:05):

You can (and often should) explicitly name it yourself using `have h : T := V`

.

#### Scott Morrison (Jun 09 2021 at 08:05):

Then it will be called `h`

instead of `this`

.

#### Scott Morrison (Jun 09 2021 at 08:06):

(My preference is to _always_ provide an explicit name if it is ever directly referred to again later. But this isn't enforced in mathlib; `this`

is considered okay.)

#### Scott Morrison (Jun 09 2021 at 08:06):

Also, @Huỳnh Trần Khanh suggestion above would be better if it used braces to separate proofs of subgoals!

#### Scott Morrison (Jun 09 2021 at 08:07):

You don't need to write `have : zero = zero := by refl`

. This unnecessarily jumps back and forth between term and tactic mode. Better to write `have : zero = zero := rfl`

, or `have : zero = zero, refl`

.

Even better is to not even introduce `this`

, and just write `exact h1 rfl`

.

#### Shaun Modipane (Jun 09 2021 at 09:01):

thanks, i got it, hope we could work together on other projects.

#### Shaun Modipane (Jun 09 2021 at 10:52):

how do you guys handle goals that impossible to prove, like ⊢ succ b = 0.

#### Johan Commelin (Jun 09 2021 at 10:56):

@Shaun Modipane I hope that you also have a hypothesis that is false, otherwise you are stuck

#### Shaun Modipane (Jun 12 2021 at 09:51):

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4

who can solve this problem without revert tactic

#### Mario Carneiro (Jun 12 2021 at 09:54):

the usual way it is done is to use `induction c generalizing b`

instead of using `revert`

explicitly

#### Mario Carneiro (Jun 12 2021 at 10:00):

```
intro h,
induction c with c ih generalizing b,
{ rw [mul_zero, mul_eq_zero_iff] at h,
exact h.resolve_left ha },
cases b,
{ rw [mul_zero, eq_comm, mul_eq_zero_iff] at h,
exact (h.resolve_left ha).symm },
{ rw [mul_succ, mul_succ, add_right_cancel_iff] at h,
congr, exact ih _ h },
```

#### Shaun Modipane (Jun 12 2021 at 10:08):

quick question, how did you get so good?

@Mario Carneiro

#### Mario Carneiro (Jun 12 2021 at 10:09):

lots of experience

#### Mario Carneiro (Jun 12 2021 at 10:09):

aka write lots of lean code

#### Mario Carneiro (Jun 12 2021 at 10:10):

and put it where other people can critique it (e.g. mathlib PRs)

#### Shaun Modipane (Jun 12 2021 at 10:10):

what does generalizing b do? if you can can you send me the Mathlib doc.

#### Mario Carneiro (Jun 12 2021 at 10:10):

#### Mario Carneiro (Jun 12 2021 at 10:11):

it's basically the same as `revert b, induction c; intro b`

#### Mario Carneiro (Jun 12 2021 at 10:11):

the `;`

there means to do `intro b`

in all the subgoals

#### Shaun Modipane (Jun 12 2021 at 10:11):

how many years of experience in lean do you have?

#### Mario Carneiro (Jun 12 2021 at 10:12):

4 years or so? about 1 year before mathlib started

#### Mario Carneiro (Jun 12 2021 at 10:13):

but you don't need that much time to get good

#### Mario Carneiro (Jun 12 2021 at 10:14):

I'm just an old hand around here

#### Shaun Modipane (Jun 12 2021 at 10:15):

what projects are you interested in and why?

you can answer me later if you are busy.

#### Mario Carneiro (Jun 12 2021 at 10:24):

I started doing formal proving in the metamath system, I thought it was interesting and fun to build all of mathematics the "right way", and I spent several years doing that before I got a PhD position to work on lean. I still think formal maths is the future, and a lot of the basics in mathlib is my work, although it has since grown further than I can keep track. I haven't done too much mathlib of late though, because I've been working on Metamath Zero, a theorem prover design which focuses on speed and correctness, pulling inspiration from metamath and lean. In particular, I am working on a *verified* theorem prover for MM0, relative to a specification of the hardware. Really, I would like to see *all* theorem provers have verified backends, but there are ways to leverage one verified theorem prover to verify the products of other projects like mathlib.

#### Huỳnh Trần Khanh (Jun 12 2021 at 10:43):

You are getting really good responses here, I recommend that you refrain from DMing specific users unless absolutely necessary. Thanks.

#### Mario Carneiro (Jun 12 2021 at 10:45):

You can also use private messages to talk to particular users in zulip fyi

#### Huỳnh Trần Khanh (Jun 12 2021 at 10:45):

I'm not against DMs, just that I have a very peculiar personality and that might make you uncomfortable unless you know me really well. :joy::joy::joy:

#### Huỳnh Trần Khanh (Jun 12 2021 at 10:45):

@Mario Carneiro well, they PM'd me and I declined to respond LOL

#### Huỳnh Trần Khanh (Jun 12 2021 at 10:56):

@Shaun Modipane I'm quoting your message here.

hey man, i hope i'm not bothering you but i want to ask. how did you get so good in lean and where did you get the exercise from

By abusing this Zulip chat as a human flesh powered search engine. Seriously. You can't really Google anything about Lean so... Just ask questions. Why are you interested in Lean? Maybe to formalize a math problem? Then you can post the problem statement on here and ask for guidance.

The more you ~~shitpost~~, the better you get. Seriously.

#### Huỳnh Trần Khanh (Jun 12 2021 at 10:57):

I've posted half coherent questions and and still got pretty decent answers. This community is really helpful.

#### Damià Torres-Latorre (Jun 17 2021 at 08:46):

Hi I'm new. I have played the natural number game and did some tutorials. Now I'm starting to try to prove some things on my own. I don't really understand the logic of the zulip chat yet, so please redirect my question to wherever it belongs.

So, to represent vectors of R^n, I am doing them as v : fin n \to R. Now if I want to have the i-th component of the vector I can do just v i, where i belongs to fin n. But if I want to have the (i+1)-th component, I tried to do v (i+1) but it does not work.

Is this trivial? What can I upload if not?

#### Eric Rodriguez (Jun 17 2021 at 08:49):

Can you post a #mwe?

#### Damià Torres-Latorre (Jun 17 2021 at 08:57):

import tactic

import data.set.finite

import data.real.basic

noncomputable theory

open set

variable d : ℕ

local notation `E`

:= fin d → ℝ

lemma ordered_vertices_implies_epsilon_fixed

(i : fin d) (hi : ↑i < d - 1) (p : fin d → E) (f : E → E) (hfp : f (p (i+1)) i ≥ (p (i+1)) i) : 0 = 0

:= sorry

#### Damià Torres-Latorre (Jun 17 2021 at 08:57):

how do I post the mwe in a way such that it looks like code here?

#### Sebastien Gouezel (Jun 17 2021 at 08:58):

#### Eric Rodriguez (Jun 17 2021 at 08:58):

you can wrap it in 3 backticks (`), like this:

```
import tactic
import data.set.finite
import data.real.basic
noncomputable theory
open set
variable d : ℕ
local notation E := fin d → ℝ
lemma ordered_vertices_implies_epsilon_fixed
(i : fin d) (hi : ↑i < d - 1) (p : fin d → E) (f : E → E) (hfp : f (p (i+1)) i ≥ (p (i+1)) i) : 0 = 0
:= sorry
```

#### Eric Rodriguez (Jun 17 2021 at 09:03):

well, your first issue right now is that `fin 0`

doesn't have any elements (and specifically no 1)!

#### Eric Rodriguez (Jun 17 2021 at 09:03):

you can use `fin d.succ`

to get around this

#### Eric Rodriguez (Jun 17 2021 at 09:03):

but this can still be weird; for example, in `fin 1`

, `1=0`

#### Kevin Buzzard (Jun 17 2021 at 09:04):

The point is that you need to explicitly use `hi`

, not just hope that the system magically notices it by itself.

#### Anne Baanen (Jun 17 2021 at 09:04):

There is also docs#fin_rotate, which is exactly the permutation you're looking for on all `fin n`

.

#### Damià Torres-Latorre (Jun 17 2021 at 09:05):

Ok, thanks, that makes sense. How do I use hi? Also, is hi doing what I think it is doing? (discarding the last element of fin d)

#### Kevin Buzzard (Jun 17 2021 at 09:05):

I guess `hi`

is not quite doing what you expect it to do, because natural number subtraction isn't quite doing what you might expect, as 0 - 1 = 0.

#### Damià Torres-Latorre (Jun 17 2021 at 09:11):

I do not understand how to use fin_rotate, sorry

Also it is true that hi does not work, if I write

```
hi : \u i + 1 < d
```

would that work?

#### Kevin Buzzard (Jun 17 2021 at 09:14):

Yes, that variant of `hi`

is probably exactly what you want. A term of type `fin d`

is a *pair* consisting of a natural number `n`

and a proof that `n < d`

. The up-arrow just forgets the proof. In particular a term of type `fin d`

is not a natural number; all this took a while to dawn on me. Because of all this, you can't just expect to be able to do arithmetic on terms of type `fin d`

, because if `i : fin d`

then it's hard to guess what `i + 1`

means in general (because there _could_ be overflow, whether or not there is in your situation). `fin_rotate`

is just the "add 1 mod d" function.

#### Damià Torres-Latorre (Jun 17 2021 at 09:20):

All right, thank you. I get what fin_rotate does morally, but I still do not understand how to use it, because fin_rotate i returns an equiv.perm object, which is not anymore of the correct type, and I have not been able to coerce it into fin d again

#### Kevin Buzzard (Jun 17 2021 at 09:37):

I think you want `fin_rotate d i`

#### Damià Torres-Latorre (Jun 17 2021 at 09:39):

Ok, so fin_rotate d is a permutation of fin d, got it, thank you!

#### Yakov Pechersky (Jun 17 2021 at 12:06):

An equiv.perm is automatically coerced into a function, when it is used as Kevin showed. I also think that instead of writing arrows for coercing fin, it's clearer for you and the reader if you write the type ascriptions explicitly, like (i : nat) + 1 < d. Yes, the pretty printer will still show the arrow, but your code will be more interpretable by other readers.

Last updated: Dec 20 2023 at 11:08 UTC