(no topic)

Stream: new members

[Andrew Ashworth]

This message has no topic

[Andrew Ashworth]

yes, you need to reply to threads explicitly, but small questions need not have their own topic, it seems

[Andrew Ashworth]

previously people were doing @person | quote "..." and then their reply

[Andrew Ashworth]

this is definitely better for a larger chat room. which hopefully will happen since Lean is going to be super popular

[Sebastian Ullrich]

I mean, the Gitter one is already larger than I can care to follow

[Andrew Ashworth]

are you ferinko

[Simon Hudon]

I was going to ask that! It will be weird referring to people by name instead of handle

[Patrick Massot]

Hi everyone!

[Andrew Ashworth]

well, Moses isn't actually his name either, haha

[Andrew Ashworth]

well, this is just the new members room, I didn't want to pollute #general with off topic comments

[Moses Schönfinkel]

It is?

[Moses Schönfinkel]

Interesting. I was apparently using the "all messages" tab which somehow forwarded to New Members automatically.

[Kevin Buzzard]

Well this is very modern.

[Kevin Buzzard]

I had trouble logging in with github, I had to go back a forth a while, but we got there in the end

[Sebastian Ullrich]

The design isn't exactly modern :laughing: . But other than that, I like it.

[Andrew Ashworth]

i wonder if there's an option to customize the css styling anywhere

[Sean Leather]

I also had trouble registering and signing in. Had to figure out which cookies to allow.

[Sean Leather]

What does the gray text mean?

[Sean Leather]

Oh, I think I see. It's a different channel?

[Andrew Ashworth]

everything on zulip is filtered by topic and stream

[Sean Leather]

Yeah, it's confusing to see different streams interleaved on one page.

[Simon Hudon]

If you click on a topic, you'll only see the messages that belong to that topic

[Andrew Ashworth]

probably want to deselect "all messages" at the top left of your screen then

[Andrew Ashworth]

zulip is what i think happened when a bulletin board and irc server had a lovechild

[Sean Leather]

It's the #new members view that I'm on. I don't yet know what topics I'm interested in, so I'm not sure which ones to look at.

[Sean Leather]

I don't see a way to merge topics. That would probably help.

[Andrew Ashworth]

if topics share something in common they should probably be filtered at the stream level

[Dan Abolafia]

(deleted)

[Kevin Buzzard]

(deleted)

[Nam]

somehow that line still worked ;).

[Kevin Buzzard]

You just changed thread. I am surprised it worked actually!

[Nam]

darn. i apologize. this tool needs some time to get used to.

[Lukas]

Hello,

I want to proof the following case:

case mynat.succ
t b d : mynat,
dh : t * (d + b) = t * d + t * b
⊢ t * (succ d + b) = t * succ d + t * b

my idea is to rw dh to get t * succ d + t * b on the left side. I think it should work because succ d should also be a mynat.

However I get

tactic failed, there are unsolved goals
state:
case mynat.succ
t b d : mynat,
dh : t * (d + b) = t * d + t * b
⊢ t * (succ d + b) = t * succ d + t * b

Did I missunderstood something or do I have to give an additional hint in the rw step?

[Kevin Buzzard]

You definitely can't do rw dh

[Kevin Buzzard]

If dh : A = B then rw dh will only work when there is something exactly equal to A in the goal

[Kevin Buzzard]

i.e. you really need exactly the symbols t * (d + b) in the goal for rw dh to work.

[Kevin Buzzard]

If dh said something like ∀ d, t * (d + b) = t * d + t * b then you would be OK. But it doesn't.

[Kevin Buzzard]

dh just says that something is true for that one specific d, not all d.

[Lukas]

Kevin Buzzard said:

i.e. you really need exactly the symbols t * (d + b) in the goal for rw dh to work.

okay thanks,

can I somehow substitute the succ d into a new variable and then it will work - or is that the wrong direction?

[Kevin Buzzard]

If induction was that easy, then you would be able to prove pretty much any statement by induction.

[Kevin Buzzard]

you have fixed naturals t and b and d, and dh is only a statement about those fixed naturals.

[Kevin Buzzard]

Look, here is a proof that for every natural number $n$, we have $n=n^2$.

[Kevin Buzzard]

Let's prove it by induction.

[Kevin Buzzard]

The base case is fine -- because $0=0^2$.

[Kevin Buzzard]

Now for the inductive step, let $n$ be any natural at all.

[Kevin Buzzard]

Let's assume h : n = n^2 and try and deduce succ n = (succ n)^2

[Kevin Buzzard]

By your way of thinking, n is an arbitrary natural number, so we can let it be succ n and use h to prove what we want to prove.

[Kevin Buzzard]

That can't be how induction works though, because what we're trying to prove isn't true.

[Lukas]

okay thanks for the explanation

[Jalex Stark]

(deleted)

[Golol]

(deleted)

[Jason Orendorff]

(deleted)

[Pedro Minicz]

