Diagonal Ramsey Number Lower Bound

Stream: new members

[Sam Raleigh]

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)$ with Lean. For the following, note that $K_m$ refers to the complete graph on $m$ vertices and $E(G)$ is the edge set of graph $G$. The diagonal Ramsey number ${R}(k)$ is the smallest number $n$ such that for any 2-coloring of the edges of $K_n$, there is a monchromatic $K_k$ subgraph of $K_n$ (i.e. a $K_k$ subgraph where either all the edges are blue or all the edges are red). Ramsey proved in 1929 that $R(k)$ is finite for all $k$, 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) > n$ given the necessary inequality on $n$ and $k$ in Lean, I expect my goal for the proof would look like something along the lines of "there exists some $c : E(K_n) \rightarrow \{red, blue\}$ such that for every $H \subseteq K_n$ where $H \cong K_k$ there exists $e_1, e_2 \in E(H)$ such that $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 $K_n$ has no monochromatic $K_k$ subgraphs, then there is some coloring in the space of random colorings of $K_n$ which has no monochromatic $K_k$ subgraph. What tactic could I use to prove the goal with such an argument?

[David Wärn]

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

[David Wärn]

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

[Jalex Stark]

The details will depend on how you implement your probability distribution

[Jalex Stark]

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

[Sam Raleigh]

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 : (

[David Wärn]

@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

[David Wärn]

Lean does have probability theory though!

[Jalex Stark]

where? mathlib has a little bit of measure theory

[Sam Raleigh]

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

[David Wärn]

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

[David Wärn]

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

[Bryan Gin-ge Chen]

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

[Bhavik Mehta]

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

[Sam Raleigh]

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

[Kevin Buzzard]

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.

[Sam Raleigh]

I see, thank you

[Sam Raleigh]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Kevin Buzzard]

the more topics the better :-)

[Kevin Buzzard]

(as we just saw)

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Sam Raleigh]

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

[Mario Carneiro]

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:

[Mario Carneiro]

This is why I don't like transitive coercions

[Reid Barton]

So what real do you get?

[Reid Barton]

n?

[Reid Barton]

Mario Carneiro said:

cau_seq real int

This can't be what you meant, right?

[Mario Carneiro]

sorry, cau_seq real abs

[Mario Carneiro]

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

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

Or even without that second part.

[Reid Barton]

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?

[Johan Commelin]

What happens if you try?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

(hopefully I can offer instance feedback)

[Sam Raleigh]

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!

[Kenny Lau]

the type of \acannot be inferred

[Kenny Lau]

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)

[Sam Raleigh]

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

[Kenny Lau]

well the MWE would be mono_sub_colorings _ n k

[Kenny Lau]

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

[Kenny Lau]

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

[Sam Raleigh]

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

[Sam Raleigh]

Perhaps I don't understand the definition of an MWE

[Sam Raleigh]

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

[Sam Raleigh]

o wait

[Sam Raleigh]

I see what you mean

[Reid Barton]

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!

[Kenny Lau]

well this is just a misunderstanding.

[Sam Raleigh]

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?

[Kenny Lau]

right

[Sam Raleigh]

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

[Kenny Lau]

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

[Sam Raleigh]

Thanks!

[Bryan Gin-ge Chen]

Obligatory TPiL link. See also 6.5.

[Kevin Buzzard]

The former!

[Kenny Lau]

I stand corrected.

[Sam Raleigh]

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?

[Reid Barton]

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

[Reid Barton]

How would it know what type to pick?

[Sam Raleigh]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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

[Sam Raleigh]

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.

[Reid Barton]

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

[Reid Barton]

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

[Sam Raleigh]

I was wondering how to do this, thank you.

[Sam Raleigh]

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?

[Kevin Buzzard]

    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

[Kevin Buzzard]

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

[Kevin Buzzard]

(because of associativity conventions)

[Sam Raleigh]

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

[Kevin Buzzard]

Read more?

[Sam Raleigh]

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

[Kevin Buzzard]

Learning to read Lean error messages takes a long time

[Kevin Buzzard]

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

[Sam Raleigh]

That'll be the day...

[Kevin Buzzard]

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"

[Sam Raleigh]

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,

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

this is part of why backwards reasoning flows more smoothly

[Sam Raleigh]

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

[Reid Barton]

h0 is also wrong, though

[Sam Raleigh]

Sorry I should have posted the full thing

[Sam Raleigh]

Give me one moment

[Sam Raleigh]

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

