Zulip Chat Archive

Stream: new members

Topic: Diagonal Ramsey Number Lower Bound


view this post on Zulip Sam Raleigh (Apr 25 2020 at 08:03):

Hello there!

TLDR: Is there a tactic that allows me to prove goals of the form "there exists..." with the probabilistic method?

I'd like to prove Erdos' classical lower bound on the diagonal Ramsey numbers R(k){R}(k) with Lean. For the following, note that KmK_m refers to the complete graph on mm vertices and E(G)E(G) is the edge set of graph GG. The diagonal Ramsey number R(k){R}(k) is the smallest number nn such that for any 2-coloring of the edges of KnK_n, there is a monchromatic KkK_k subgraph of KnK_n (i.e. a KkK_k subgraph where either all the edges are blue or all the edges are red). Ramsey proved in 1929 that R(k)R(k) is finite for all kk, but finding the exact number is much more challenging! Here is the theorem I am trying to prove and its proof for reference:

proof1.jpeg
proof2.jpeg

If I were just to prove that R(k)>nR(k) > n given the necessary inequality on nn and kk in Lean, I expect my goal for the proof would look like something along the lines of "there exists some c:E(Kn){red,blue}c : E(K_n) \rightarrow \{red, blue\} such that for every HKnH \subseteq K_n where HKkH \cong K_k there exists e1,e2E(H)e_1, e_2 \in E(H) such that c(e1)c(e2)c(e_1) \neq c(e_2).

Now, onto my question: What tactic would I use to prove a goal of the form "there exists..." in Lean with a non-constructive proof? The only way I know how to prove existence goals is with the use tactic, but as you can see the proof pictured above does not construct anything that I could give the use tactic. Instead the argument is that since there is a positive probability that a random 2 coloring of KnK_n has no monochromatic KkK_k subgraphs, then there is some coloring in the space of random colorings of KnK_n which has no monochromatic KkK_k subgraph. What tactic could I use to prove the goal with such an argument?

view this post on Zulip David Wärn (Apr 25 2020 at 08:19):

I think you want something like this, to translate an existential statement into the negation of a universal statement

example (α : Type) (P : α  Prop) (h : ¬  a, ¬ P a) :  a, P a :=
by {push_neg at h, assumption}

There's probably a more idiomatic way of writing this, but push_neg is convenient whenever you want to get rid of negations in a complicated Prop

view this post on Zulip David Wärn (Apr 25 2020 at 08:27):

There are two different ways to say "this colouring does not satisfy Ramsey": there's the one you mentioned of "for any subset there are two edges with distinct colours", and there's "there is no subset that is mono". Of course the two formulations are equivalent (via push_neg or something), so feel free to choose whichever formulation is more convenient

view this post on Zulip Jalex Stark (Apr 25 2020 at 08:28):

The details will depend on how you implement your probability distribution

view this post on Zulip Jalex Stark (Apr 25 2020 at 08:28):

i don't know of really any development of probability theory in Lean

view this post on Zulip Sam Raleigh (Apr 25 2020 at 08:31):

Thank you both for your answers. Jalex's comment has me wondering if I'm thinking too far ahead. I might need to rely on a version of the proof that is a counting argument instead. I was unaware that Lean didn't have any probability theory : (

view this post on Zulip David Wärn (Apr 25 2020 at 08:31):

@Bhavik Mehta actually formalized this particular argument here: https://github.com/b-mehta/combinatorics/blob/graphs/src/lower_ramsey.lean
My understanding is that for this argument you just need cardinalities of finite sets, or finset.card

view this post on Zulip David Wärn (Apr 25 2020 at 08:31):

Lean does have probability theory though!

view this post on Zulip Jalex Stark (Apr 25 2020 at 08:32):

where? mathlib has a little bit of measure theory

view this post on Zulip Sam Raleigh (Apr 25 2020 at 08:34):

Thanks for the find David! I'll have to take a good look into this later

view this post on Zulip David Wärn (Apr 25 2020 at 08:35):

Yes I wouldn't know if there are actually enough facts about probability that you could formalize this sort of arguments comfortably

view this post on Zulip David Wärn (Apr 25 2020 at 08:37):

But you can at least talk about probability mass functions. @Johan Commelin made an attempt at formailizing Erdos' probabilistic proof that there are graphs with high chromatic number and high girth in this language
https://github.com/leanprover-community/mathlib/blob/hedetniemi/src/graph_theory/random_graph.lean
I think at the moment it's unclear what the best way of formulating probabilistic arguments is

view this post on Zulip Bryan Gin-ge Chen (Apr 25 2020 at 08:41):

