Zulip Chat Archive

Stream: maths

Topic: well-ordering principle


Nicholas McConnell (Feb 18 2020 at 04:41):

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 (Feb 18 2020 at 04:46):

nat.find will compute this n for you.

Nicholas McConnell (Feb 18 2020 at 04:47):

Ah okay thanks

Nicholas McConnell (Feb 18 2020 at 04:51):

I'm not sure how to use it?

Johan Commelin (Feb 18 2020 at 06:51):

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

Kevin Buzzard (Feb 18 2020 at 08:20):

(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 (Feb 18 2020 at 08:43):

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 (Feb 18 2020 at 08:49):

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 (Feb 19 2020 at 04:19):

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 (Feb 19 2020 at 04:21):

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

Nicholas McConnell (Feb 19 2020 at 04:21):

Oh okay...

Nicholas McConnell (Feb 19 2020 at 04:24):

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 (Feb 19 2020 at 04:25):

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

Nicholas McConnell (Feb 19 2020 at 04:25):

Ah thanks

Nicholas McConnell (Feb 19 2020 at 04:46):

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 (Feb 19 2020 at 05:00):

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

Scott Morrison (Feb 19 2020 at 05:01):

haha, I was seconds behind:

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

Alex J. Best (Feb 19 2020 at 05:01):

the strategy you wanted you can achieve via

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

Nicholas McConnell (Feb 19 2020 at 23:45):

Thanks

Nicholas McConnell (Feb 20 2020 at 00:01):

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 (Feb 20 2020 at 00:12):

have q := lt_trichotomy 0 a will do that

Nicholas McConnell (Feb 20 2020 at 02:54):

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

Nicholas McConnell (Feb 20 2020 at 03:25):

(deleted)

Nicholas McConnell (Feb 20 2020 at 03:45):

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 (Feb 20 2020 at 04:34):

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 (Feb 20 2020 at 04:36):

Seems like norm_cast will help a lot to clean that up

Nicholas McConnell (Feb 20 2020 at 04:45):

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 (Feb 20 2020 at 04:47):

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 (Feb 20 2020 at 04:50):

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 (Feb 20 2020 at 04:52):

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 (Feb 20 2020 at 05:27):

Thank you greatly. I am learning Lean slowly but surely

Patrick Massot (Feb 20 2020 at 08:18):

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 (Feb 20 2020 at 08:25):

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 (Feb 20 2020 at 08:43):

Nicholas had the right statement!

Patrick Massot (Feb 20 2020 at 08:43):

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

Nicholas McConnell (Feb 20 2020 at 17:09):

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 (Feb 20 2020 at 17:12):

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 (Feb 20 2020 at 17:12):

But the theorems are a different part of the api

Floris van Doorn (Feb 20 2020 at 17:31):

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 (Feb 20 2020 at 17:32):

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 (Feb 20 2020 at 17:33):

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 (Feb 24 2020 at 17:07):

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 (Feb 24 2020 at 17:08):

norm_cast

Nicholas McConnell (Feb 24 2020 at 17:11):

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 (Feb 24 2020 at 17:12):

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 (Feb 24 2020 at 17:12):

push_cast?

Nicholas McConnell (Feb 24 2020 at 17:13):

Alright, let me try that

Nicholas McConnell (Feb 24 2020 at 17:13):

Thanks Alex!

Nicholas McConnell (Feb 24 2020 at 17:13):

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 (Feb 24 2020 at 17:19):

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

Kevin Buzzard (Feb 24 2020 at 17:23):

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 (Feb 24 2020 at 17:27):

Should norm_cast be renamed to pull_cast? :grinning_face_with_smiling_eyes:

Patrick Massot (Feb 24 2020 at 17:27):

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

Kevin Buzzard (Feb 24 2020 at 17:28):

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

Kevin Buzzard (Feb 24 2020 at 17:31):

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 (Feb 24 2020 at 19:01):

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

Mario Carneiro (Feb 24 2020 at 19:02):

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

Mario Carneiro (Feb 24 2020 at 19:02):

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

Nicholas McConnell (Feb 24 2020 at 21:27):

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 (Feb 24 2020 at 21:28):

MWE?

Kevin Buzzard (Feb 24 2020 at 21:28):

post some code?

Kevin Buzzard (Feb 24 2020 at 21:29):

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

Kevin Buzzard (Feb 24 2020 at 21:31):

import tactic

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

Nicholas McConnell (Feb 24 2020 at 21:32):

Just want to prove the result

Kevin Buzzard (Feb 24 2020 at 21:32):

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 (Feb 24 2020 at 21:34):

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 (Feb 24 2020 at 21:36):

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

Nicholas McConnell (Feb 24 2020 at 21:36):

Casting from natural number to integer

Kevin Buzzard (Feb 24 2020 at 21:37):

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 (Feb 24 2020 at 21:37):

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

Kevin Buzzard (Feb 24 2020 at 21:37):

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 (Feb 24 2020 at 21:38):

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 (Feb 24 2020 at 21:38):

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

Kevin Buzzard (Feb 24 2020 at 21:39):

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

Nicholas McConnell (Feb 24 2020 at 21:40):

Added them

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

Kevin Buzzard (Feb 24 2020 at 21:40):

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 (Feb 24 2020 at 21:41):

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

Nicholas McConnell (Feb 24 2020 at 21:42):

I did that and there's the same result

Nicholas McConnell (Feb 24 2020 at 21:42):

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

Scott Morrison (Feb 24 2020 at 21:43):

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

Kevin Buzzard (Feb 24 2020 at 21:43):

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

unknown identifier 'prime'

unknown identifier 'divides'

Nicholas McConnell (Feb 24 2020 at 21:44):

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

Floris van Doorn (Feb 24 2020 at 21:44):

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

Kevin Buzzard (Feb 24 2020 at 21:44):

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 (Feb 24 2020 at 21:45):

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

Nicholas McConnell (Feb 24 2020 at 21:45):

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

Nicholas McConnell (Feb 24 2020 at 21:46):

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 (Feb 24 2020 at 21:46):

(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 (Feb 24 2020 at 21:47):

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

Nicholas McConnell (Feb 24 2020 at 21:47):

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

Floris van Doorn (Feb 24 2020 at 21:48):

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

Floris van Doorn (Feb 24 2020 at 21:49):

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

Kevin Buzzard (Feb 24 2020 at 21:49):

Yes, they are not integers after all.

Kevin Buzzard (Feb 24 2020 at 21:49):

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

Scott Morrison (Feb 24 2020 at 21:49):

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

Nicholas McConnell (Feb 24 2020 at 21:49):

Ohh, I finally get it.

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

Kevin Buzzard (Feb 24 2020 at 21:50):

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 (Feb 24 2020 at 21:51):

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 (Feb 24 2020 at 21:54):

Alright, my apologies for that.

Kevin Buzzard (Feb 24 2020 at 22:08):

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 (Feb 24 2020 at 22:20):

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 (Feb 24 2020 at 22:43):

(deleted)

Kevin Buzzard (Feb 24 2020 at 22:48):

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 (Feb 24 2020 at 22:48):

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 (Feb 24 2020 at 22:48):

I always forget it's not as smart as rw

Nicholas McConnell (Feb 24 2020 at 22:48):

Thanks, even though I figured it out

Nicholas McConnell (Feb 26 2020 at 05:03):

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 (Feb 26 2020 at 05:03):

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

Nicholas McConnell (Feb 26 2020 at 05:06):

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

Bryan Gin-ge Chen (Feb 26 2020 at 05:14):

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 (Feb 26 2020 at 05:17):

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


Last updated: Dec 20 2023 at 11:08 UTC