[Sam Raleigh]

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

[Reid Barton]

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

[Reid Barton]

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.

[Sam Raleigh]

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

[Sam Raleigh]

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

[Reid Barton]

Lean already knows the correct way to elaborate the goal

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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,
  }

[Reid Barton]

now the goal is the correct 0 < 2^a

[Bryan Gin-ge Chen]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

rw fpow_sub at h; try {by norm_num},

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

I suspect you'll need h2 later on

[Reid Barton]

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

[Reid Barton]

I seem to recall that

[Reid Barton]

That seems usually annoying

[Reid Barton]

maybe there's a good reason though

[Kevin Buzzard]

Because nobody fixed it yet?

[Kevin Buzzard]

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

[Sam Raleigh]

Is there a list of all the theorems somewhere?

[Kevin Buzzard]

The documentation?

[Kevin Buzzard]

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

[Kevin Buzzard]

Better make yourself a nice cup of tea before you start

[Sam Raleigh]

Haha thanks!

[Sam Raleigh]

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?

[Kevin Buzzard]

That's correct

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Sam Raleigh]

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),

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

That also doesn't help.

[Sam Raleigh]

@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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sam Raleigh]

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?

[Kevin Buzzard]

You can just look up the definitions :-)

[Kevin Buzzard]

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

[Sam Raleigh]

genius! why didn't I think of that

[Sam Raleigh]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sam Raleigh]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Steffan]

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

[Mario Carneiro]

rfl is a term, refl is a tactic

[Steffan]

Oh, didn't know that existed

[Steffan]

I don't see the purpose of it though.

[Mario Carneiro]

which one? they are both useful

[Mario Carneiro]

I probably use rfl a lot more than the refl tactic

[Steffan]

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

[Mario Carneiro]

not everything has to be written as a tactic you know

[Mario Carneiro]

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

[Mario Carneiro]

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

[Steffan]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Steffan]

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.

[Mario Carneiro]

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

[Mario Carneiro]

by exact term is like term

[Sam Raleigh]

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?

[Reid Barton]

Please include imports

[Kenny Lau]

the solution is rw fpow_one at h,

[Kenny Lau]

also all those (2:\Q) are redundant

[Sam Raleigh]

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

[Kenny Lau]

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

[Sam Raleigh]

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).

[Sam Raleigh]

Still valuable as an answer key though!

[Sam Raleigh]

I am curious as to what this means though

[Kenny Lau]

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

[Kenny Lau]

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

[Sam Raleigh]

oh so it's just a default name

[Sam Raleigh]

got it, thanks!

[Sam Raleigh]

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

[Sam Raleigh]

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

[Kenny Lau]

(that's the same thing)

[Reid Barton]

How about starting with apply nat.fpow_ne_zero_of_pos?

[Sam Raleigh]

@Reid Barton I get

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

[Reid Barton]

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

[Sam Raleigh]

What is fpow_ne_zero_of_ne_zero? It isnt showing up in the documentation

[Reid Barton]

It's in src/algebra/group_with_zero_power.lean

[Reid Barton]

maybe in some namespace

[Sam Raleigh]

I just #check'd it, I see

[Sam Raleigh]

Why doesn't it appear in the online documentation?

[Reid Barton]

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

[Bryan Gin-ge Chen]

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

[Sam Raleigh]

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

[Sam Raleigh]

Thanks bryan

[Reid Barton]

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".

[Sam Raleigh]

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?

[Reid Barton]

I just use git grep

[Sam Raleigh]

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

[Sam Raleigh]

What exactly does it do?

[Sam Raleigh]

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

[Bryan Gin-ge Chen]

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

[Sam Raleigh]

Thanks!

[Bryan Gin-ge Chen]

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

[Sam Raleigh]

So I'm trying to define a set $S$ of all 2-colorings of a complete graph on $n$ vertices $K_n$ which are monochromatic on a $K_k$ subgraph of $K_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 $K_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 $S$:

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 $S$ by starting with the powerset of edges of $K_{n-k}$, and then taking the union of this set and some set of order $(n-k)*k$ (for the edges between the $K_k$ subgraph and the rest of $K_n$). Then I would take the union of this union over all choice of the $K_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 $S$? How would you go about doing it?

Thank you!

[Sam Raleigh]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

Contrived example:

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

and filtering with this predicate gives your set S

[Bhavik Mehta]

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

[Bhavik Mehta]

(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)

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Sam Raleigh]

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.

[Sam Raleigh]

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