@Koundinya Vajjha proved the Markov and Chebyshev inequalities here: https://github.com/jtristan/stump-learnable/blob/81b3854a8ef9ce4329ed1bb6f0e5528ec2ca136f/src/lib/attributed/to_mathlib.lean

view this post on Zulip Bhavik Mehta (Apr 25 2020 at 11:14):

Just to chime in, David's exactly right that my proof just used cardinalities of finite sets - the argument is the exact same as the one you posted though, just phrased in terms of cardinalities rather than probabilities. I'm of the opinion that at the moment, cardinality arguments are the easiest way to prove this sort of thing in lean - there's a lot of api for finsets already there

view this post on Zulip Sam Raleigh (Apr 25 2020 at 18:23):

@Bhavik Mehta Thank you for your reply. What exactly do you mean by "phrased in terms of cardinalities rather than probabilities"?

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 18:27):

Instead of using the language of probability, one can "clear denominators" and make claims about sizes of sets instead. For example, to prove "there exists..." using the probabilistic language one would prove that the probability that a random structure satisfied your property is a positive real. To prove it using the cardinality language one would prove that the cardinality of the structures which had the property was a positive integer.

view this post on Zulip Sam Raleigh (Apr 25 2020 at 18:28):

I see, thank you

view this post on Zulip Sam Raleigh (Apr 28 2020 at 13:19):

Wasn't sure that my other questions were non-trivial enough to deserve their own topic, but I'll just post them here instead. Also sorry I thought I provided an MWE earlier. What else do you need @Mario Carneiro ? The casting isssue has gone away but now I have:

don't know how to synthesize placeholder
context:
n k : ℕ,
h : n ≥ k
⊢ Type ?

Occurring at mono_sub_colorings

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:20):

You had an example of an error talking about real when applying choose to too many arguments, I want to reproduce that

view this post on Zulip Patrick Massot (Apr 28 2020 at 13:20):

Sam Raleigh said:

Wasn't sure that my other questions were non-trivial enough to deserve their own topic

This is not the right attitude. And you still aren't posting MWE.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 13:20):

the more topics the better :-)

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 13:20):

(as we just saw)

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:22):

I think there will always be some fraction of people who think this way, and this is their first post so we don't have a chance to intercept. The "noob questions" thread is unkillable

view this post on Zulip Patrick Massot (Apr 28 2020 at 13:23):

Sure, we simply need to keep moving people out of it.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:23):

I think we can probably have a rule saying that if the discussion goes beyond problem -> MWE please -> what's an MWE -> MWE given -> solution then it should go into its own topic post facto

view this post on Zulip Sam Raleigh (Apr 28 2020 at 13:23):

import data.nat.basic
import data.int.basic
import data.rat.basic

import algebra.field_power

import tactic

import data.finset
import algebra.big_operators
import data.real.basic
import data.set.lattice

open finset
open nat

local notation `edges_of `X := powerset_len 2 X

universe u
variables {α : Type u} (K : finset α) {n : } [decidable_eq α]

def mono_sub_colorings (n : ) (k : ) : finset (finset (finset α)) := sorry

lemma num_mono_sub_colorings (n k : ) (h : n  k)
  : (card (mono_sub_colorings n k) : ) = ((2 : )^((n.choose(2)) - (k.choose(2))) : ) * n.choose(k) :=
begin
  sorry,
end

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:42):

Here's a minimized example:

import tactic data.real.basic

variable (n : )
#check λ x, n x

Apparently, nat coerces to int, which coerces to cau_seq real int because cau_seq real int is a ring, and cau_seq real int has a coe_fn instance to nat -> real. So with these imports you can apply one nat to another and you get a real. :shrug:

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:42):

This is why I don't like transitive coercions

view this post on Zulip Reid Barton (Apr 28 2020 at 13:45):

So what real do you get?

view this post on Zulip Reid Barton (Apr 28 2020 at 13:45):

n?

view this post on Zulip Reid Barton (Apr 28 2020 at 13:46):

Mario Carneiro said:

cau_seq real int

This can't be what you meant, right?

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:47):

sorry, cau_seq real abs

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:51):

import tactic data.real.basic

example (a b : ) : a b = a :=
by induction a; [refl, {apply_fun (λ x:, x+1) at a_ih, exact a_ih}]

view this post on Zulip Reid Barton (Apr 28 2020 at 13:57):

https://www.destroyallsoftware.com/talks/wat

view this post on Zulip Patrick Massot (Apr 28 2020 at 13:58):

not exactly the hall of fame we were targeting...

view this post on Zulip Reid Barton (Apr 28 2020 at 14:11):

