# Zulip Chat Archive

## Stream: general

### Topic: (no topic)

#### Kevin Buzzard (Feb 26 2018 at 18:50):

So general chatter goes in "archives" topic?

#### Kevin Buzzard (Feb 26 2018 at 18:51):

oh no I have made (no topic). Do I have to have a topic?

#### Andrew Ashworth (Feb 26 2018 at 18:51):

no topic necessary for off-topic conversation

#### Kevin Buzzard (Feb 26 2018 at 18:51):

I don't understand how to have off-topic conversation

#### Kevin Buzzard (Feb 27 2018 at 08:10):

Chris has already observed that mathematicians frequently want to sum from 0 to n, or 1 to n, and have a bunch of basic facts about such sums available to them. I know there are finsets and fintypes or whatever, but this case of summing from 0 to n or 1 to n is such a common usage case in maths. Is there already a specialised type for dealing specifically with such sums, which is easier to handle than dealing with general finsets? I am thinking about teaching induction to mathematicians without having to fill their heads with what I would call "specialised types" such as finset.

#### Kevin Buzzard (Feb 27 2018 at 08:10):

If not I might be tempted to build such things myself but I don't want to reinvent the wheel.

#### Simon Hudon (Feb 27 2018 at 08:12):

I was faced with a similar situation last year. The formulation of `sum`

I find is less than conducive to reasoning. I'm not sure if my lemmas about `foldl`

and `foldr`

are still around (I think they are now in mathlib) but your best bet I think is to prove `sum (xs ++ ys) = sum xs + sum ys`

. That should get you started at least

#### Mario Carneiro (Feb 27 2018 at 08:14):

DId you try `by simp`

? I think this is the consequence of several lemmas

#### Mario Carneiro (Feb 27 2018 at 08:15):

But I'm also working on a definition of sums over natural numbers to make this sort of thing easier

#### Kevin Buzzard (Feb 27 2018 at 08:25):

I didn't try simp because I was writing teaching materials and for some reason I wanted to be "explicit" about what was happening -- e.g. "this lemma with this name shows the fundamental fact which we will need, namely that the sum to n+1 is related to the sum to n in this obvious way". There is a danger with the sort of stuff I was doing that simp would just clear the goal completely and I know I can target it with (have blah, by simp) or whatever, but my goal was not to prove the lemma, it was to show math undergraduates how to use induction in Lean without any extra bells and whistles.

#### Kevin Buzzard (Feb 27 2018 at 08:26):

I suspect that in general as my thoughts about teaching progress I will want access to lemmas with possibly names that Mario disapproves of and which state things which he does not want in mathlib (e.g. because they can be done with a fold in one line or some such thing). Things like folds are what I am trying to avoid currently because I do not want to teach them any functional programming.

#### Kevin Buzzard (Feb 27 2018 at 08:27):

You CS guys might think this is mad, but look at Chris Hughes -- he showed up knowing a bit of matlab and had no idea what a functional program was, and I got him doing mathematics in Lean very quickly because of tactic mode. The more tactics / lemmas there are, the more mathematicians are able to stay away from the whole functional thing, and they can just get into it later when it all begins to make more sense.

#### Sean Leather (Feb 27 2018 at 08:29):

@Kevin Buzzard Not mad at all. Tactics are great for incrementally proving theorems.

#### Simon Hudon (Feb 27 2018 at 08:30):

I think that will limit how much you can do but there must still be interesting fragments

#### Sean Leather (Feb 27 2018 at 08:30):

... and this is coming from a CS guy, though, again, I'm not sure why that matters. :wink:

#### Kevin Buzzard (Feb 27 2018 at 08:31):

I think that you can get through a whole bunch of my introduction to proof course in Lean without really knowing too much about functional programming. I've seen it happen.

#### Kevin Buzzard (Feb 27 2018 at 08:32):

My job is not to teach functional programming, it is to teach rigorous thinking.

#### Simon Hudon (Feb 27 2018 at 08:32):

I think functional programming is especially hard to avoid as you're scaling up your proof efforts which often doesn't really come up in introductions

#### Sean Leather (Feb 27 2018 at 08:32):

@Kevin Buzzard I'm sure you're right. Why do you feel the need to defend that idea?

#### Mario Carneiro (Feb 27 2018 at 08:32):

If that's the kind of teaching you are going for, I recommend giving a direct inductive definition like it is done in TPIL

#### Kevin Buzzard (Feb 27 2018 at 08:33):

I would be interested to hear @Chris Hughes 's take on the issue. I am not sure he knows what a fold is but he has proved the fundamental theorem of arithmetic and much more in Lean.

