well-ordering principle

Stream: maths

[Nicholas McConnell]

Does mathlib have a builtin well-ordering principle? If not, here is my attempt to create one: how should I start?

lemma WOP (f : ℕ → Prop) (h : ∃ k, f(k)) : ∃ n, (f(n) ∧ ∀ k, (f(k) → k ≥ n)) :=
begin
sorry
end

[Chris Hughes]

nat.find will compute this n for you.

[Nicholas McConnell]

Ah okay thanks

[Nicholas McConnell]

I'm not sure how to use it?

[Johan Commelin]

If you hit Ctrl-Shift-p in VScode, and then type #nat.find you'll find all the lemmas about it.

[Kevin Buzzard]

(and yes, mathlib has a bunch of stuff about general well-orderings as well, although in the case of nat there is more)

[Kevin Buzzard]

PS k ≥ n is the same as n ≤ k and as a general convention we stick to ≤ because e.g. then you don't have to state every lemma involving ≤ twice.

[Kevin Buzzard]

import tactic

def yadayadayada := 37

open_locale classical

lemma WOP (f : ℕ → Prop) (h : ∃ k, f(k)) : ∃ n, (f(n) ∧ ∀ k, (f(k) → k ≥ n)) :=
begin
  use nat.find h,
  split,
  { exact nat.find_spec h},
  { intro k,
    exact nat.find_min' h}
end

[Nicholas McConnell]

My point is that I'm confused about this:

type mismatch at application
  nat.find prime
term
  prime
has type
  ℕ → Prop : Type
but is expected to have type
  ∃ (n : ℕ), ?m_1 n : Prop

What on earth is the type named via an existential quantifier?

[Mario Carneiro]

You have to provide a proof that some prime exists, and it returns the least prime

[Nicholas McConnell]

Oh okay...

[Nicholas McConnell]

I tried this with a proof that some k exists with k % 4 = 2, but I doubt this is the way to find the smallest such k

lemma someK : ∃(k:ℕ), k % 4 = 2 :=
begin
use 10,
ring,
end

#check nat.find(someK)

[Alex J. Best]

Try #eval nat.find someK it will return 2 so looks like it does the right thing to me.

[Nicholas McConnell]

Ah thanks

[Nicholas McConnell]

In here, I feel like I'm supposed to change "0 < a * a" in the goal to "a * 0 < a * a" and then use mul_lt_mul_of_pos_left, but I'm not sure how to...

2 goals
a : ℤ,
h : a ≠ 0,
p : 0 < a
⊢ 0 < a * a

[Alex J. Best]

Using the library library_search tactic I found exact mul_pos' p p

[Scott Morrison]

haha, I was seconds behind:

example (n : ℤ) (a : 0 < n) : 0 < n * n := by library_search

[Alex J. Best]

the strategy you wanted you can achieve via

 rw [←( int.mul_zero a)],
 exact mul_lt_mul_of_pos_left p p,

[Nicholas McConnell]

Thanks

[Nicholas McConnell]

Another general question, is there any way to use a lemma statement?

For example, is there a command which can use lt_trichotomy to turn this

1 goal
a : ℤ,
h : a ≠ 0,
p : ¬0 < a
⊢ 0 < a ^ 2

into this?

1 goal
a : ℤ,
h : a ≠ 0,
p : ¬0 < a
q : 0 < a ∨ 0 = a ∨ a < 0
⊢ 0 < a ^ 2

[Mario Carneiro]

have q := lt_trichotomy 0 a will do that

[Nicholas McConnell]

Thanks. Sorry if I'm overwhelming you guys with questions, I am totally new to Lean

[Nicholas McConnell]

(deleted)

[Nicholas McConnell]

In proving this, I just need to be able to use p > 0 to get 0 ≠ ↑p (something I can apply s to). What's the best way you know to do this? [I feel like I could come up with one myself but it would be unnecessarily overwhelming]

1 goal
a p : ℕ,
hp : p > 0,
q : 0 ≤ ↑a * ↑a,
r : ↑p * ↑p ≤ ↑a * ↑a + ↑p * ↑p,
s : 0 ≠ ↑p → 0 < ↑p ^ 2
⊢ 0 < ↑a * ↑a + ↑p * ↑p

[Alex J. Best]

Not that it matters too much to the answer but : What is the cast ↑ to? Integers, reals? I.e. what is the actual lemma statement you are proving ?

[Mario Carneiro]

Seems like norm_cast will help a lot to clean that up

[Nicholas McConnell]

Alex J. Best said:

Not that it matters too much to the answer but : What is the cast ↑ to? Integers, reals? I.e. what is the actual lemma statement you are proving ?

Integers. I confess that I didn't know ↑ had multiple meanings

[Alex J. Best]

It means cast in general, so it could be casting nats to reals or rationals or whatever and it will just be printed in the same way. As mario says, whenever you have such a cast the tactic norm_cast can often reduce you back to the case where there are none.

[Alex J. Best]

Don't know if you wanted a full answer or not, but here is one way of concluding:

example (a p : ℕ) (hp : p > 0) (q : 0 ≤ (↑a :ℤ) * ↑a) (r : (↑p:ℤ) * ↑p ≤ ↑a * ↑a + ↑p * ↑p) (s : 0 ≠ (↑p:ℤ) → 0 < ↑p ^ 2) : 0 < ↑a * ↑a + ↑p * ↑p :=
begin
norm_cast at *,
specialize s (ne_of_lt hp),
rw [nat.pow_two] at s,
exact nat.lt_of_lt_of_le s r,
end

[Alex J. Best]

And the exact same proof still applies even if we started with reals or whatever as after norm_cast we end up in the same state.

[Nicholas McConnell]

Thank you greatly. I am learning Lean slowly but surely

[Patrick Massot]

have q := lt_trichotomy 0 a will do that

This works but doesn't teach Nicholas what he should have done. @Nicholas McConnell what you wanted here was to type:

have q : 0 < a ∨ 0 = a ∨ a < 0,
  library_search,

and look at the messages view.

[Kevin Buzzard]

I know from experience of watching students that this one is hard to find because you have to get the three terms in the right order and I think < vs > might also matter

[Patrick Massot]

Nicholas had the right statement!

[Patrick Massot]

But it's true that library_search would find the variations. That would be a job for Gabriel.

[Nicholas McConnell]

bandicam-2020-02-20-12-06-47-319.mp4

So I tried using nat.find. You say I'm supposed to pass in a proposition that a natural number satisfying a certain property exists, and then it'll return the smallest one. I thought in the general case, it would return a new variable and adjoin conditions "it satisfies it" and "nothing smaller satisfies it." But this is happening instead. What should I really do?

[Kevin Buzzard]

I can't watch the video on my phone because of download issues but iirc nat.find just produces a natural, and then lean also supplies the theorems saying that nat.find h satisfies all the things you want it to satisfy

[Kevin Buzzard]

But the theorems are a different part of the api

[Floris van Doorn]

You want to write open_locale classical near the top of your file (but not directly after the import statements). Then Lean will stop complaining about predicates being decidable.

[Floris van Doorn]

Also, you want to use let ds := nat.find d, not have. have is for proofs of propositions, and Lean will forget how you proved them. let is for data, and Lean will remember how you defined them.

[Floris van Doorn]

nat.find itself will only give you the natural number. You can then use nat.find_spec and nat.find_min (or nat.find_min') to know the properties about this natural number.

[Nicholas McConnell]

Now I'm wondering if there's a way to convert, e.g., ↑(a+b*c) to ↑a + ↑b * ↑c, using the casting from naturals to integers
Because I think I know how to carry on in this case. [I just tried "ring" on expressions involving integers and it worked.]

[Patrick Massot]

norm_cast

[Nicholas McConnell]

I've tried that, but all I've seen it do is eliminate unnecessary ↑'s, such as changing the goal from ↑(a+b) * ↑c = ↑d to (a+b) * c = d

[Nicholas McConnell]

I'm talking about expressions with subtraction, that you can't just do that do, but you can still distribute ↑ over + and *.

[Alex J. Best]

push_cast?

[Nicholas McConnell]

Alright, let me try that

[Nicholas McConnell]

Thanks Alex!

[Nicholas McConnell]

I guess I'll mostly be here asking what commands are called. XD There are (presumed hyperbole) zillions of commands, as someone else pointed out

[Patrick Massot]

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

[Kevin Buzzard]

https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_cast is where you want to look. norm_cast goes the other way to what you want -- push_cast goes the right way.

[Johan Commelin]

Should norm_cast be renamed to pull_cast? :grinning_face_with_smiling_eyes:

[Patrick Massot]

I'd be ready to bet that, if we could see the whole proof, we would end up using norm_cast.

[Kevin Buzzard]

It is true that people usually want norm_cast rather than push_cast. The fewer coercions the better!

[Kevin Buzzard]

For an expression with subtraction there is omega. For example example (n m : ℕ) : m + n - m = n := by omega works, but ring fails because of natural number subtraction. On the other hand omega doesn't work with multiplication of two non-constant terms.

[Mario Carneiro]

I think simp will also work to push down casts in most cases

[Mario Carneiro]

which I think is the real reason push_cast doesn't see much use

[Mario Carneiro]

that probably would have been my first step on Nicholas's goal

[Nicholas McConnell]

push_cast isn't changing the goal from "↑(d * q + r) - ↑d * ↑q = ↑r" to "(↑d * ↑q + ↑r) - ↑d * ↑q = ↑r"... how should I do this?

[Patrick Massot]

MWE?

[Kevin Buzzard]

post some code?

[Kevin Buzzard]

Do you actually want to make this change, or do you just want to prove the result?

[Kevin Buzzard]

import tactic

example (d q r : ℕ) : ((d * q + r : ℕ) : ℤ) - d * q = r :=
begin
  push_cast, ring,
end

[Nicholas McConnell]

Just want to prove the result

[Kevin Buzzard]

push_cast changed the goal to ⊢ ↑d * ↑q + ↑r - ↑d * ↑q = ↑r for me, so you'll need to give some more clues

[Nicholas McConnell]

If it helps, here's my topmost goal:

12 goals
a p : ℕ,
ha : ¬divides p a,
hp1 : 1 < p,
hp2 : ∀ (k : ℕ), divides k p → k = 1 ∨ k = p,
zero_lt_one : 0 < 1,
p_pos : 0 < p,
dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d,
d : ℕ := nat.find dh,
dm : ∀ (d' : ℕ), (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d',
dx1 : 0 < d,
h1 : 1 < d,
r q : ℕ,
hq1 : a = d * q + r,
hq2 : r < d,
x_ex y_ex : ℤ,
hy : x_ex * ↑a + y_ex * ↑p = ↑d,
thing : (0 < r ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑r) → d ≤ r,
htr1 : 0 < r
⊢ ↑(d * q + r) - ↑d * ↑q = ↑r

push_cast is doing absolutely nothing for me

[Kevin Buzzard]

This is no good, I can't tell what the uparrows mean.

[Nicholas McConnell]

Casting from natural number to integer

[Kevin Buzzard]

Can't you just post a working example of some code that I can just cut and paste so I can get into the same situation as you?

[Kevin Buzzard]

I can't diagnose it just from the tactic state.

[Kevin Buzzard]

PS I am impressed by the number of goals. There are tricks you can do with brackets which keeps this sort of thing under control.

[Nicholas McConnell]

You gotta forgive me for being new to Lean! (sniffs)

import tactic
universe u
local attribute [instance] classical.prop_decidable

lemma bezout (a p : ℕ) (hp : prime p) (ha : ¬(divides p a)) :
  ∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1 hp2,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := LCex a p p_pos,
let d := nat.find(dh),
have dx : 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := nat.find_spec dh,
have dm : ∀ d', (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d' := λ d', nat.find_min' dh,
cases dx with dx1 dx2,
have h := lt_trichotomy 1 d,
cases h with h1 h2,
have r1 := div_alg a d dx1,
cases r1 with r hr,
cases hr with q hq,
cases hq with hq1 hq2,
cases dx2 with x_ex hx,
cases hx with y_ex hy,
have thing := dm r,
have htr := lt_trichotomy 0 r,
cases htr with htr1 htr2,
have claim : (1-x_ex*q) * ↑a + (-y_ex*q) * ↑p = ↑r,
have claim2 : ↑a-↑d*↑q = ↑r,
rw hq1,
push_cast,

-- ...
end

[Kevin Buzzard]

Alternatively type set_option pp.all true before your code and just post the goal (if you can find it ;-) )

[Kevin Buzzard]

It doesn't run for me. Are you missing some imports or opens or something?

[Nicholas McConnell]

Added them

(Also I omitted LCex and div_alg so you may as well change them to "sorry")

[Kevin Buzzard]

It still doesn't run for me. Cut and paste what you're posting into a new file called scratch.lean or whatever and get it running.

[Kevin Buzzard]

The optimal way to get help here is to make other people's lives easier.

[Nicholas McConnell]

I did that and there's the same result

[Nicholas McConnell]

Should I... upload the file to my drive so you can see it or something?

[Scott Morrison]

Try minimising the file for a bit, and then copy and paste it here.

[Kevin Buzzard]

Which Lean are you using? Which mathlib? With the latest Lean and mathlib I get

unknown identifier 'prime'

unknown identifier 'divides'

[Nicholas McConnell]

Oh my bad, I mentioned div_alg but forgot I also defined my own "prime" and "divides"

[Floris van Doorn]

import tactic
example (d q r : ℕ) : ((d * q + r : ℕ) : ℤ) - (d : ℤ) * (q  : ℤ) = (r  : ℤ) :=
begin
  push_cast, simp,
end

[Kevin Buzzard]

OK so I say again: make a completely new file. Paste what you're pasting here into the new file. Make it work. Then post here.

[Kevin Buzzard]

Doesn't matter if it's super-long. But neither Floris nor I can see the problem yet.

[Nicholas McConnell]

Alright, that's what I'm about to do. (Just a few minutes ago I was very unwilling to)

[Nicholas McConnell]

import tactic
universe u
local attribute [instance] classical.prop_decidable

def ex1 (x y z : ℕ) : ℕ := x + y * z

def even (n : ℕ) : Prop := ∃ k, n = 2*k
def odd (n : ℕ) : Prop := ∃ k, n = 2*k+1

def divides (n m : ℕ) : Prop := ∃ k, n*k = m
def prime (p : ℕ) : Prop := 1 < p ∧ (∀ k, (divides k p → (k = 1 ∨ k = p)))

lemma square_eq_times_itself (a : ℤ) : a^2 = a*a :=
begin
rw pow_succ,
rw pow_succ,
rw pow_zero,
rw mul_one,
end

lemma nonzero_square_pos (a : ℤ) (h : 0 ≠ a) : 0 < a^2 :=
begin
sorry -- to make things easier to read
end

lemma square_nonneg (a : ℤ) : 0 <= a^2 :=
begin
sorry -- to make things easier to read
end

lemma LCex (a p : ℕ) (hp : 0 < p) :
  ∃(d:ℕ), 0 < d ∧ (∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = d))) :=