I wonder how far we could get by elaborating x y when x is not a function to x.to_fun y, combined with the proposal to search "superclass" namespaces

view this post on Zulip Reid Barton (Apr 28 2020 at 14:12):

Or even without that second part.

view this post on Zulip Reid Barton (Apr 28 2020 at 14:32):

In any case,

instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_fun.{u₂ u₃} b] [has_coe_t_aux a b] : has_coe_to_fun.{u₁ u₃} a :=

and perhaps

instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_sort.{u₂ u₃} b] [has_coe_t_aux a b] : has_coe_to_sort.{u₁ u₃} a :=

seem particularly dubious; possibly we can just delete them?

view this post on Zulip Johan Commelin (Apr 28 2020 at 14:32):

What happens if you try?

view this post on Zulip Reid Barton (Apr 28 2020 at 14:32):

I would have to wait a few hours for mathlib to finish building, I imagine?

view this post on Zulip Reid Barton (Apr 28 2020 at 14:33):

I'm happy to try this but I cannot offer instant feedback :slight_smile:

view this post on Zulip Reid Barton (Apr 28 2020 at 14:34):

(hopefully I can offer instance feedback)

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:12):

Could someone please explain why I'm getting a "don't know how to synthesize placeholder context" issue (and what this means) on card in the following code? Also just to be sure, is this an appropriate MWE for the problem at hand?

import data.finset
open finset

universe u
variable α : Type u

def mono_sub_colorings (n : ) (k : ) : finset (finset (finset α)) := sorry

lemma test (n k : ) : card (mono_sub_colorings n k) = n.choose(k) :=
begin
  sorry
end

Thank you!

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:14):

the type of \acannot be inferred

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:15):

but this is not an MWE because it does not compile (I only compiled it with my eyes though so I'm not 100% sure)

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:17):

Thanks! I copied and pasted this exact code into a separate lean file and it compiles (aside from this issue you just fixed).

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:17):

well the MWE would be mono_sub_colorings _ n k

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:18):

and then my comment of the type of \a not able to be inferred would apply

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:18):

also this is not python, we write n.choose k here

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:19):

Thank you for the clarification. Wouldn't a person seeking to assist with the problem want to know what mono_sub_colorings was?

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:20):

Perhaps I don't understand the definition of an MWE

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:20):

And what do you mean by your last comment? I did write n.choose(k), no?

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:21):

o wait

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:21):

I see what you mean

view this post on Zulip Reid Barton (Apr 28 2020 at 16:21):

I think Kenny is being somewhat unreasonable. If the issue is that some code is not compiling, then we want to be able to verify that the same code does not compile. It is not supposed to be "W" in the sense of working/compiling then!

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:22):

well this is just a misunderstanding.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:25):

Ah I think I'm starting to get it. So by "don't know how to synthesize placeholder" Lean means that it is unsure what argument to insert in the underscore in mono_sub_colorings _ n k, yes?

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:26):

right

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:41):

Given universe u, what is the difference between variables {α : Type u} and variables α : Type u?

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:45):

if you prove a theorem / make a definition using the latter then you don't need to supply \a and Lean will try to infer \a

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:46):

Thanks!

view this post on Zulip Bryan Gin-ge Chen (Apr 28 2020 at 16:47):

Obligatory TPiL link. See also 6.5.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 16:48):

The former!

view this post on Zulip Kenny Lau (Apr 28 2020 at 16:51):

I stand corrected.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:56):

Judging by what Kevin said, I'd think that variable {\a : u} would allow me to have lemma test (n k : ℕ) : card (mono_sub_colorings n k) = n.choose(k) := sorry without any issues. So why am I getting a cannot synthesize placeholder error?

view this post on Zulip Reid Barton (Apr 28 2020 at 16:57):

Kevin said Lean would try to infer \a, not that it would succeed.

view this post on Zulip Reid Barton (Apr 28 2020 at 16:57):

How would it know what type to pick?

view this post on Zulip Sam Raleigh (Apr 28 2020 at 16:58):

Wouldn't it be able to infer it from the definition of mono_sub_colorings?

view this post on Zulip Reid Barton (Apr 28 2020 at 17:00):

But what even is the correct answer? There isn't one.

view this post on Zulip Reid Barton (Apr 28 2020 at 17:00):

If this isn't clear, imagine adding variable {\b : Type u}, or even deleting variable {\a : Type u}.

view this post on Zulip Reid Barton (Apr 28 2020 at 17:01):

Who knows, Lean seems to like the type nat -> real so maybe that is a good choice.

view this post on Zulip Reid Barton (Apr 28 2020 at 17:05):

If you like, the point is that card could take a finset of anything, so that's precisely the point where we lose the ability to determine the implicit parameter of mono_sub_colorings.

