Primes and modular arithmetic.

Stream: new members

[Wrenna Robson]

Hi. I'm working on a kata and I'm doing some actual number theory in Lean for the first time.

theorem solution
  {p q : ℕ}
  (hp : nat.prime p)
  (hq : nat.prime q)
  (p_lt_q : p < q)
  (p_ne_two : p ≠ 2)
  (q_ne_two : q ≠ 2)
  (consecutive : ∀ k, p < k → k < q → ¬ nat.prime k) :
∃ a b c, p + q = a * b * c
∧ a > 1 ∧ b > 1 ∧ c > 1 :=
begin
    sorry,
end

This is my MWE, although it's really just a sorry right now. I did one attempt but it got in such a tangle...

Here is my sketch proof:
p odd as non-two prime, q same. So p + q even, so there's a natural k such that 2*k = p + q. p < k < q, so by hypothesis k is not prime. So there's some a, 1 < a < k, such that a | k. Let b = (k/a). Use a, b, 2 as the a, b, c needed.

Now, I'd like to avoid too much unnecessary work here. To show that p and q are odd, it makes sense that I'd use nat.prime.eq_two_or_odd. But this has the "odd" condition as p % 2 = 1. This doesn't seem very useful - in particular, I can't see how you make it compatible with the MOD N definition, or the definition of oddness - so while there surely must be a way to get to where I want, it isn't clear to me.

To find k, I think I might want to use nat.exists_dvd_of_not_prime or nat.not_prime_iff_min_fac_lt - the former seems better. These are the only two "number theoretic" theorems I want - everything else seems like it ought to just be algebra. But I can't see how to run at it neat#ly.

[Jalex Stark]

Wrenna Robson said:

Now, I'd like to avoid too much unnecessary work here. To show that p and q are odd, it makes sense that I'd use nat.prime.eq_two_or_odd. But this has the "odd" condition as p % 2 = 1. This doesn't seem very useful - in particular, I can't see how you make it compatible with the MOD N definition, or the definition of oddness - so while there surely must be a way to get to where I want, it isn't clear to me.

It sounds like you're asking for a lemma relating oddness and % 2 = 1 relation. You could write this lemma out explicitly and then see if library_search finds it.

[Wrenna Robson]

Yes. I have had a good look before asking! But I haven't found one.

[Jalex Stark]

finding existing lemmas is hard, for sure

[Jalex Stark]

#naming

[Jalex Stark]

one surprisingly useful strategy is to literally guess the name of the lemma

[Wrenna Robson]

Yes I've got very far with that!

[Jalex Stark]

another strategy is using tactic#library_search

[Jalex Stark]

for the latter you have to actually write a statement of the lemma you want, for this you might find tactic#extract_goal useful

[Wrenna Robson]

How embarassing!

[Wrenna Robson]

Here it is: https://leanprover-community.github.io/mathlib_docs/data/nat/parity.html#nat.odd_iff

[Wrenna Robson]

lemma odd_iff_one_mod_2 {a : ℕ} : odd a ↔ a % 2 = 1 :=
begin
    library_search,
end

This worked :)

[Jalex Stark]

I don't think it's embarrassing at all!

[Wrenna Robson]

So using nat.prime.eq_two_or_odd I can get p = 2 \\/ p % 2 = 1.

[Jalex Stark]

I think I wrote the kata you're working on, and I think I found and forgot the name of this lemma literally three times during the process of writing it

[Ruben Van de Velde]

or.resolve_left?

[Wrenna Robson]

Thanks :)

[Wrenna Robson]

That was my next question.

[Wrenna Robson]

It's a really nice kata, Jalex! Because it is not very hard number theory but it's just hard enough to stretch me in Lean.

[Ruben Van de Velde]

(I went looking for that with library_search as well just now, so I guessed :))

[Kevin Buzzard]

Proving stuff like this is a kerfuffle. I can do the maths, and then I just muddle through the proofs. I think the only difference between you (Wrenna) and me is that I know a couple more tricks. I've always had a "grind it out" policy in maths (as you saw with my L<0 proof earlier). I think people with more dignity try to write cleaner code but all I want is "goals accomplished".

[Wrenna Robson]

I like beauty in my code, for my sins.

[Ruben Van de Velde]

Not sure if you knew this trick yet:

  have := hp.eq_two_or_odd.resolve_left p_ne_two,

(given hp : nat.prime p, nat.prime.foo hp can be abbreviated hp.foo)

[Wrenna Robson]

Why does it look like there are two functions with the same name here?

[Wrenna Robson]

https://leanprover-community.github.io/mathlib_docs/data/nat/parity.html#nat.even_add

[Wrenna Robson]

theorems, even, not functions

[Jalex Stark]

do you mean nat.even_add and nat.even.add?

[Wrenna Robson]

Oh I see. Ha, a punctuation mark off.