#### Mario Carneiro (Feb 27 2018 at 08:33):

then you can give all the natural lemmas and prove basic properties and there is no hidden magic

#### Chris Hughes (Feb 27 2018 at 13:14):

I totally agree that tactics is the way to teach lean to maths students. I proved the fundamental theorem of arithmetic without even knowing what lambda did, and this gave me enough proficiency very quickly, that I've probably learnt a fair amount about functional programming, whatever that is, without really thinking about trying to learn functional programming.

#### Kevin Buzzard (Feb 27 2018 at 22:00):

Hey Patrick did you make an arbitrary product of rings a ring recently?

#### Kevin Buzzard (Feb 27 2018 at 22:10):

@Patrick Massot I need that now! But it's in gitter chat and it'll be hard to find :-/

#### Kevin Buzzard (Feb 27 2018 at 22:12):

Aah I've found it by looking through your github repos until I found the right commit :-)

#### Patrick Massot (Feb 28 2018 at 00:15):

Yes: https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/indexed_product.lean I will make a PR at some point

#### Kevin Buzzard (May 01 2018 at 20:02):

#### Kevin Buzzard (May 01 2018 at 20:02):

he made that

#### Kevin Buzzard (May 01 2018 at 20:03):

it's the syntax tree for my proof that sqrt(3) is irrational

#### Kevin Buzzard (May 01 2018 at 20:03):

it's like `set_option pp.all`

#### Kevin Buzzard (May 01 2018 at 20:04):

In fact we made it from the output of `set_option pp.all`

and some emacs trickery and some python code

#### Kevin Buzzard (May 01 2018 at 20:04):

and then he made that in blender

#### Kevin Buzzard (May 01 2018 at 20:05):

red dots are functions, blue are evaluated terms

#### Chris Hughes (May 01 2018 at 20:10):

I proved it for non integer nth roots of integers.

import data.nat.gcd algebra.group_power data.rat open nat int lemma nat.mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by induction n; simp [*, nat.pow_succ, mul_comm, mul_assoc, mul_left_comm] lemma nat.dvd_of_pow_dvd_pow : ∀ {a b n : ℕ}, 0 < n → a ^ n ∣ b ^ n → a ∣ b | a 0 := λ n hn h, dvd_zero _ | a (b+1) := λ n hn h, let d := nat.gcd a (b + 1) in have hd : nat.gcd a (b + 1) = d := rfl, match d, hd with | 0 := λ hd, (eq_zero_of_gcd_eq_zero_right hd).symm ▸ dvd_zero _ | 1 := λ hd, begin have h₁ : a ^ n = 1 := coprime.eq_one_of_dvd (coprime.pow n n hd) h, have := pow_dvd_pow a hn, rw [nat.pow_one, h₁] at this, exact dvd.trans this (one_dvd _), end | (d+2) := λ hd, have (b+1) / (d+2) < (b+1) := div_lt_self dec_trivial dec_trivial, have ha : a = (d+2) * (a / (d+2)) := by rw [← hd, nat.mul_div_cancel' (gcd_dvd_left _ _)], have hb : (b+1) = (d+2) * ((b+1) / (d+2)) := by rw [← hd, nat.mul_div_cancel' (gcd_dvd_right _ _)], have a / (d+2) ∣ (b+1) / (d+2) := nat.dvd_of_pow_dvd_pow hn $ dvd_of_mul_dvd_mul_left (show (d + 2) ^ n > 0, from pos_pow_of_pos _ (dec_trivial)) (by rwa [← nat.mul_pow, ← nat.mul_pow, ← ha, ← hb]), by rw [ha, hb]; exact mul_dvd_mul_left _ this end using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf psigma.snd⟩]} lemma int.nat_abs_pow (a : ℤ) (n : ℕ) : a.nat_abs ^ n = (a ^ n).nat_abs := by induction n; simp [*, nat.pow_succ, _root_.pow_succ, nat_abs_mul, mul_comm] lemma int.dvd_of_pow_dvd_pow {a b : ℤ} {n : ℕ} (hn : 0 < n) (h : a ^ n ∣ b ^ n) : a ∣ b := begin rw [← nat_abs_dvd, ← dvd_nat_abs, ← int.nat_abs_pow, ← int.nat_abs_pow, int.coe_nat_dvd] at h, rw [← nat_abs_dvd, ← dvd_nat_abs, int.coe_nat_dvd], exact nat.dvd_of_pow_dvd_pow hn h end lemma int.cast_pow {α : Type*} [ring α] (a : ℤ) (n : ℕ) : ((a ^ n : ℤ) : α) = (a : α) ^ n := by induction n; simp [*, _root_.pow_succ] def nth_root_irrational {x : ℤ} {a : ℚ} {n : ℕ} (hn : 0 < n) (h : a ^ n = x) : {a' : ℤ // a = a'} := have had : ((a.denom : ℤ) : ℚ) ≠ 0 := int.cast_ne_zero.2 (ne_of_lt (int.coe_nat_lt.2 a.3)).symm, ⟨a.num, begin rw [rat.num_denom a, rat.mk_eq_div, div_pow _ had, div_eq_iff_mul_eq (pow_ne_zero _ had), ← int.cast_pow, ← int.cast_mul, ← int.cast_pow, int.cast_inj] at h, have := int.coe_nat_dvd.1 (dvd_nat_abs.2 (int.dvd_of_pow_dvd_pow hn (dvd_of_mul_left_eq _ h))), have := coprime.eq_one_of_dvd a.4.symm this, rw [rat.num_denom a, rat.mk_eq_div, this], simp, end⟩