view this post on Zulip Reid Barton (Apr 28 2020 at 17:05):

No matter what that parameter is, this equation will type check.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 17:08):

I see. So how do I fix it? If I try Kenny's suggestion lemma test (n k : ℕ) : card (mono_sub_colorings α n k) = n.choose k := sorry, then I get a type mismatch because \ais expected to be of type nat.

view this post on Zulip Reid Barton (Apr 28 2020 at 17:10):

card (@mono_sub_colorings α n k)
or
card (mono_sub_colorings n k : finset (finset (finset α)))

view this post on Zulip Reid Barton (Apr 28 2020 at 17:10):

@ means "I'm going to give all the parameters including the implicit ones".

view this post on Zulip Sam Raleigh (Apr 28 2020 at 17:12):

I was wondering how to do this, thank you.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 20:49):

import algebra.field_power

lemma core_ineq
    {a b c : }
    (h : ((2 : )^(1 - b : ) * c : ) < 1) :
    (2^(a - b : ) * 2 * c : ) < (2^a : ) :=
begin

  --stuff

  have h0 : 0 < 2^a := sorry,
  have h1 : (2^a * 2 ^ 1 / 2 ^ b * c < 2^a * 1) := by exact mul_lt_mul_of_pos_left h h0,

  --other stuff

end

How do I fix the type mismatch at mul_lt_mul_of_pos_left?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:51):

    mul_lt_mul_of_pos_left ?m_6 ?m_7
  has type
    ?m_3 * ?m_4 < ?m_3 * ?m_5
  but is expected to have type
    2 ^ a * 2 ^ 1 / 2 ^ b * c < 2 ^ a * 1

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:52):

Your right hand side says ?m_3 must be 2^a but the left hand side is not of the form 2^a * X

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:00):

(because of associativity conventions)

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:01):

Is that the error you got? I mean thank you for pointing that out as I would have had to fix it eventually, but I got this error:

type mismatch at application
  mul_lt_mul_of_pos_left h h0
term
  h0
has type
  0 < 2 ^ a
but is expected to have type
  0 < ?m_1

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:02):

Read more?

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:03):

Had my eyes only looked an inch farther down on the screen, I would not have needed to ask such a silly question. Thanks Kevin : D

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:03):

Learning to read Lean error messages takes a long time

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:04):

and I remember the power I felt I had once I realised that more often than not I could actually turn the information in the error message into a way of figuring out how to fix my code

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:05):

That'll be the day...

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:05):

I think the error just means "I'm trying to match up all the metavariables but I am hopelessly stuck, I can't even solve for the first one: here's what I was thinking"

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:05):

I get a particularly difficult to read error message when I add the parentheses:

have h1 : 2^a * (2 ^ 1 / 2 ^ ↑b * ↑c) < 2^a * 1 := by exact mul_lt_mul_of_pos_left h h0,

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

Everything has to match exactly for this lemma to work, your h0 does not say what you want it to say.

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

2^(1-\u b) might look the same as 2^1/2^\u b to you but it's certainly not definitionally equal to it

view this post on Zulip Reid Barton (Apr 28 2020 at 21:07):

this is part of why backwards reasoning flows more smoothly

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:08):

@Kevin Buzzard the "stuff" part of my code handles that

view this post on Zulip Reid Barton (Apr 28 2020 at 21:08):

h0 is also wrong, though

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:08):

Sorry I should have posted the full thing

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:09):

Give me one moment

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:09):

lemma core_ineq
    {a b c : }
    (h : ((2 : )^(1 - b : ) * c : ) < 1) :
    (2^(a - b : ) * 2 * c : ) < (2^a : ) :=
begin
    rw @fpow_sub  _ _ two_ne_zero 1 b at h,

  have h0 : 0 < 2^a := sorry,
  have h1 : 2^a * (2 ^ 1 / 2 ^ b * c) < 2^a * 1 := by exact mul_lt_mul_of_pos_left h h0,

  --other stuff

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:10):

I made a mistake omitting that line in my last example, I forgot I changed h my bad

view this post on Zulip Reid Barton (Apr 28 2020 at 21:10):

have h0 : 0 < 2^a := sorry <-- this is a statement about nat

view this post on Zulip Reid Barton (Apr 28 2020 at 21:11):

That is why you get this confusing

has type
  0 < 2 ^ a
but is expected to have type
  0 < ?m_1

error. Yes, the error message could be more helpful.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:11):

@Reid Barton Thanks for pointing that out, too. I'll change it to have h0 : 0 < (2 : ℚ)^a := sorry,

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:21):

