## Stream: new members

### Topic: Diagonal Ramsey Number Lower Bound

#### 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)$ 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:

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

#### 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

#### Jalex Stark (Apr 25 2020 at 08:28):

The details will depend on how you implement your probability distribution

#### Jalex Stark (Apr 25 2020 at 08:28):

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

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

#### 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

#### David Wärn (Apr 25 2020 at 08:31):

Lean does have probability theory though!

#### Jalex Stark (Apr 25 2020 at 08:32):

where? mathlib has a little bit of measure theory

#### Sam Raleigh (Apr 25 2020 at 08:34):

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

#### 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

#### 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

#### 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

#### 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

#### 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"?

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

I see, thank you

#### 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

#### 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

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

#### Kevin Buzzard (Apr 28 2020 at 13:20):

the more topics the better :-)

(as we just saw)

#### 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

#### Patrick Massot (Apr 28 2020 at 13:23):

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

#### 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

#### 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


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

#### Mario Carneiro (Apr 28 2020 at 13:42):

This is why I don't like transitive coercions

#### Reid Barton (Apr 28 2020 at 13:45):

So what real do you get?

#### Reid Barton (Apr 28 2020 at 13:45):

n?

#### Reid Barton (Apr 28 2020 at 13:46):

Mario Carneiro said:

cau_seq real int

This can't be what you meant, right?

#### Mario Carneiro (Apr 28 2020 at 13:47):

sorry, cau_seq real abs

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


#### Reid Barton (Apr 28 2020 at 13:57):

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

#### Patrick Massot (Apr 28 2020 at 13:58):

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

#### 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

#### Reid Barton (Apr 28 2020 at 14:12):

Or even without that second part.

#### 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?

#### Johan Commelin (Apr 28 2020 at 14:32):

What happens if you try?

#### Reid Barton (Apr 28 2020 at 14:32):

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

#### Reid Barton (Apr 28 2020 at 14:33):

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

#### Reid Barton (Apr 28 2020 at 14:34):

(hopefully I can offer instance feedback)

#### 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!

#### Kenny Lau (Apr 28 2020 at 16:14):

the type of \acannot be inferred

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

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

#### Kenny Lau (Apr 28 2020 at 16:17):

well the MWE would be mono_sub_colorings _ n k

#### Kenny Lau (Apr 28 2020 at 16:18):

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

#### Kenny Lau (Apr 28 2020 at 16:18):

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

#### 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?

#### Sam Raleigh (Apr 28 2020 at 16:20):

Perhaps I don't understand the definition of an MWE

#### Sam Raleigh (Apr 28 2020 at 16:20):

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

o wait

#### Sam Raleigh (Apr 28 2020 at 16:21):

I see what you mean

#### 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!

#### Kenny Lau (Apr 28 2020 at 16:22):

well this is just a misunderstanding.

#### 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?

right

#### Sam Raleigh (Apr 28 2020 at 16:41):

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

#### 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

Thanks!

The former!

#### Kenny Lau (Apr 28 2020 at 16:51):

I stand corrected.

#### 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?

#### Reid Barton (Apr 28 2020 at 16:57):

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

#### Reid Barton (Apr 28 2020 at 16:57):

How would it know what type to pick?

#### Sam Raleigh (Apr 28 2020 at 16:58):

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

#### Reid Barton (Apr 28 2020 at 17:00):

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

#### 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}.

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

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

#### Reid Barton (Apr 28 2020 at 17:05):

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

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

#### Reid Barton (Apr 28 2020 at 17:10):

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

#### Reid Barton (Apr 28 2020 at 17:10):

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

#### Sam Raleigh (Apr 28 2020 at 17:12):

I was wondering how to do this, thank you.

#### 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?

#### 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


#### 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

#### Kevin Buzzard (Apr 28 2020 at 21:00):

(because of associativity conventions)

#### 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


#### 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

#### Kevin Buzzard (Apr 28 2020 at 21:03):

Learning to read Lean error messages takes a long time

#### 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

#### Sam Raleigh (Apr 28 2020 at 21:05):

That'll be the day...

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

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

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

#### 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

#### Reid Barton (Apr 28 2020 at 21:07):

this is part of why backwards reasoning flows more smoothly

#### Sam Raleigh (Apr 28 2020 at 21:08):

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

#### Reid Barton (Apr 28 2020 at 21:08):

h0 is also wrong, though

#### Sam Raleigh (Apr 28 2020 at 21:08):

Sorry I should have posted the full thing

#### Sam Raleigh (Apr 28 2020 at 21:09):

Give me one moment

#### 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


#### 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

#### Reid Barton (Apr 28 2020 at 21:10):

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

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

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

#### Sam Raleigh (Apr 28 2020 at 21:21):

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

#### Reid Barton (Apr 28 2020 at 21:22):

Lean already knows the correct way to elaborate the goal

#### 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

#### 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

#### 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

#### Kevin Buzzard (Apr 28 2020 at 21:24):

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

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


#### Reid Barton (Apr 28 2020 at 21:27):

now the goal is the correct 0 < 2^a

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

#### Kevin Buzzard (Apr 28 2020 at 21:29):

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

#### Kevin Buzzard (Apr 28 2020 at 21:30):

rw fpow_sub at h; try {by norm_num},

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

#### Bryan Gin-ge Chen (Apr 28 2020 at 21:32):

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

#### 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

#### Reid Barton (Apr 28 2020 at 21:33):

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

#### Reid Barton (Apr 28 2020 at 21:33):

I seem to recall that

