Zulip Chat Archive

Stream: maths

Topic: well-ordering principle


view this post on Zulip 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

view this post on Zulip Chris Hughes (Feb 18 2020 at 04:46):

nat.find will compute this n for you.

view this post on Zulip Nicholas McConnell (Feb 18 2020 at 04:47):

Ah okay thanks

view this post on Zulip Nicholas McConnell (Feb 18 2020 at 04:51):

I'm not sure how to use it?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 19 2020 at 04:21):

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

view this post on Zulip Nicholas McConnell (Feb 19 2020 at 04:21):

Oh okay...

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Feb 19 2020 at 04:25):

Ah thanks

view this post on Zulip 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

view this post on Zulip Alex J. Best (Feb 19 2020 at 05:00):

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

view this post on Zulip Scott Morrison (Feb 19 2020 at 05:01):

haha, I was seconds behind:

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

view this post on Zulip 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,

view this post on Zulip Nicholas McConnell (Feb 19 2020 at 23:45):

Thanks

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 20 2020 at 00:12):

have q := lt_trichotomy 0 a will do that

view this post on Zulip Nicholas McConnell (Feb 20 2020 at 02:54):

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

view this post on Zulip Nicholas McConnell (Feb 20 2020 at 03:25):

(deleted)

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Mario Carneiro (Feb 20 2020 at 04:36):

Seems like norm_cast will help a lot to clean that up

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Feb 20 2020 at 05:27):

Thank you greatly. I am learning Lean slowly but surely

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 20 2020 at 08:43):

Nicholas had the right statement!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 20 2020 at 17:12):

But the theorems are a different part of the api

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.]

view this post on Zulip Patrick Massot (Feb 24 2020 at 17:08):

norm_cast

view this post on Zulip 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

view this post on Zulip 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 *.

view this post on Zulip Alex J. Best (Feb 24 2020 at 17:12):

push_cast?

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 17:13):

Alright, let me try that

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 17:13):

Thanks Alex!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 24 2020 at 17:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 24 2020 at 17:27):

Should norm_cast be renamed to pull_cast? :grinning_face_with_smiling_eyes:

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 24 2020 at 19:01):

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

view this post on Zulip Mario Carneiro (Feb 24 2020 at 19:02):

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

view this post on Zulip Mario Carneiro (Feb 24 2020 at 19:02):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Feb 24 2020 at 21:28):

MWE?

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:28):

post some code?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:32):

Just want to prove the result

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:36):

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

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:36):

Casting from natural number to integer

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:37):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ;-) )

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:39):

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

view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:41):

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

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:42):

I did that and there's the same result

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:42):

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

view this post on Zulip Scott Morrison (Feb 24 2020 at 21:43):

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

view this post on Zulip 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'

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:47):

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

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:47):

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

view this post on Zulip Floris van Doorn (Feb 24 2020 at 21:48):

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

view this post on Zulip Floris van Doorn (Feb 24 2020 at 21:49):

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

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:49):

Yes, they are not integers after all.

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:49):

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

view this post on Zulip Scott Morrison (Feb 24 2020 at 21:49):

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

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:49):

Ohh, I finally get it.

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 21:54):

Alright, my apologies for that.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 22:43):

(deleted)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 22:48):

I always forget it's not as smart as rw

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 22:48):

Thanks, even though I figured it out

view this post on Zulip 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 ?

view this post on Zulip 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]

view this post on Zulip Nicholas McConnell (Feb 26 2020 at 05:06):

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

view this post on Zulip 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.]

view this post on Zulip Nicholas McConnell (Feb 26 2020 at 05:17):

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


Last updated: May 18 2021 at 06:15 UTC