@Reid Barton Could you elaborate on why backwards reasoning is better?

view this post on Zulip Reid Barton (Apr 28 2020 at 21:22):

Lean already knows the correct way to elaborate the goal

view this post on Zulip Reid Barton (Apr 28 2020 at 21:22):

If you apply a lemma which requires a side condition, then Lean will work out the correct side condition

view this post on Zulip Reid Barton (Apr 28 2020 at 21:23):

and it may print as the same 0 < 2^a but it will be at the correct type

view this post on Zulip Reid Barton (Apr 28 2020 at 21:23):

If you build up forwards, Lean has no way of knowing how your facts like h0 are supposed to relate to the goal so you must help the elaborator by being specific

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:24):

rw fpow_sub at h, works because Lean knows the type of h

view this post on Zulip Reid Barton (Apr 28 2020 at 21:26):

or say you skip have h0 : 0 < 2^a := sorry, and instead begin

  have h1 : 2^a * (2 ^ 1 / 2 ^ b * c) < 2^a * 1,
  { apply mul_lt_mul_of_pos_left h,
  }

view this post on Zulip Reid Barton (Apr 28 2020 at 21:27):

now the goal is the correct 0 < 2^a

view this post on Zulip Bryan Gin-ge Chen (Apr 28 2020 at 21:29):

Kevin Buzzard said:

rw fpow_sub at h, works because Lean knows the type of h

That adds an additional 2 ≠ 0 goal. We discussed this around here last night.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:29):

you can solve that goal whenever you feel like it with by norm_num

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:30):

rw fpow_sub at h; try {by norm_num},

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:31):

You are going to end up with a bunch of 2 \ne 0 goals, it might be even worth proving it beforehand.

view this post on Zulip Bryan Gin-ge Chen (Apr 28 2020 at 21:32):

Maybe the mathematician tactic mode should apply ; try {by norm_num} after every step.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:32):

  have h2 : (2 : )  0 := by norm_num,
  rw fpow_sub h2 at h,

I suspect you'll need h2 later on

view this post on Zulip Reid Barton (Apr 28 2020 at 21:33):

Does rw put the side conditions at the end or something?

view this post on Zulip Reid Barton (Apr 28 2020 at 21:33):

I seem to recall that

view this post on Zulip Reid Barton (Apr 28 2020 at 21:34):

That seems usually annoying

view this post on Zulip Reid Barton (Apr 28 2020 at 21:34):

maybe there's a good reason though

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:44):

Because nobody fixed it yet?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:45):

Actually maybe the idea is that if you knew how to prove it with a one-liner you would have written the proof in the rw line

view this post on Zulip Sam Raleigh (Apr 28 2020 at 21:52):

Is there a list of all the theorems somewhere?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:57):

The documentation?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:00):

https://leanprover-community.github.io/mathlib_docs/

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:00):

Better make yourself a nice cup of tea before you start

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:13):

Haha thanks!

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:16):

Is this list complete though? For example I can't find fpow_add in the algebra.field_power section. Is that because it isn't located here?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:26):

That's correct

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:27):

Import enough stuff to make #check fpow_add work, and then right click and go to definition to find where it's located

view this post on Zulip Bryan Gin-ge Chen (Apr 28 2020 at 22:28):

It recently moved to algebra.group_with_zero_power. (I guess that's why the google search doesn't pull it up).

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:30):

Another question - how come example (a b : ℕ) : (2 : ℚ)^(a - b : ℤ) = (2 : ℚ)^a * (2 : ℚ)^(-b : ℤ) := by exact fpow_add two_ne_zero a (-b) has no errors but the following code gives me a type mismatch error?

lemma core_ineq
  {a b c : }
  (h : ((2 : )^(1 - b : ) * c : ) < 1) :
  ((2 : )^(a - b : ) * 2 * c : ) < (2:)^(a : ) :=
begin
  rw fpow_add two_ne_zero a (-b),

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:31):

Why not use h2 from above instead of two_ne_zero -- does it make a difference? [edit: no]

view this post on Zulip Reid Barton (Apr 28 2020 at 22:31):

This is precisely what was discussed at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/195362228

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:33):

It's because exact is happy with definitional equality and rw needs syntactic equality I should think.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:34):

a + -b isn't syntactically equal to a - b

view this post on Zulip Reid Barton (Apr 28 2020 at 22:35):

That also doesn't help.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:36):

@Kevin Buzzard I'm just playing around with different possibilities to increase my understanding of type casting.
@Reid Barton Ah right, thank you. I guess I didn't understand Mario's answer as clearly as I thought I did

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:37):