#### Kenny Lau (May 01 2018 at 20:13):

def nth_root_irrational {x : ℤ} {a : ℚ} {n : ℕ} (hn : 0 < n) (h : a ^ n = x) : {a' : ℤ // a = a'} :=

#### Kenny Lau (May 01 2018 at 20:13):

yay you made it constructive :D

#### Kenny Lau (May 01 2018 at 20:13):

he made that

who?

#### Simon Hudon (May 01 2018 at 20:18):

His son I believe

#### Kenny Lau (May 01 2018 at 20:19):

oh

#### Mario Carneiro (May 02 2018 at 09:01):

yay you made it constructive :D

Actually, it makes no difference since if a rational number is an integer, then you can obtain its value using `rat.num`

, or `rat.floor`

#### Mario Carneiro (May 02 2018 at 09:02):

(which is to say, that theorem would still be constructive with `exists`

)

#### gary (Jul 25 2018 at 20:31):

Hi all,

I'm working on applying formal methods to cryptocurrency protocols. We're a well funded startup (recently raised $20 million) and pay competetively.

If anyone has interest, please message me.

Thanks!

#### Jason Dagit (Aug 16 2018 at 16:38):

I have an expression that uses a type class instance. Is there a command to that prints out which instance was inferred?

#### Simon Hudon (Aug 16 2018 at 16:40):

Before the code printing the expression, use `set_option pp.implicit true`

so that the pretty printer shows more parts of your expression, namely, implicit parameters (which include class instances)

#### Jason Dagit (Aug 16 2018 at 16:41):

Thanks

#### Keeley Hoek (Aug 18 2018 at 11:57):

(deleted)

#### Nicholas Scheel (Dec 16 2018 at 04:49):

(deleted)

#### Namdak Tonpa (Jan 07 2019 at 16:32):

I know I'm flooding, but here is IRC bot written in pure Lean 3.4.1 (someone asked me in lounge)

https://github.com/forked-from-1kasper/leanbot

Can't wait to write WebSocket binary protocol for Lean4!

#### Moses Schönfinkel (Jan 07 2019 at 17:24):

This is the kind of flooding that is appreciated. By all means do continue to flood.

#### Jason Rute (May 20 2019 at 04:52):

(deleted)

#### Cyril Cohen (Jul 24 2019 at 09:13):

(deleted)

#### Daniel Donnelly (Aug 29 2019 at 03:06):

I'm not sure either how to make a "function that returns a string". I've tried 10 different thoughts on it :/

#### Daniel Donnelly (Sep 07 2019 at 14:17):

(deleted)

#### Uranus Testing (Mar 28 2020 at 11:41):

deleted

#### Phiroc (Apr 06 2020 at 11:16):

What is *prod,* exactly? Not *mult,* obviously.

#### Mario Carneiro (Apr 06 2020 at 11:17):

it is the type former for pairs

#### Mario Carneiro (Apr 06 2020 at 11:17):

`prod A B`

is the type of pairs of an element of A and an element of B

#### Mario Carneiro (Apr 06 2020 at 11:17):

like cartesian product but with types instead of sets

#### Mario Carneiro (Apr 06 2020 at 11:18):

it's usually written `A \times B`

or `A × B`

#### Phiroc (Apr 06 2020 at 11:19):

I see.

#### Phiroc (Apr 06 2020 at 11:20):

@Kevin Buzzard , but that's the proof provided by the author of the book.

#### Phiroc (Apr 06 2020 at 11:20):

How would you write the proof?

#### Kevin Buzzard (Apr 06 2020 at 11:21):

Can you please reply on the correct thread?

#### Kevin Lacker (May 22 2020 at 18:22):