(tmp)

[Michael Beeson]

So, the parameter M:Type that is mentioned in the class definition doesn't get passed automatically with the members of the class, in this case Rel and p44. I need to mention M in defining test. When I've successfully defined test, and I want to use it, I have to pass M as the first argument, e.g. test M. Then it's the passed M that will be used as the type of p44. That explains why you have to pass M as an argument to test. Are these statements correct?

[Kevin Buzzard]

These statements are in the wrong topic (and you could move them)

[Kevin Buzzard]

Look at the type of Rel. It takes M as an input.

[Kevin Buzzard]

#check @Rel

[Xavier Xarles]

(deleted)

[Patrick Lutz]

(deleted)

[Emiel Lanckriet]

Install mathematics_in_lean, I wanted to start looking at the online book Mathematics in Lean. I installed Lean in VS code as they suggested, but when I run the commando leanproject get mathematics_in_lean in Git Bash, the program ask for a password this is the exact response:
Please provide password for encrypted SSH private key:
However, there is no mention of a password in the text, so what is the password or where did I go wrong?

[Kevin Buzzard]

I think that this might be your SSH private key, if you set up SSH keys in github

[Kevin Buzzard]

GitHub is asking you to authenticate, it looks like

[Emiel Lanckriet]

Ok, I will take a look at that.

[Kevin Buzzard]

Stepping back a bit -- do you have a userid at the GitHub website?

[Emiel Lanckriet]

Yes

[Kevin Buzzard]

Ok so GitHub is perhaps saying "instead of providing your github password, just let me know that you are you, because you set up an ssh key at some point". I'm not an expert, this is kind of a guess.

[Filippo A. E. Nuccio]

(deleted)

[Malo Jaffré]

(deleted)

[Kevin Buzzard]

(deleted)

[Wrenna Robson]

If I have other questions on different kata, is it better etiquette here to start a new thread or continue this one?

[Jalex Stark]

Wrenna Robson said:

If I have other questions on different kata, is it better etiquette here to start a new thread or continue this one?

You probably meant to post this on some particular other thread. But generally it's good etiquette to start a new topic for every "different" question. Really the point is that you want to give people the opportunity to stop paying attention to topics they don't care about, and this is easier if individual topics are small

[Wrenna Robson]

Thanks!

[Hanting Zhang]

(deleted)

[Jakob Scholbach]

[Mark Gerads]

https://github.com/leanprover-community/mathlib/pull/6484#issuecomment-788189034
bors says:

Build failed (retrying...):

Build mathlib

But I see

@github-actions
continuous integration / Build mathlib (push) Successful in 118m
Details

Does this mean that my pull request somehow conflicted with another pull request which was accepted within the time since I downloaded Mathib, in which case, I should remake the pull request? This is my best guess as of now. I am unable to see the details of the fail.
When I press

@bors
bors — Build failed
Details

Permission denied

Thus I can only guess. Hmmm. May I have permission to see the details?

[Bryan Gin-ge Chen]

The Build mathlib link has all the details that are needed.

In this case, the issue was with another PR #6452: https://github.com/leanprover-community/mathlib/pull/6452#pullrequestreview-601069376

[Mark Gerads]

I need to know how to pull any recent changes from master to my branch. Maybe I should just delete the branch and start from scratch though; 'tis a simple solution.

[Bryan Gin-ge Chen]

For what it's worth, the bors page doesn't actually have much useful information in this case: Screen-Shot-2021-03-01-at-3.08.13-PM.png

(Sometimes when bors crashes the log page will have some crash log details...)

[Bryan Gin-ge Chen]

Mark Gerads said:

I need to know how to pull any recent changes from master to my branch. Maybe I should just delete the branch and start from scratch though; 'tis a simple solution.

I think your branch is fine, but for future reference, I think git fetch origin then git merge origin/master should work.

[Moritz Firsching]

(deleted)

[Kevin Buzzard]

(deleted)

[Hanting Zhang]

(deleted)

[Matúš Behun]

what's best way to find stuff in mathlib, so far i am using grep and file hierarchy, e.g. I am looking for definition of order or linear_order

[Eric Rodriguez]

my favourite is example : <stuff> := by library_search, although the docs with some decent keywords can be okay

[Matúš Behun]

cheers, hovering with mouse over keyword helped in this case

[Matúš Behun]

What's difference between constant and variable declaration

[Kevin Buzzard]

Can you ask this question in a thread with a topic name? Or edit the topic name for your post?

[Patrick Massot]

Did you read https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections? That would be the first step.

[Eric Wieser]

Zulip admins, can we turn off "no topic" topics? https://zulip.com/help/require-topics

[Rudi Cilibrasi]

We can help you install lean and mathlib if you have any difficulties. I installed to reproduce Mario result above that the zero function is the 5th program in partrec hehehe

[Eric Wieser]

(you can edit your message above to change the "topic" so that it moves to the right place)