Sam, a lot of your recent questions seem to indicate that you are doing implicit steps in your head. Lean will not let you skip anything. The error is clear. Lean is looking for 2 ^ (↑a + -↑b) and it can only see 2 ^ (↑a - ↑b). Just because you know these are the same doesn't mean that the rw tactic knows they are the same.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:40):

lemma core_ineq
  {a b c : }
  (h : ((2 : )^(1 - b : ) * c : ) < 1) :
  ((2 : )^(a - b : ) * 2 * c : ) < (2:)^(a : ) :=
begin
  change _ ^ (a + (-b) : ) * _ * _ < _,
  rw fpow_add _ a (-b),
end

Lean needs to be explicitly told to make the change because rw isn't going to do it.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:41):

But really this is cheeky, because the fact that a-b happens to be definitionally equal to a+(-b) shouldn't really be used.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:41):

begin
  rw sub_eq_add_neg,
  rw fpow_add _ a (-b),

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:41):

Got it. From henceforth I shall assume lean is as pedantic as my 7th grade english teacher. Is there some resource that lists the definitional equivalences in lean so that you can recognize when to avoid proving unnecessary steps?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:41):

You can just look up the definitions :-)

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:42):

Lean is at least as pedantic as your 7th grade english teacher.

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:42):

genius! why didn't I think of that

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:42):

(not being sarcastic - I genuinely did not think to do that for some reason)

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:42):

The definition of a - b is actually hard to look up I should think

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:43):

but what is true by definition and what isn't shouldn't really be relevant. You're supposed to use the interface

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:43):

You can prove a - b = a + -b either by rfl or by sub_eq_add_neg and in some sense the latter is more appropriate

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:44):

(of course if you look up the proof of sub_eq_add_neg you'll probably see that it's rfl)

view this post on Zulip Sam Raleigh (Apr 28 2020 at 22:44):

So "good practice" is always proving equivalences yourself instead of relying on coincidental definitional equivalences

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:44):

In the natural number game, the proof of 0 + n = n is zero_add, which is proved by induction, but the proof of n + 0 = n is rfl because it's true by definition

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:44):

This to me is an indication that definitional equality is really a rather pathological thing

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:45):

You can only find this out by looking at the definition of +, and mathematical arguments should not depend on the definition of +, they should depend on the interface for +, which includes zero_add and add_zero

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:46):

just like you shouldn't care whether Lean's real numbers are defined via Cauchy sequences, Dedekind cuts, or something else

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:49):

set_option pp.notation false
example (a b : ) : a - b = 0 :=
begin
  unfold has_sub.sub,
  unfold algebra.sub,
  -- ⊢ eq (has_add.add a (has_neg.neg b)) 0
  -- now comment out the set_option line
  -- ⊢ a + -b = 0
end

view this post on Zulip Steffan (Apr 28 2020 at 23:29):

Where did this thing come from that you abbreviate refl rfl?

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:31):

rfl is a term, refl is a tactic

view this post on Zulip Steffan (Apr 28 2020 at 23:32):

Oh, didn't know that existed

view this post on Zulip Steffan (Apr 28 2020 at 23:33):

I don't see the purpose of it though.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:33):

which one? they are both useful

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:33):

I probably use rfl a lot more than the refl tactic

view this post on Zulip Steffan (Apr 28 2020 at 23:35):

I don't see the purpose of rfl. refl is much shorter than apply rfl.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:35):

not everything has to be written as a tactic you know

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:36):

you can write terms in all sorts of places, like inside tactics

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:36):

as well as just writing a term proof and skipping tactics altogether

view this post on Zulip Steffan (Apr 28 2020 at 23:37):

Nevermind, I see. e.g. rfl is easier to write than by refl.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:38):

You should search mathlib for rfl, it's surprisingly common, especially for proving lemmas "by definition"

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:39):

here's a fun one from the sensitivity conjecture:

lemma succ_n_eq (p q : Q (n+1)) : p = q  (p 0 = q 0  π p = π q) :=
begin
  split,
  { rintro rfl, exact rfl, rfl, },
  ...
end

view this post on Zulip Steffan (Apr 28 2020 at 23:40):

haha, that's a cool one :D

although I don't know what rintro is yet.

I actually didn't know that by apply term = term, that was my problem.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:41):

Actually by apply term is like term _ _ _ depending on how many arguments term has as a function

view this post on Zulip Mario Carneiro (Apr 28 2020 at 23:41):

by exact term is like term

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:45):

lemma core_ineq
  {a b c : }
  (h : ((2 : )^(1 - b : ) * c : ) < 1) :
  ((2 : )^(a - b : ) * 2 * c : ) < (2:)^(a : ) :=