begin
sorry -- to make things easier to read
end

lemma div_alg (a b : ℕ) (hp : 0 < b) : ∃(r q : ℕ), (a = b*q+r ∧ r < b) :=
begin
sorry -- to make things easier to read
end

def isLC (a p d : ℕ) : Prop := 0 < d ∧ (∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = d)))

lemma bezout (a p : ℕ) (hp : prime p) (ha : ¬(divides p a)) :
  ∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1 hp2,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := LCex a p p_pos,
let d := nat.find(dh),
have dx : 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := nat.find_spec dh,
have dm : ∀ d', (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d' := λ d', nat.find_min' dh,
cases dx with dx1 dx2,
have h := lt_trichotomy 1 d,
cases h with h1 h2,
have r1 := div_alg a d dx1,
cases r1 with r hr,
cases hr with q hq,
cases hq with hq1 hq2,
cases dx2 with x_ex hx,
cases hx with y_ex hy,
have thing := dm r,
have htr := lt_trichotomy 0 r,
cases htr with htr1 htr2,
have claim : (1-x_ex*q) * ↑a + (-y_ex*q) * ↑p = ↑r,
have claim2 : ↑a-↑d*↑q = ↑r,
rw hq1,
push_cast,

-- ...
end

[Scott Morrison]

(And while Kevin says it doesn't matter if it's super-long, learning how to generate a _minimal_ example of the problem you're encountering is a great skill -- more often than not you solve the problem yourself while minimising.)

[Nicholas McConnell]

Oh yeah, I minimized it by replacing all the unimportant bodies to "sorry"

[Nicholas McConnell]

When I did that, the push_cast still had the same result for me

[Floris van Doorn]

Replace the line with claim2 to have claim2 : (a : ℤ)-↑d*↑q = ↑r,

[Floris van Doorn]

You didn't actually tell Lean what the target of the ↑'s were.

[Kevin Buzzard]

Yes, they are not integers after all.

[Kevin Buzzard]

They are just "some coercion from naturals to any old thing"

[Scott Morrison]

Generally, you don't ever want to type ↑ yourself: always use the (x : T) mechanism.

[Nicholas McConnell]

Ohh, I finally get it.

And you're finally glad I posted that MWE, huh.

[Kevin Buzzard]

In fact you can probably write claim2 : (a : ℤ) - d * q = r because Lean will figure out all the coercions itself once you explicitly tell it the first one.

[Kevin Buzzard]

Nicholas McConnell said:

And you're finally glad I posted that MWE, huh.

In the sense that I wasted some time trying to diagnose your problem when you were withholding information, but the moment you posted a MWE the answer was clear, yes.

[Nicholas McConnell]

Alright, my apologies for that.

[Kevin Buzzard]

I guess the other thing worth saying is that once you learn how to post MWEs and not just WEs, you start stripping away the irrelevant stuff and you then often end up solving your own problems. If you had done that here, you would see that the goal was created by claim2 and once everything else was stripped away you would have ended up with

import tactic

lemma MWE (a d q r : ℕ)
  (hq1 : a = d * q + r)
  : false -- irrelevant goal
  :=
begin
have claim2 : ↑a-↑d*↑q = ↑r,
rw hq1,
push_cast,
repeat {sorry}
end

You could have made that yourself. Now look at what happens after claim2 -- the number of goals goes from 1 to 9. So now you can see where the problem probably is.

[Kevin Buzzard]

Other notes: square_eq_times_itself is already in mathlib and is called pow_two. Of course it's very good practice for a beginner to prove these things themselves, but don't forget library_search. We have mul_self_pos and mul_self_nonneg as well, which will make some of those sorrys easy to remove. The rule of thumb is: if it's obvious, it's already there.

[Nicholas McConnell]

(deleted)

[Kevin Buzzard]

In tactic mode you can just do this:

variable (foo : ℤ → ℤ → Prop)

lemma test (hp : ∀(x y:ℤ),(foo x y → x+y=0)) : ∀(x y:ℤ),(foo x y → y+x=0) :=
begin
  intros x y h,
  rw add_comm,
  exact hp x y h
end

In term mode you can use the stupid triangle which I can never get to work.

lemma test' (hp : ∀(x y:ℤ),(foo x y → x+y=0)) : ∀(x y:ℤ),(foo x y → y+x=0) :=
λ x y h, add_comm ▸ hp x y h -- doesn't work

[Kevin Buzzard]

oh I got it:

lemma test' (hp : ∀(x y:ℤ),(foo x y → x+y=0)) : ∀(x y:ℤ),(foo x y → y+x=0) :=
λ x y h, add_comm x y ▸ hp x y h

[Kevin Buzzard]

I always forget it's not as smart as rw

[Nicholas McConnell]

Thanks, even though I figured it out

[Nicholas McConnell]

How do I change a hypothesis from 0 ≤ 2 * r to 0 ≤ 2 * ↑r (involving integers)? I don't see how to use norm_cast while specifying I want it to go to integers.

In other words, given

a b : ℕ,
b_pos : 0 < b,
ho : odd b,
r q : ℕ,
tri1 : 2 * r < b,
divq1 : a = b * q + r,
divq2 : r < b,
thing : 0 ≤ 2 * r

how can I get thing2 : 0 ≤ 2 * ↑r ?

[Nicholas McConnell]

[I trust that since this is not a problem-diagnosing question I don't need to put an MWE]

[Nicholas McConnell]

By the way, my ambition is to prove that (-2) * ↑r ≤ 0

[Bryan Gin-ge Chen]

import tactic

lemma foo (r : ℕ) (thing : 0 ≤ 2 * r) : true :=
begin
  have thing2 : (0 ≤ 2 * (r : ℤ)) :=
    by { norm_cast, exact thing },
  trivial
end

[MWEs are always preferable because it's easier to give a good suggestion when we can quickly check whether it works. Very few of us can emulate Lean + mathlib perfectly in our heads.]

[Nicholas McConnell]

Thanks. Also, I'll keep that in mind.