simple noob question - how do I prove 1 + 1 = 2 in lean? it seems like it should be something built into "nat" but i can't find it

#### Patrick Massot (May 22 2020 at 18:22):

`rfl`

#### Kevin Lacker (May 22 2020 at 18:24):

ok thanks. how could I have figured that out without bugging you, is there some way I missed?

#### Patrick Massot (May 22 2020 at 18:25):

The first trick would have been to post this in the "new members" stream, with a topic.

#### Patrick Massot (May 22 2020 at 18:25):

And then try `by library_search`

#### Kevin Lacker (May 22 2020 at 18:26):

ok. thanks!

#### Johan Commelin (May 23 2020 at 05:39):

@Kevin Lacker Have you seen the tutorials? They definitely help. For example the natural number game. See #homepage for some links to get started

#### Ami (May 25 2020 at 16:18):

(deleted)

#### Yury G. Kudryashov (May 25 2020 at 16:41):

Is there any way to forbid "no topic" posts?

Ami, I don't understand what exactly you want to prove. If I interpret the definitions correctly, then you have

```
inductive M : Type
| one : M
| two : M
def Q (x : M) : Prop := x = M.two
def P (x : M) : Prop := x = M.one
```

How exactly do you define `Φ(x)`

: is it `(∀ y, Q y) → P x`

or `∀ y, (Q y → P x)`

?

#### Ami (May 25 2020 at 16:43):

the first one.

#### Yury G. Kudryashov (May 25 2020 at 16:43):

And what are you trying to prove about `Φ`

?

#### Patrick Massot (May 25 2020 at 16:43):

Ami, it will be much easier to get someone putting enough energy into answering your question if you put more energy asking it (eg. typing it and providing enough context)

#### Ami (May 25 2020 at 16:44):

That's true. I will do it.

#### Kevin Lacker (May 25 2020 at 20:29):

hmm, i was looking at what seems to be a totally different tutorial linked from a totally different home page, at https://leanprover.github.io/ .

#### Alex J. Best (May 25 2020 at 20:33):

That webpage is more closely linked to the last official lean release, as opposed to the work being dont by members of this chat on mathlib and the community fork (while we wait for lean 4). So I'd definitely recommend the https://leanprover-community.github.io/ version of everything.

#### Patrick Massot (May 25 2020 at 21:01):

Maybe it's time to kindly ask for a couple of links from https://leanprover.github.io/ to https://leanprover-community.github.io/

#### Kevin Buzzard (Jun 18 2020 at 07:29):

Google still puts all the official out of date pages ahead of the community pages when you're searching for lean

#### James Arthur (Jul 01 2020 at 08:32):

(deleted)

#### Kevin Buzzard (Sep 21 2020 at 16:27):

Nat golf anyone? I was writing lecture notes.

```
import tactic
example (n : ℕ) : (1 + 2 * n) / 2 = n :=
begin
have h2 := nat.mod_add_div (1 + 2 * n) 2,
have h3 : 2 * ((1 + 2 * n) / 2) = 2 * n →
(1 + 2 * n) / 2 = n := λ h, mul_left_cancel' _ h,
simp * at *, cc,
end
```

#### Shing Tak Lam (Sep 21 2020 at 16:51):

```
example (n : ℕ) : (1 + 2 * n) / 2 = n :=
nat.div_eq_of_lt_le (by linarith) (by {rw nat.succ_eq_add_one, linarith})
```

#### Bhavik Mehta (Sep 21 2020 at 20:58):

```
example (n : ℕ) : (1 + 2 * n) / 2 = n :=
(nat.add_mul_div_left 1 n (by simp)).trans (zero_add _)
```

#### Bhavik Mehta (Sep 21 2020 at 21:02):

I guess if we're golfing the proof:

```
example (n : ℕ) : (1 + 2 * n) / 2 = n :=
(nat.add_mul_div_left 1n(by simp)).trans$zero_add _
```

#### Mario Carneiro (Sep 21 2020 at 22:21):

golfing is no excuse for poor formatting :P

#### Bhavik Mehta (Sep 22 2020 at 16:08):

I need some excuse to have bad formatting though :(

#### Vaibhav Karve (Sep 23 2020 at 16:37):

[Deleted message]

#### Tomas Skrivan (Oct 29 2020 at 10:00):

(deleted)

#### Eric Wieser (Feb 16 2021 at 18:12):

(deleted)

#### Peter Nelson (Feb 20 2021 at 16:43):

(deleted)

#### François Sunatori (Mar 06 2021 at 20:01):

(deleted)

Last updated: May 16 2021 at 22:14 UTC