begin
  rw @fpow_sub  _ _ two_ne_zero 1 b at h,
  rw pow_one (2 : ) at h,

How do I make rw recognize the instance of the target pattern (2:\Q)^1 in h? Is rw failing to do so because I've coerced 1 to \Z, but the 1 in pow_one is of type \nat?

view this post on Zulip Reid Barton (Apr 29 2020 at 01:47):

Please include imports

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:48):

the solution is rw fpow_one at h,

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:49):

also all those (2:\Q) are redundant

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:52):

The imports:

import data.nat.basic
import data.int.basic
import data.rat.basic

import algebra.field_power

import tactic

import data.finset
import algebra.big_operators
import data.real.basic
import data.set.lattice

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:52):

import tactic algebra.field_power data.rat.basic

lemma core_ineq {a b c : }
  (h : (2 ^ (1 - b : ) * c : ) < 1) :
  (2 ^ (a - b : ) * 2 * c : ) < 2 ^ (a : ) :=
begin
  convert mul_lt_mul_of_pos_left h (fpow_pos_of_pos two_pos a) using 1,
  { have : (2 : )  0 := dec_trivial,
    rw [fpow_sub this, fpow_sub this, fpow_one, div_eq_mul_inv, div_eq_mul_inv],
    simp only [mul_assoc, mul_comm, mul_left_comm] },
  { rw mul_one }
end

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:55):

Thanks kenny, but I wasn't asking for the full proof. I want to do it myself (as ugly as that might turn out to be).

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:55):

Still valuable as an answer key though!

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:57):

I am curious as to what this means though

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:58):

if you look at the tactic state you will see this : 2 \ne 0

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:58):

which is because I didn't specify a name for the lemma

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:59):

oh so it's just a default name

view this post on Zulip Sam Raleigh (Apr 29 2020 at 01:59):

got it, thanks!

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:01):

If my context looks like:

1 goal
a b c : ,
h : 2 / 2 ^ b * c < 1
 2 ^ a  0

How would I go about closing the goal using nat.fpow_ne_zero_of_pos? The online documentation says that the parameters for nat.fpow_ne_zero_of_pos are (h : 0 < p) (n : ℤ), but this seems to be inconsistent with what lean expects:

fpow_ne_zero_of_pos : 0 < ?M_3 → ∀ (n : ℤ), ↑?M_3 ^ n ≠ 0

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:02):

I want a theorem for which I can specify the exponent, not receive statement prefaced by a universal quantifier.

view this post on Zulip Kenny Lau (Apr 29 2020 at 03:04):

(that's the same thing)

view this post on Zulip Reid Barton (Apr 29 2020 at 03:04):

How about starting with apply nat.fpow_ne_zero_of_pos?

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:09):

@Reid Barton I get

invalid apply tactic, failed to unify
  2 ^ a  0
with
  ↑?m_3 ^ ?m_4  0

view this post on Zulip Reid Barton (Apr 29 2020 at 03:12):

maybe fpow_ne_zero_of_ne_zero then? is a field a group_with_zero, whatever that is?

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:14):

What is fpow_ne_zero_of_ne_zero? It isnt showing up in the documentation

view this post on Zulip Reid Barton (Apr 29 2020 at 03:15):

It's in src/algebra/group_with_zero_power.lean

view this post on Zulip Reid Barton (Apr 29 2020 at 03:15):

maybe in some namespace

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:16):

I just #check'd it, I see

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:17):

Why doesn't it appear in the online documentation?

view this post on Zulip Reid Barton (Apr 29 2020 at 03:17):

No idea, is the online documentation older than April 7 maybe?

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 03:17):

No, it's there: https://leanprover-community.github.io/mathlib_docs/algebra/group_with_zero_power.html#fpow_ne_zero_of_ne_zero

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:18):

Ah I see, so it's just the google search engine for the docs that was acting up again

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:18):

Thanks bryan

view this post on Zulip Reid Barton (Apr 29 2020 at 03:18):

ok, I see a field is indeed a group_with_zero though maybe it would be better if the documentation didn't require me to know the term "division ring".

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:19):

Does virtual studio have functionality that would allow me to query my local mathlib documents instead of the online documentation for theorems that I need?

view this post on Zulip Reid Barton (Apr 29 2020 at 03:19):

I just use git grep

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:23):

IS dec_trivial a theorem or a tactic? A bit unclear on this

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:23):

What exactly does it do?

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:24):

more importantly, where is it located in the online documentation?

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 03:32):

dec_trivial is a term. I don't think it has a particularly useful docstring, but it's explained in (where else) TPiL.

view this post on Zulip Sam Raleigh (Apr 29 2020 at 03:34):

