new member

Stream: new members

[Shaun Modipane]

hey im new

[Julian Berman]

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]

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]

post the link to the level

[Mario Carneiro]

and what you have done so far

[Shaun Modipane]

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

[Mario Carneiro]

and where are you stuck?

[Shaun Modipane]

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
im trying to solve this lemma

[Kevin Buzzard]

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]

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

[Huỳnh Trần Khanh]

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]

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

[Huỳnh Trần Khanh]

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]

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

[Scott Morrison]

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]

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

[Scott Morrison]

Then it will be called h instead of this.

[Scott Morrison]

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

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

[Scott Morrison]

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]

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

[Shaun Modipane]

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

[Johan Commelin]

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

[Shaun Modipane]

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]

the usual way it is done is to use induction c generalizing b instead of using revert explicitly

[Mario Carneiro]

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]

quick question, how did you get so good?
@Mario Carneiro

[Mario Carneiro]

lots of experience

[Mario Carneiro]

aka write lots of lean code

[Mario Carneiro]

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

[Shaun Modipane]

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

[Mario Carneiro]

tactic#induction

[Mario Carneiro]

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

[Mario Carneiro]

the ; there means to do intro b in all the subgoals

[Shaun Modipane]

how many years of experience in lean do you have?

[Mario Carneiro]

4 years or so? about 1 year before mathlib started

[Mario Carneiro]

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

[Mario Carneiro]

I'm just an old hand around here

[Shaun Modipane]

what projects are you interested in and why?
you can answer me later if you are busy.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

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]

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

[Huỳnh Trần Khanh]

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

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

[Damià Torres-Latorre]

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]

Can you post a #mwe?

[Damià Torres-Latorre]

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]

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

[Sebastien Gouezel]

#backticks

[Eric Rodriguez]

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]

well, your first issue right now is that fin 0 doesn't have any elements (and specifically no 1)!

[Eric Rodriguez]

you can use fin d.succ to get around this

[Eric Rodriguez]

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

[Kevin Buzzard]

The point is that you need to explicitly use hi, not just hope that the system magically notices it by itself.

[Anne Baanen]

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

[Damià Torres-Latorre]

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]

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]

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]

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]

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]

I think you want fin_rotate d i

[Damià Torres-Latorre]

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

[Yakov Pechersky]

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.