Zulip Chat Archive

Stream: general

Topic: (no topic)


view this post on Zulip Kevin Buzzard (Feb 26 2018 at 18:50):

So general chatter goes in "archives" topic?

view this post on Zulip Kevin Buzzard (Feb 26 2018 at 18:51):

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

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 18:51):

no topic necessary for off-topic conversation

view this post on Zulip Kevin Buzzard (Feb 26 2018 at 18:51):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 27 2018 at 08:14):

DId you try by simp? I think this is the consequence of several lemmas

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sean Leather (Feb 27 2018 at 08:29):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 27 2018 at 08:32):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 27 2018 at 22:00):

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

view this post on Zulip 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 :-/

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:02):

pic1.png

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:02):

he made that

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:03):

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

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:03):

it's like set_option pp.all

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:04):

and then he made that in blender

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:05):

red dots are functions, blue are evaluated terms

view this post on Zulip 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

view this post on Zulip 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'} :=

view this post on Zulip Kenny Lau (May 01 2018 at 20:13):

yay you made it constructive :D

view this post on Zulip Kenny Lau (May 01 2018 at 20:13):

he made that

who?

view this post on Zulip Simon Hudon (May 01 2018 at 20:18):

His son I believe

view this post on Zulip Kenny Lau (May 01 2018 at 20:19):

oh

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 09:02):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Jason Dagit (Aug 16 2018 at 16:41):

Thanks

view this post on Zulip Keeley Hoek (Aug 18 2018 at 11:57):

(deleted)

view this post on Zulip Nicholas Scheel (Dec 16 2018 at 04:49):

(deleted)

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Jason Rute (May 20 2019 at 04:52):

(deleted)

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:13):

(deleted)

view this post on Zulip 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 :/

view this post on Zulip Daniel Donnelly (Sep 07 2019 at 14:17):

(deleted)

view this post on Zulip Uranus Testing (Mar 28 2020 at 11:41):

deleted

view this post on Zulip Phiroc (Apr 06 2020 at 11:16):

What is prod, exactly? Not mult, obviously.

view this post on Zulip Mario Carneiro (Apr 06 2020 at 11:17):

it is the type former for pairs

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 06 2020 at 11:17):

like cartesian product but with types instead of sets

view this post on Zulip Mario Carneiro (Apr 06 2020 at 11:18):

it's usually written A \times B or A × B

view this post on Zulip Phiroc (Apr 06 2020 at 11:19):

I see.

view this post on Zulip Phiroc (Apr 06 2020 at 11:20):

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

view this post on Zulip Phiroc (Apr 06 2020 at 11:20):

How would you write the proof?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 11:21):

Can you please reply on the correct thread?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 22 2020 at 18:22):

rfl

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 22 2020 at 18:25):

And then try by library_search

view this post on Zulip Kevin Lacker (May 22 2020 at 18:26):

ok. thanks!

view this post on Zulip 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

view this post on Zulip Ami (May 25 2020 at 16:18):

(deleted)

view this post on Zulip 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)?

view this post on Zulip Ami (May 25 2020 at 16:43):

the first one.

view this post on Zulip Yury G. Kudryashov (May 25 2020 at 16:43):

And what are you trying to prove about Φ?

view this post on Zulip 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)

view this post on Zulip Ami (May 25 2020 at 16:44):

That's true. I will do it.

view this post on Zulip 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/ .

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip 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

view this post on Zulip James Arthur (Jul 01 2020 at 08:32):

(deleted)

view this post on Zulip 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

view this post on Zulip 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})

view this post on Zulip 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 _)

view this post on Zulip 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 _

view this post on Zulip Mario Carneiro (Sep 21 2020 at 22:21):

golfing is no excuse for poor formatting :P

view this post on Zulip Bhavik Mehta (Sep 22 2020 at 16:08):

I need some excuse to have bad formatting though :(

view this post on Zulip Vaibhav Karve (Sep 23 2020 at 16:37):

[Deleted message]

view this post on Zulip Tomas Skrivan (Oct 29 2020 at 10:00):

(deleted)

view this post on Zulip Eric Wieser (Feb 16 2021 at 18:12):

(deleted)

view this post on Zulip Peter Nelson (Feb 20 2021 at 16:43):

(deleted)

view this post on Zulip François Sunatori (Mar 06 2021 at 20:01):

(deleted)


Last updated: May 16 2021 at 22:14 UTC