Thanks!

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 03:38):

(OK, technically, dec_trivial does call a tactic... but you use it like a term.)

view this post on Zulip Sam Raleigh (Apr 29 2020 at 12:45):

So I'm trying to define a set SS of all 2-colorings of a complete graph on nn vertices KnK_n which are monochromatic on a KkK_k subgraph of KnK_n. I've used some of the definitions of @Bhavik Mehta as an initial stepping stone. Here is Bhavik's definition of the set of all colorings of KnK_n:

import data.nat.basic data.finset tactic
open finset
open nat

local notation `edges_of `X := powerset_len 2 X

universe u
variables {α : Type u} (K : finset α) {n : }

def colorings : finset (finset (finset α)) := powerset (edges_of K)

I'd like to define something similar for SS:

def mono_sub_colorings (n : ) (k : ) : finset (finset (finset α)) := --something

I am having some difficulty formalizing this. At first I thought I could somehow define SS by starting with the powerset of edges of KnkK_{n-k}, and then taking the union of this set and some set of order (nk)k(n-k)*k (for the edges between the KkK_k subgraph and the rest of KnK_n). Then I would take the union of this union over all choice of the KkK_k subgraph. My questions are:

  1. Can you define a finset by the union of two other finsets?
  2. Is this construction ideal in lean or is there a more canonical / less contrived way of constructing SS? How would you go about doing it?

Thank you!

view this post on Zulip Sam Raleigh (Apr 29 2020 at 12:46):

  1. If the answer to question 1 is yes, then how?

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:18):

  1. Yes! You can use the union operator which should take the union of the two given finsets

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:19):

Contrived example:

example (s t : finset α) : finset α :=
begin
  let new_finset := s  t,
  exact new_finset
end

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:21):

As for 2, I did the same construction in a different way. I defined a predicate red_on H c which indicated when the colouring c was red on the particular subgraph H

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:22):

(More specifically, for the K_k given by the vertices of the subset H)

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:23):

I defined blue_on similarly, and then mono_on as the "or" of those two

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:23):

Then all the colourings which are monochromatic on H are given by filtering: (colourings G).filter (mono_on H)

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:25):

Next I defined def has_mono G (s : ℕ) c : Prop := ∃ (H' ∈ powerset_len s G), mono_on H' c, which says that G with the colouring c has a monochromatic K_s if there is a subset of the vertices of size s for which the colouring is monochromatic

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:25):

and filtering with this predicate gives your set S

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:25):

card ((colourings G).filter (has_mono G s))

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:26):

(I should apologise, the code I wrote is pretty hard to understand and might not compile with newer versions of mathlib since I PR'd some lemmas at the top - if it'd be useful to you I can tidy it up)

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:29):

Defining S in the way you suggest would be possible - I personally went straight for my way because filtering is a natural way of thinking about it to me - I don't see any immediate reason yours wouldn't work though. An important thing you should be aware of though is that taking a union over another set as you suggest here: "union over all choice of the K_k subgraph" is better expressed using the bind operator in data/finset

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:30):

And just in case you weren't aware yet, there's some lemmas for getting the cardinality of finsets in algebra/big_operator

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:32):

Let me know if you have any questions or want me to explain my proof some more! I should say that the proofs I gave weren't "good lean" so don't take them as good practice, but you can certainly take implementation ideas - I think these were reasonably well thought out

view this post on Zulip Bhavik Mehta (Apr 29 2020 at 14:47):

Another piece of advice which took me too long to learn when I started doing combinatorics in lean is that your definitions should be general, and your lemmas can restrict usage. For instance, when I defined def red_on (H : finset α) (c : finset (finset α)) : Prop := (edges_of H) ⊆ c, I didn't insist that H was a subset of G, nor that c was actually a colouring of G, but instead these conditions are on the lemmas, eg thing1 has the condition that H is a subset of G, and the filter ensures that c is a colouring of G. A simpler example is when we define division on naturals - the definition of division doesn't require the denominator to be non-zero, but (most of) the useful lemmas do. For combinatorics at least I've found this turns out to make things much much easier

view this post on Zulip Sam Raleigh (Apr 29 2020 at 15:22):

This is a fantastic answer, thank you so much for your help @Bhavik Mehta. I'll look into the bind and `big_operator. Don't worry about your cold not being readable. I just needed an example of how to even begin a proof about objects (graphs) that don't have a standard definition in lean yet, and your proof was extremely useful in this regard to a lean beginner like me.

view this post on Zulip Sam Raleigh (Apr 29 2020 at 15:29):

Also I had no idea filter was a thing. I'll have to look into this as well


Last updated: May 17 2021 at 22:15 UTC