#### Reid Barton (Apr 28 2020 at 21:34):

That seems usually annoying

#### Reid Barton (Apr 28 2020 at 21:34):

maybe there's a good reason though

#### Kevin Buzzard (Apr 28 2020 at 21:44):

Because nobody fixed it yet?

#### 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

#### Sam Raleigh (Apr 28 2020 at 21:52):

Is there a list of all the theorems somewhere?

#### Kevin Buzzard (Apr 28 2020 at 21:57):

The documentation?

#### Kevin Buzzard (Apr 28 2020 at 22:00):

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

#### Kevin Buzzard (Apr 28 2020 at 22:00):

Better make yourself a nice cup of tea before you start

Haha thanks!

#### 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?

That's correct

#### 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

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

#### 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


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

#### 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

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

#### Kevin Buzzard (Apr 28 2020 at 22:34):

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

#### Reid Barton (Apr 28 2020 at 22:35):

That also doesn't help.

#### 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

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

#### 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) : ℤ) * _ * _ < _,
end


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

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

#### Kevin Buzzard (Apr 28 2020 at 22:41):

begin


#### 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?

#### Kevin Buzzard (Apr 28 2020 at 22:41):

You can just look up the definitions :-)

#### Kevin Buzzard (Apr 28 2020 at 22:42):

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

#### Sam Raleigh (Apr 28 2020 at 22:42):

genius! why didn't I think of that

#### Sam Raleigh (Apr 28 2020 at 22:42):

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

#### Kevin Buzzard (Apr 28 2020 at 22:42):

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

#### 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

#### 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

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

#### Sam Raleigh (Apr 28 2020 at 22:44):

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

#### 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

#### Kevin Buzzard (Apr 28 2020 at 22:44):

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

#### 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

#### 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

#### 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,
-- now comment out the set_option line
-- ⊢ a + -b = 0
end


#### Steffan (Apr 28 2020 at 23:29):

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

#### Mario Carneiro (Apr 28 2020 at 23:31):

rfl is a term, refl is a tactic

#### Steffan (Apr 28 2020 at 23:32):

Oh, didn't know that existed

#### Steffan (Apr 28 2020 at 23:33):

I don't see the purpose of it though.

#### Mario Carneiro (Apr 28 2020 at 23:33):

which one? they are both useful

#### Mario Carneiro (Apr 28 2020 at 23:33):

I probably use rfl a lot more than the refl tactic

#### Steffan (Apr 28 2020 at 23:35):

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

#### Mario Carneiro (Apr 28 2020 at 23:35):

not everything has to be written as a tactic you know

#### Mario Carneiro (Apr 28 2020 at 23:36):

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

#### Mario Carneiro (Apr 28 2020 at 23:36):

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

#### Steffan (Apr 28 2020 at 23:37):

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

#### Mario Carneiro (Apr 28 2020 at 23:38):

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

#### 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


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

#### 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

#### Mario Carneiro (Apr 28 2020 at 23:41):

by exact term is like term

#### 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?

#### Kenny Lau (Apr 29 2020 at 01:48):

the solution is rw fpow_one at h,

#### Kenny Lau (Apr 29 2020 at 01:49):

also all those (2:\Q) are redundant

#### 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


#### 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


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

#### Sam Raleigh (Apr 29 2020 at 01:55):

Still valuable as an answer key though!

#### Sam Raleigh (Apr 29 2020 at 01:57):

I am curious as to what this means though

#### Kenny Lau (Apr 29 2020 at 01:58):

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

#### Kenny Lau (Apr 29 2020 at 01:58):

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

#### Sam Raleigh (Apr 29 2020 at 01:59):

oh so it's just a default name

got it, thanks!

#### 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

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

#### Kenny Lau (Apr 29 2020 at 03:04):

(that's the same thing)

#### Reid Barton (Apr 29 2020 at 03:04):

How about starting with apply nat.fpow_ne_zero_of_pos?

#### 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


#### 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?

#### Sam Raleigh (Apr 29 2020 at 03:14):

What is fpow_ne_zero_of_ne_zero? It isnt showing up in the documentation

#### Reid Barton (Apr 29 2020 at 03:15):

It's in src/algebra/group_with_zero_power.lean

#### Reid Barton (Apr 29 2020 at 03:15):

maybe in some namespace

#### Sam Raleigh (Apr 29 2020 at 03:16):

I just #check'd it, I see

#### Sam Raleigh (Apr 29 2020 at 03:17):

Why doesn't it appear in the online documentation?

#### Reid Barton (Apr 29 2020 at 03:17):

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

#### 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

Thanks bryan

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

#### 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?

#### Reid Barton (Apr 29 2020 at 03:19):

I just use git grep

#### Sam Raleigh (Apr 29 2020 at 03:23):

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

#### Sam Raleigh (Apr 29 2020 at 03:23):

What exactly does it do?

#### Sam Raleigh (Apr 29 2020 at 03:24):

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

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

Thanks!

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

#### Sam Raleigh (Apr 29 2020 at 12:45):

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 (Apr 29 2020 at 12:46):

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

#### 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

#### 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


#### 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

#### Bhavik Mehta (Apr 29 2020 at 14:22):

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

#### Bhavik Mehta (Apr 29 2020 at 14:23):

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

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

#### 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

#### Bhavik Mehta (Apr 29 2020 at 14:25):

and filtering with this predicate gives your set S

#### Bhavik Mehta (Apr 29 2020 at 14:25):

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

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

#### 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

#### 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

#### 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

#### 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

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

#### 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