[Kevin Buzzard]

you were nat even wrong

[Wrenna Robson]

Alright, next question - this is more of a logic one.

begin
    have op : ¬ even p,
    {
        rw nat.not_even_iff,
        exact hp.eq_two_or_odd.resolve_left p_ne_two,
    },
    have oq : ¬ even q,
    {
        rw nat.not_even_iff,
        exact hq.eq_two_or_odd.resolve_left q_ne_two,
    },
    have epq : even (p + q),
    {
        rw nat.even_add,
        sorry,
    },
    sorry,
end

Here, I have even p ↔ even q as a goal, and ¬even p and ¬even q as hypotheses. So, uh, this is "just true", right? I tried simp (didn't work) - clearly I guess I could split the iff and so on but it seems like a lot...

[Kevin Buzzard]

I would envisage simp proving it by changing even p and even q to false, but it won't do that unless you explicitly tell it to use the hypotheses not even p and not even q

[Kevin Buzzard]

(simp doesn't use any of the hypotheses in your local context by default)

[Wrenna Robson]

So something like simp [op, oq]?

[Wrenna Robson]

Yes!

[Kevin Buzzard]

that's what I'd try

[Kevin Buzzard]

when I was a beginner I'd try simp on anything. Now I know a bit more about term rewriting I kind of get how to use it much better.

[Wrenna Robson]

Suppose I have something like p + q = 2*d and p < q, and I want to show p < d and d < q. It feels a bit like I want to do something like p = p /2 + p/2 < p/2 + q/2 = (p+q)/2 = d and so forth. However everything here is in the naturals (where I would prefer to stay I think?), even though I want to briefly soujourn into the rationals.

[Kevin Buzzard]

I agree that staying in the naturals is a PITA for this one. The moment you divide by 2 you have trouble. I would be tempted to use norm_cast.

[Wrenna Robson]

This really reminds me of some of the first stuff of yours I read, Kevin - the way mathematicians hop between the naturals, the reals, the integers, the rationals, without ever thinking of them as different objects, and how that sort of thing is uncovered by formalising like this.

[Wrenna Robson]

Ah, I haven't encountered norm_cast before.

[Kevin Buzzard]

Lemme see if I can knock something up. I would prove it for the rationals first.

[Ruben Van de Velde]

I used

  have : ¬nat.prime k,
  { apply consecutive; linarith },

[Wrenna Robson]

Ha! Yes, indeed, linarith just does it...

[Kevin Buzzard]

oh that's great! That's better than my suggestion. I had assumed linarith would only work over Q

[Kevin Buzzard]

This was what I was thinking; change the entire question to one about rationals and then use linarith.

example (p q d : ℕ) (h : p < q) (hd : p + q = 2 * d) : p < d ∧ d < q :=
begin
  suffices : (p : ℚ) < d ∧ (d : ℚ) < q,
    cases this, split; assumption_mod_cast,
  have hd' : (p : ℚ) + q = 2 * d,
    assumption_mod_cast,
  have h' : (p : ℚ) < q,
    assumption_mod_cast,
  split; linarith,
end

[Kevin Buzzard]

it didn't occur to me that split; linarith would do it over N

[Ruben Van de Velde]

I have no intuition about when linarith works on N, but sometimes it does

[Kevin Buzzard]

example (p q d : ℕ) (h : p < q) (hd : p + q = 2 * d) : p < d ∧ d < q :=
begin
  split; omega
end

This is the correct proof.

[Wrenna Robson]

...

[Kevin Buzzard]

omega is a tactic designed to work on naturals, it's complete for Presburger arithmetic, he said, only barely understanding what this means

[Kevin Buzzard]

I think it means "as long as you don't have two variables multiplied together, you're in good shape with omega"

[Wrenna Robson]

I have put it in. Next I need 2 ≤ d...

[Wrenna Robson]

Again this is obviously true as p < d by omega or linarith or whatever

[Wrenna Robson]

and p is not 2 and is prime. However...

[Kevin Buzzard]

you want p prime -> p >=2, that will be in the library. Then omega or linarith can take it from there.

[Wrenna Robson]

Aye.

[Wrenna Robson]

nat.prime.one_lt is the one I think.

[Kevin Buzzard]

But you need it in the local context, it's not good enough to just have it somewhere in mathlib

[Wrenna Robson]

Aye.

[Wrenna Robson]

I think it doesn't like the ≠...

[Kevin Buzzard]

rotten luck. Not even omega?

[Ruben Van de Velde]

Try two_le?

[Wrenna Robson]

?

[Wrenna Robson]

do you mean one_le_two?

[Ruben Van de Velde]

No, nat.prime.two_le rather than nat.prime.one_lt

[Kevin Buzzard]

omega works for me.

[Wrenna Robson]

hmm, maybe I'm using it wrong.

[Kevin Buzzard]

example (p : ℕ) (h : nat.prime p) (h2 : p ≠ 2) : 2 < p :=
begin
  have h := nat.prime.one_lt h,
  omega,
end

[Wrenna Robson]

Ah I was trying omega [nat.prime.two_le hp],

[Kevin Buzzard]

oh omega _does_ look at your local context

[Wrenna Robson]

bother said pooh

[Kevin Buzzard]

and I don't know if it takes arguments

[Kevin Buzzard]

yeah we make it random to keep beginners on their toes

[Wrenna Robson]

The have k := syntax I either hadn't seen or had forgotton.

[Kevin Buzzard]

there is some code I don't really understand that you can see when you hover over a tactic. It's something to do with parsers. If I hover over omega it says omega id*

[Wrenna Robson]

That's quite useful for "I want to instantiate a theorem in some particular way."

[Kevin Buzzard]

but if I hover over simp it says simp !? only? (* | [(* | (- id | (<- expr | expr))), ...]?) (with id*)? (at (* | (⊢ | id)*))? tactic.simp_config_ext?

[Kevin Buzzard]

which I think means "simp can take some extra arguments"

[Kevin Buzzard]

I genuinely don't know what you can put after omega, I only use it as a standalone tactic and I don't understand parsers well enough to know what id* means

[Wrenna Robson]

Alright, home stretch...

[Wrenna Robson]

begin
    have op : ¬ even p,
    {
        rw nat.not_even_iff,
        exact hp.eq_two_or_odd.resolve_left p_ne_two,
    },
    have oq : ¬ even q,
    {
        rw nat.not_even_iff,
        exact hq.eq_two_or_odd.resolve_left q_ne_two,
    },
    have epq : even (p + q),
    {
        rw nat.even_add,
        simp [op, oq],
    },
    rw even_iff_two_dvd at epq,
    cases (exists_eq_mul_right_of_dvd epq) with d hd,
    have compd : ¬ nat.prime d,
    {
        apply consecutive;
        omega,
    },
    have d2 : 2 ≤ d,
    {
        have k := nat.prime.two_le hp,
        omega,
    },
    cases (nat.exists_dvd_of_not_prime d2 compd) with n hn,
    use [2, n, d/n],
    sorry,
end

[Kevin Buzzard]

What's the local context at the sorry?

[Kevin Buzzard]

(either that or post a #mwe)

[Wrenna Robson]

pq: ℕ
hp: nat.prime p
hq: nat.prime q
p_lt_q: p < q
p_ne_two: p ≠ 2
q_ne_two: q ≠ 2
consecutive: ∀ (k : ℕ), p < k → k < q → ¬nat.prime k
op: ¬even p
oq: ¬even q
epq: 2 ∣ p + q
d: ℕ
hd: p + q = 2 * d
compd: ¬nat.prime d
d2: 2 ≤ d
n: ℕ
hn: n ∣ d ∧ n ≠ 1 ∧ n ≠ d
⊢ p + q = 2 * n * (d / n) ∧ 2 > 1 ∧ n > 1 ∧ d / n > 1

[Kevin Buzzard]

still loving the cut and paste from the infoview eats random spaces bug

[Kevin Buzzard]

a style point: you're not supposed to ever see > in Lean code or goals.

[Wrenna Robson]

So if from hn I can get 1 < n and n < d then technically I should be done...

[Kevin Buzzard]

a > b desugars to b < a but it still manages to fool some tactics, so we just decided to ban it

[Kevin Buzzard]

yeah this is looking good

[Wrenna Robson]

I am a bit suspicious that, mmm, I haven't necessarily shown that d/n is an integer - it just seemed to accept me using it.

[Kevin Buzzard]

it's natural division, so 3/2=1 and 1/0=37

[Wrenna Robson]

Like it is an integer becasuse n | d but I'm not used to Lean letting me be lazy.

[Wrenna Robson]

Ah lovely.

[Kevin Buzzard]

right -- it's divided and then rounded

[Wrenna Robson]

So possibly I don't want to use the division.

[Kevin Buzzard]

it should be OK, there will probably be a lemma saying that if n | d then (n / d) * d = n

[Wrenna Robson]

Really I want to use n | d to find some m so that n*m = d. There should be some lemma for that.

[Wrenna Robson]

Or that, yes.

[Kevin Buzzard]

in fact you can just do cases on n | d

[Kevin Buzzard]

n | d is by definition "exists m, d = n * m`

[Wrenna Robson]

Now, for some chunk series of ands, it's split, right?

[Wrenna Robson]

Repeated multiple times.

[Kevin Buzzard]

yes, split if they're in the goal and cases if they're hypotheses

[Kevin Buzzard]

the introduction and elimination tactics for and.

[Wrenna Robson]

Now, can I use rcases instead of cases, in order to get hn as three separate hypotheses originally?

[Wrenna Robson]

I'm not sure if I'll need to but...

[Wrenna Robson]

Hmm, it didn't work like I expected.

[Kevin Buzzard]

I like the way that you're kind of mathsy and computer-sciency at the same time. Are you that Royal Holloway PhD student or am I confusing you with someone else?

[Wrenna Robson]

That's me :)

[Kevin Buzzard]

mathsy beginners have more trouble with the CS stuff and CS beginners with the maths stuff

[Wrenna Robson]

And I have trouble with everything! ;P

[Kevin Buzzard]

You're doing great!

[Wrenna Robson]

Thanks!

[Kevin Buzzard]

example (P Q R : Prop) (h : P ∧ Q ∧ R) : false :=
begin
  rcases h with ⟨hP, hQ, hR⟩,
  sorry
end

[Wrenna Robson]

I can even claim that Lean is actual research work... though the paper I'm currently trying to figure out uses Isabelle for what it does (and I don't get Isabelle and it's much less user-friendly, alas).

[Kevin Buzzard]

I think the 24/7 helpline we have here is massively important

[Wrenna Robson]

Yes.

[Kevin Buzzard]

It was just over 3 years ago that I was spamming the chat asking questions and other people were helping me out.

[Wrenna Robson]

Circle of life!

[Kevin Buzzard]

I could do the maths no problem but I had no clue about the CS stuff.

[Wrenna Robson]

Hmm, the rcases format I wanted to use hasn't worked. Before I had cases (nat.exists_dvd_of_not_prime d2 compd) with n hn. Now I thought rcases (nat.exists_dvd_of_not_prime d2 compd) with n ⟨hn1, hn2, hn3⟩ might work... but it does not

[Kevin Buzzard]

Try rcases?

[Wrenna Robson]

No joy.

[Kevin Buzzard]

you probably want \<n, hn1, hn2, hn3\>

[Wrenna Robson]

Hmm! Yes. In my head the n was on a different level of hypothesis.

[Kevin Buzzard]

rcases? (nat.exists_dvd_of_not_prime d2 compd) should tell you what you want though

[Wrenna Robson]

It actually gave me something not very helpful!

[Kevin Buzzard]

rcases ('?' expr (: n)?) | ((h :)? expr (with patt)?) should answer all your questions

[Wrenna Robson]

oh well that clears that up

[Wrenna Robson]

how could i have been so blind

[Kevin Buzzard]

parsers are cool. I wish I understood them a bit better.

[Kevin Buzzard]

The moment you start learning how to write interactive tactics you need to know this stuff, but I have never written a line of meta code in my life

[Wrenna Robson]

the deep magic

[Wrenna Robson]

Now, I am going to want to extract 1<= n <= d from n|d and let omega do its work.

[Wrenna Robson]

Must be a lemma for that.

[Kevin Buzzard]

I'm guessing le_of_dvd or something

[Kevin Buzzard]

for n<=d

[Kevin Buzzard]

the naming convention is really cool

[Wrenna Robson]

What does "of" mean?

[Wrenna Robson]

Hmm, I have it but for ints. I hope that isn't an issue...

[Kevin Buzzard]

X_of_Y means Y -> X

[Kevin Buzzard]

is it really not there for nats?

[Wrenna Robson]

Oh it is, the search just didn't give it the first time.

[Kevin Buzzard]

oh yeah, sometimes I hit esc and then ctrl-space and get more options

[Kevin Buzzard]

I've never understood what's going on with that

[Kevin Buzzard]

X_of_Y_of_Z means Y -> Z -> X

[Kevin Buzzard]

e.g. lt_of_le_of_lt, something we used a lot before linarith was discovered

[Kevin Buzzard]

#naming

[Ruben Van de Velde]

I got there in the end, but the 1 < a and 1 < k/a were somewhat tedious - I hope there's a better solution

theorem solution
  {p q : ℕ}
  (hp : nat.prime p)
  (hq : nat.prime q)
  (p_lt_q : p < q)
  (p_ne_two : p ≠ 2)
  (q_ne_two : q ≠ 2)
  (consecutive : ∀ k, p < k → k < q → ¬ nat.prime k) :
∃ a b c, p + q = a * b * c
∧ a > 1 ∧ b > 1 ∧ c > 1 :=
begin
  have hp1 := hp.eq_two_or_odd.resolve_left p_ne_two,
  have hq1 := hq.eq_two_or_odd.resolve_left q_ne_two,
  rw ←nat.odd_iff at hp1 hq1,
  obtain ⟨k, hk⟩ : even (p + q),
  { simp at hp1 hq1,
    simp [hp1, hq1] with parity_simps },
  have : ¬nat.prime k,
  { apply consecutive; linarith },
  obtain ⟨a, hadvd, hane1, hanek⟩ := nat.exists_dvd_of_not_prime (by linarith [hp.two_le, hq.two_le]) this,
  use [a, k / a, 2],
  have hapos : 0 < a,
  { rw [nat.pos_iff_ne_zero],
    rintro rfl,
    rw [zero_dvd_iff] at hadvd,
    exact hanek hadvd.symm },
  refine ⟨_, _, _, _⟩,
  { rw [hk, nat.mul_div_cancel' hadvd, mul_comm] },
  { apply lt_of_le_of_ne _ hane1.symm,
    rwa [nat.succ_le_iff] },
  { obtain ⟨b, rfl⟩ := hadvd,
    have : b ≠ 0,
    { rintro rfl,
      linarith [hp.two_le, hq.two_le, hk] },
    rw mul_comm,
    rw nat.mul_div_cancel _ hapos,
    apply lt_of_le_of_ne,
    { rwa [nat.succ_le_iff, nat.pos_iff_ne_zero] },
    { contrapose! hanek, rw [←hanek, mul_one] } },
  { dec_trivial }
end

[Wrenna Robson]

Hmm my lean server crashed...

[Kevin Buzzard]

Where's the 1 < a proof?

[Kevin Buzzard]

it's difficult to follow the spoiler solution because no indents. Style point: the question should say 1 < a \and ..., not a > 1.

[Wrenna Robson]

I'm done!

[Wrenna Robson]

theorem solution
  {p q : ℕ}
  (hp : nat.prime p)
  (hq : nat.prime q)
  (p_lt_q : p < q)
  (p_ne_two : p ≠ 2)
  (q_ne_two : q ≠ 2)
  (consecutive : ∀ k, p < k → k < q → ¬ nat.prime k) :
∃ a b c, p + q = a * b * c
∧ a > 1 ∧ b > 1 ∧ c > 1 :=
begin
    have op : ¬ even p,
    {
        rw nat.not_even_iff,
        exact hp.eq_two_or_odd.resolve_left p_ne_two,
    },
    have oq : ¬ even q,
    {
        rw nat.not_even_iff,
        exact hq.eq_two_or_odd.resolve_left q_ne_two,
    },
    have epq : even (p + q),
    {
        rw nat.even_add,
        simp [op, oq],
    },
    rw even_iff_two_dvd at epq,
    cases (exists_eq_mul_right_of_dvd epq) with d hd,
    have compd : ¬ nat.prime d,
    {
        apply consecutive;
        omega,
    },
    have d2 : 2 ≤ d,
    {
        have k := nat.prime.two_le hp,
        omega,
    },
    have d0 : d > 0,
    {
        omega,
    },
    rcases (nat.exists_dvd_of_not_prime d2 compd) with ⟨n, hn1, hn2, hn3⟩,
    have npos := nat.pos_of_dvd_of_pos hn1 d0,
    have nltd := nat.le_of_dvd d0 hn1,
    use [2, n, d/n],
    split,
    {
        rw mul_assoc,
        rw nat.mul_div_cancel';
        assumption,
    },
    split,
    {
        omega,
    },
    split,
    {
        omega,
    },
    {
        apply (mul_lt_mul_left npos).mp,
        rw nat.mul_div_cancel',
        omega,
        assumption,
    },
end

[Kevin Buzzard]

ctrl-shift-p and type "Lean : restart" to restart lean after a crash

[Kevin Buzzard]

(in VS Code, if you're using emacs you're on your own)

[Wrenna Robson]

Would very much appreciate feedback on how making this less sprawling, although happily I do have indents.

[Mario Carneiro]

Kevin Buzzard said:

I genuinely don't know what you can put after omega, I only use it as a standalone tactic and I don't understand parsers well enough to know what id* means

It means it takes 0 or more identifiers. For example, omega h1 h2

[Wrenna Robson]

I'm using VS Code, because emacs scares me.

[Mario Carneiro]

I don't know from that what the identifiers mean, though

[Kevin Buzzard]

but I couldn't get omega (f h) to work -- should I have been able to?

[Mario Carneiro]

no

[Mario Carneiro]

id means an identifier or name, not an expression

[Kevin Buzzard]

oh, f h is not an identifier?

[Kevin Buzzard]

but f and h are?

[Mario Carneiro]

f h is two identifiers, (f h) is an expression

[Mario Carneiro]

f h is also an expression

[Ruben Van de Velde]

Hmm, can't nest code in the spoiler tag, but since you're done as well, I just opened it up

[Kevin Buzzard]

that was what was confusing me.

[Mario Carneiro]

an identifier is a sequence of letters and underscores

[Mario Carneiro]

and dots

[Kevin Buzzard]

Can you quote code in the spoiler tag? I think spoilers are new to Zulip

[Mario Carneiro]

pretty sure

[Kevin Buzzard]

I think my code would look pretty much the same as Ruben's or Wrenna's, except Wrenna I'd indent 2 spaces not 4.

[Wrenna Robson]

Yes that is that I haven't changed the setting in VS code.

[Mario Carneiro]

Kevin Buzzard said:

rcases ('?' expr (: n)?) | ((h :)? expr (with patt)?) should answer all your questions

This says that rcases takes either a ? followed by an expression, followed by optionally a colon and a number, i.e. rcases? (f x) or rcases? f x : 5, or an optional variable and a colon, followed by an expression, optionally followed by with and a pattern, like rcases h : e with <> or rcases e with <a, b, c>

[Kevin Buzzard]

these things are fiddly. Did you say it was a kata? You should both post your solutions and see if any of the CS whizzes had a go at it.

[Wrenna Robson]

Presumably there is some way to tell it to do two spaces for Lean files.

[Wrenna Robson]

Yeah it was. I'm just doing some basic tidying up.

[Mario Carneiro]

the syntax of patterns is not specified there because it is recursive and the notation kind of breaks down

[Kevin Buzzard]

That was going to be my next question :-)

[Wrenna Robson]

For a pattern like this:

    have op : ¬ even p,
    {
        rw nat.not_even_iff,
        exact hp.eq_two_or_odd.resolve_left p_ne_two,
    },

Is there a one-liner way of doing it? "have some goal, by re-writing the goal and then having it exactly"

[Kevin Buzzard]

instead of rw h you might well be able to just use the function h.1 directly.

[Mario Carneiro]

you can find it in the docs for docs#tactic.rcases_patt_parse though, in pseudo BNF style

patt ::= patt_med (":" expr)?
patt_med ::= (patt_hi "|")* patt_hi
patt_hi ::= id | "rfl" | "_" | "⟨" (patt ",")* patt "⟩" | "(" patt ")"

[Kevin Buzzard]

have op : ¬ even p := nat.not_even_iff.1 (hp.eq_two_or_odd.resolve_left p_ne_two), or something like that should work

[Wrenna Robson]

Sadly not.

[Wrenna Robson]

type mismatch at application
  nat.not_even_iff.mp (hp.eq_two_or_odd.resolve_left p_ne_two)
term
  hp.eq_two_or_odd.resolve_left p_ne_two
has type
  p % 2 = 1
but is expected to have type
  ¬even ?m_1

[Ruben Van de Velde]

mpr?

[Ruben Van de Velde]

Looks like I should've tried throwing omega at more subgoals

[Kevin Buzzard]

then it would be rw \l

[Kevin Buzzard]

no you're right

[Wrenna Robson]

mpr?

[Kevin Buzzard]

try .2

[Kevin Buzzard]

or .mpr. If h : a <-> b then internally h is a pair of proofs, h.1 : a -> b and h.2 : b -> a

[Wrenna Robson]

Right.

[Wrenna Robson]

.mpr is a mnemonic of some kind?

[Kevin Buzzard]

and h.mp is the same as h.1 and h.mpr is the same as h.2. I think Ruben's suggestion should work.

[Mario Carneiro]

have op : ¬ even p := nat.not_even_iff.2 (hp.eq_two_or_odd.resolve_left p_ne_two),

[Ruben Van de Velde]

Modus ponens reverse

[Kevin Buzzard]

"modus ponens reversed" or something?

[Wrenna Robson]

Right.

[Kevin Buzzard]

omega is great for nat goals because some stuff is so fiddly with nat. There are so many stupid things like a + b - a = b which are more painful than you think because of natural subtraction.

[Kevin Buzzard]

After a while the naming convention can't handle it all so you have to rely more on memory or search skillz

[Kevin Buzzard]

is that add_sub_self or what?

[Kevin Lacker]

naming is going to become even harder as we get more and more lemmas. i think we are going to need a better library_search & i hope lean 4 enables that

[Wrenna Robson]

Can we do a similar one-liner trick for

    have compd : ¬ nat.prime d,
    {
        apply consecutive;
        omega,
    },

[Wrenna Robson]

:= consecutive (by omega)?

[Wrenna Robson]

No.

[Kevin Buzzard]

something like that could well work

[Kevin Buzzard]

you should be able to get it to work somehow

[Ruben Van de Velde]

It needs two (by omega)s

[Kevin Buzzard]

got it

[Kevin Buzzard]

hence the semicolon

[Wrenna Robson]

So with have compd : ¬ nat.prime d := consecutive (by omega) (by omega), I get Cannot reify expr : ℕ

[Wrenna Robson]

Which is a bit mysterious.

[Kevin Buzzard]

what is the type of consecutive? apply is quite clever.

[Kevin Buzzard]

you might need to add some _s in

[Wrenna Robson]

∀ (k : ℕ), p < k → k < q → ¬nat.prime k

[Kevin Buzzard]

so try consecutive _ (by omega) (by omega)

[Wrenna Robson]

Yep

[Kevin Buzzard]

apply figured out the natural input by itself.

[Wrenna Robson]

Magic.

[Wrenna Robson]

begin
    have op : ¬ even p := nat.not_even_iff.mpr (hp.eq_two_or_odd.resolve_left p_ne_two),
    have oq : ¬ even q := nat.not_even_iff.mpr (hq.eq_two_or_odd.resolve_left q_ne_two),
    have epq : even (p + q) := nat.even_add.mpr (by simp [op, oq]),
    cases (exists_eq_mul_right_of_dvd (even_iff_two_dvd.mpr epq)) with d hd,
    have compd : ¬ nat.prime d := consecutive _ (by omega) (by omega),
    have d2 : 2 ≤ d, by linarith [nat.prime.two_le hp],
    have d0 : d > 0, by omega,
    rcases (nat.exists_dvd_of_not_prime d2 compd) with ⟨n, hn1, hn2, hn3⟩,
    have npos := nat.pos_of_dvd_of_pos hn1 d0,
    have nltd := nat.le_of_dvd d0 hn1,
    use [2, n, d/n],
    split,
    {
        rw mul_assoc,
        rw nat.mul_div_cancel';
        assumption,
    },
    split, omega,
    split, omega,
    {
        apply (mul_lt_mul_left npos).mp,
        rw nat.mul_div_cancel',
        omega,
        assumption,
    },
end

[Wrenna Robson]

This is looking very respectable.

[Wrenna Robson]

Oh bother. It looks like the version of Lean on Codewars doesn't like it.

[Wrenna Robson]

Something to do with the even.

[Wrenna Robson]

Here's my full #mwe.

import tactic
import data.nat.basic
import data.nat.prime
import data.nat.modeq

import data.int.basic
import data.int.parity

universe u
open_locale classical

theorem solution
  {p q : ℕ}
  (hp : nat.prime p)
  (hq : nat.prime q)
  (p_lt_q : p < q)
  (p_ne_two : p ≠ 2)
  (q_ne_two : q ≠ 2)
  (consecutive : ∀ k, p < k → k < q → ¬ nat.prime k) :
∃ a b c, p + q = a * b * c
∧ a > 1 ∧ b > 1 ∧ c > 1 :=
begin
    have op : ¬ even p := nat.not_even_iff.mpr (hp.eq_two_or_odd.resolve_left p_ne_two),
    have oq : ¬ even q := nat.not_even_iff.mpr (hq.eq_two_or_odd.resolve_left q_ne_two),
    have epq : even (p + q) := nat.even_add.mpr (by simp [op, oq]),
    cases (exists_eq_mul_right_of_dvd (even_iff_two_dvd.mpr epq)) with d hd,
    have compd : ¬ nat.prime d := consecutive _ (by omega) (by omega),
    have d2 : 2 ≤ d, by linarith [nat.prime.two_le hp],
    have d0 : d > 0, by omega,
    rcases (nat.exists_dvd_of_not_prime d2 compd) with ⟨n, hn1, hn2, hn3⟩,
    have npos := nat.pos_of_dvd_of_pos hn1 d0,
    have nltd := nat.le_of_dvd d0 hn1,
    use [2, n, d/n],
    split,
    {
        rw mul_assoc,
        rw nat.mul_div_cancel';
        assumption,
    },
    split, omega,
    split, omega,
    {
        apply (mul_lt_mul_left npos).mp,
        rw nat.mul_div_cancel',
        omega,
        assumption,
    },
end

[Kevin Buzzard]

When i do codewars I use a custom repo with precisely the version of lean and mathlib supported by codewars at that time

[Ruben Van de Velde]

Try nat.even

[Ruben Van de Velde]

There was some refactoring there recently

[Wrenna Robson]

"unknown identifier 'nat.even'" on my local copy.

[Kevin Buzzard]

If you're using a version of lean/mathlib which is not the same as the codewars one then you can't expect to get a piece of code which compiles both locally and on codewars.

[Wrenna Robson]

Yes.

[Kevin Buzzard]

Lean is not backwards compatible

[Wrenna Robson]

Aye. Some progress on CodeWars using that, but even_iff_two_dvd (or nat.even_iff_two_dvd) is unrecognised - I don't know if the name of it changed.

[Mario Carneiro]

Here's my version of the compression pass:

theorem solution
  {p q : ℕ}
  (hp : nat.prime p)
  (hq : nat.prime q)
  (p_lt_q : p < q)
  (p_ne_two : p ≠ 2)
  (q_ne_two : q ≠ 2)
  (consecutive : ∀ k, p < k → k < q → ¬ nat.prime k) :
∃ a b c, p + q = a * b * c
∧ a > 1 ∧ b > 1 ∧ c > 1 :=
begin
  have op : ¬ even p := nat.not_even_iff.2 (hp.eq_two_or_odd.resolve_left p_ne_two),
  have oq : ¬ even q := nat.not_even_iff.2 (hq.eq_two_or_odd.resolve_left q_ne_two),
  have epq : even (p + q) := nat.even_add.2 (by simpa [op]),
  rw even_iff_two_dvd at epq,
  cases exists_eq_mul_right_of_dvd epq with d hd,
  have compd : ¬ nat.prime d := consecutive d (by linarith) (by linarith),
  have d2 : 2 ≤ d := by linarith [hp.two_le],
  have d0 : d > 0 := by linarith [d2],
  rcases nat.exists_dvd_of_not_prime d2 compd with ⟨n, hn1, hn2, hn3⟩,
  have npos := nat.pos_of_dvd_of_pos hn1 d0,
  have nltd := nat.le_of_dvd d0 hn1,
  refine ⟨2, n, d/n, _, _, _, _⟩,
  { rwa [mul_assoc, nat.mul_div_cancel' hn1] },
  { norm_num },
  { exact lt_of_le_of_ne npos hn2.symm },
  { apply (mul_lt_mul_left npos).mp,
    rw nat.mul_div_cancel' hn1,
    simp [lt_of_le_of_ne nltd hn3] },
end

[Kevin Buzzard]

honestly the way to fix this is to make a project with the same version of lean and mathlib as codewars. They say explicitly what version they're running. It's impossible to second-guess what has changed in the interim.

[Wrenna Robson]

Right.

[Mario Carneiro]

I also removed all the omega calls because omega is slow

[Ruben Van de Velde]

Try replacing (even_iff_two_dvd.mpr epq) by epq, I think it'll be fine definitionally

[Mario Carneiro]

and you don't need omega to prove 1 < 2

[Kevin Buzzard]

linarith

[Kevin Buzzard]

lt_add_one

[Ruben Van de Velde]

one_lt_two

[Kevin Buzzard]

lol does that work for 3 < 37?

[Kevin Buzzard]

dec_trivial

[Mario Carneiro]

:(

[Kevin Buzzard]

Maybe le_refl _ works?

[Mario Carneiro]

no one loves my baby

[Ruben Van de Velde]

Or nat.le.intro or something like that? suggest tends to come up with that

[Kevin Buzzard]

:-)

[Wrenna Robson]

Replacing epq worked with some prodding. Lesson learned about setting up a project right...

[Kevin Buzzard]

Mario wrote norm_num precisely to solve goals like this (3 < 37 etc)

[Kevin Buzzard]

linarith is good for inequalities with variables but when there's only numbers, norm_num works.

[Kevin Buzzard]

Your baby was what convinced me not to give up! Remember in 2017 when i couldn't do anything?

[Ruben Van de Velde]

Plenty of options in any case

[Kevin Buzzard]

Q1 on my first example sheet needed a proof that (1 : real) != 2 and there was no way of doing it :-)

[Wrenna Robson]

Not quite sure I understand simpa.

[Kevin Buzzard]

Mario can tell you what that does too.

[Kevin Buzzard]

It does something like: simplify all goals and assumptions, and then try closing the goal with assumption

[Mario Carneiro]

simpa using h = simp at h |-; exact h

[Kevin Buzzard]

so it works if an assumption and a goal simplify to the same thing

[Wrenna Robson]

Right!

[Wrenna Robson]

refine is nice.

[Wrenna Robson]

In { exact lt_of_le_of_ne npos hn2.symm }, npos is of type n > 0, and lt_of_le_of_ne is expecting 1 <= n in that spot. So 1 <= n is definitionally equal to n > 0?

[Wrenna Robson]

Wew! Alright. Thank you all - this has been a really great learning experience.

[Wrenna Robson]

Also how is it 00:14... I guess when the focus hole hits.

[Kevin Buzzard]

what better way to spend a Friday night in lockdown.

[Kevin Buzzard]

Well done to both of you!

[Wrenna Robson]

Ha, yes, of course, I certainly wouldn't spend a Friday night in normal times on my computer doing compuscimaths <_<

[Kevin Buzzard]

By the way I have a discord server which currently has 3 Imperial UGs and a Cambridge UG solving basic analysis questions in Lean, live streaming and chatting, right now.

[Wrenna Robson]

Ooh.

[Kevin Buzzard]

voice chat -- the one thing zulip doesn't offer

[Wrenna Robson]

Yes! I really like zulip o/w.

[Wrenna Robson]

We used it for our first year project vivas - topic per talk, could field questions during other talks.

[Wrenna Robson]

It works like my mind works - that is, multi-stranded.

[Wrenna Robson]

(...I would be super interested in listening in...)

[Kevin Buzzard]

I DM'ed you a link

[Kevin Buzzard]

anyone is welcome, but I don't advertise the links publically any more

[Wrenna Robson]

So you did! Thank you.