(no topic)

Stream: general

[Kevin Buzzard]

So general chatter goes in "archives" topic?

[Kevin Buzzard]

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

[Andrew Ashworth]

no topic necessary for off-topic conversation

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Simon Hudon]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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

[Simon Hudon]

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

[Sean Leather]

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

[Kevin Buzzard]

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]

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

[Simon Hudon]

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]

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

[Mario Carneiro]

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]

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]

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

[Chris Hughes]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

pic1.png

[Kevin Buzzard]

he made that

[Kevin Buzzard]

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

[Kevin Buzzard]

it's like set_option pp.all

[Kevin Buzzard]

In fact we made it from the output of set_option pp.all and some emacs trickery and some python code

[Kevin Buzzard]

and then he made that in blender

[Kevin Buzzard]

red dots are functions, blue are evaluated terms

[Chris Hughes]

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]

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

[Kenny Lau]

yay you made it constructive :D

[Kenny Lau]

he made that

who?

[Simon Hudon]

His son I believe

[Kenny Lau]

oh

[Mario Carneiro]

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]

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

[gary]

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]

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

[Simon Hudon]

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]

Thanks

[Keeley Hoek]

(deleted)

[Nicholas Scheel]

(deleted)

[Namdak Tonpa]

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]

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

[Jason Rute]

(deleted)

[Cyril Cohen]

(deleted)

[Daniel Donnelly]

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

[Daniel Donnelly]

(deleted)

[Uranus Testing]

deleted

[Phiroc]

What is prod, exactly? Not mult, obviously.

[Mario Carneiro]

it is the type former for pairs

[Mario Carneiro]

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

[Mario Carneiro]

like cartesian product but with types instead of sets

[Mario Carneiro]

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

[Phiroc]

I see.

[Phiroc]

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

[Phiroc]

How would you write the proof?

[Kevin Buzzard]

Can you please reply on the correct thread?

[Kevin Lacker]

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]

rfl

[Kevin Lacker]

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

[Patrick Massot]

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

[Patrick Massot]

And then try by library_search

[Kevin Lacker]

ok. thanks!

[Johan Commelin]

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

(deleted)

[Yury G. Kudryashov]

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]

the first one.

[Yury G. Kudryashov]

And what are you trying to prove about Φ?

[Patrick Massot]

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]

That's true. I will do it.

[Kevin Lacker]

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]

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]

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]

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

[James Arthur]

(deleted)

[Kevin Buzzard]

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]

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]

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

[Bhavik Mehta]

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]

golfing is no excuse for poor formatting :P

[Bhavik Mehta]

I need some excuse to have bad formatting though :(

[Vaibhav Karve]

[Deleted message]

[Tomas Skrivan]

(deleted)

[Eric Wieser]

(deleted)

[Peter Nelson]

(deleted)

[François Sunatori]

(deleted)

[Yaël Dillies]

/poll What should the notation for order_dual be?
ᵒᵈ
﹥⇄﹤

[Notification Bot]

Eric Wieser has marked this topic as resolved.

[Notification Bot]

This topic was moved here from #general > Stating properties of monadic results by Eric Wieser.

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

(ugh, the double checkmarks when editing topic names get me every time)

[Notification Bot]

Eric Wieser has marked this topic as unresolved.