Zulip Chat Archive

Stream: new members

Topic: Splitting "and" inside a function.


view this post on Zulip Calle Sönne (Feb 22 2019 at 13:53):

I have following code:

theorem ratio_test (a :   ) (L : ) (h : M1P1.is_limit (λ n, abs ((a (n+1))/(a n))) L)  (h₁ : L < 1) : M1P1.is_limit a 0 :=
begin
  have h₂ : (1 - L) / 2 > 0, rwa [sub_zero (1:), lt_sub, div_lt_div_right two_pos, zero_div] at h₁,
  cases h ((1 - L)/2) h₂ with N H, simp only [abs_sub_lt_iff] at H,
end

Tactic state:

a :   ,
L : ,
h : M1P1.is_limit (λ (n : ), |a (n + 1) / a n| ) L,
h₁ : L < 1,
h₂ : (1 - L) / 2 > 0,
N : ,
H :  (n : ), n  N  |a (n + 1) / a n| - L < (1 - L) / 2  L - |a (n + 1) / a n| < (1 - L) / 2
 M1P1.is_limit a 0

Is it possible for me to split the "and" inside hypothesis H?

view this post on Zulip Mario Carneiro (Feb 22 2019 at 13:54):

cases H

view this post on Zulip Calle Sönne (Feb 22 2019 at 13:55):

I tried doing that, it gives me error:
cases tactic failed, it is not applicable to the given hypothesis

view this post on Zulip Mario Carneiro (Feb 22 2019 at 13:55):

oh wait, I didn't see the forall. You can first rewrite with imp_and_distrib and forall_and_distrib

view this post on Zulip Calle Sönne (Feb 22 2019 at 13:58):

Thank you :)

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:10):

Calle, let me emphasize the natural number subtraction discussion: what you had to endure was the result of Lean not yet having enough tactics to fight natural number subtraction hell. One day Lean will catch up with the rest of the world in this area, and it will disappear. In the mean time you shouldn't think everything is hopeless. Your have h₂ : (1 - L) / 2 > 0, rwa [←sub_zero (1:ℝ), lt_sub, ←div_lt_div_right two_pos, zero_div] at h₁, is unneeded suffering. There is no nat subtraction in this statement, you can safely replace this proof with linarith

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:10):

have h₂ : (1 - L) / 2 > 0, by linarith,

view this post on Zulip Calle Sönne (Feb 22 2019 at 14:10):

theorem ratio_test (a :   ) (L : ) (h : M1P1.is_limit (λ n, abs ((a (n+1))/(a n))) L)  (h₁ : L < 1) : M1P1.is_limit a 0 :=
begin
  have h₂ : (1 - L) / 2 > 0, rwa [sub_zero (1:), lt_sub, div_lt_div_right two_pos, zero_div] at h₁,
  cases h ((1 - L)/2) h₂ with N H, simp only [abs_sub_lt_iff] at H,
  simp only [imp_and_distrib, forall_and_distrib] at H, cases H with Ha Hb,
  simp [lt_sub, add_div] at Ha,
end

Tactic state:

a :   ,
L : ,
h : M1P1.is_limit (λ (n : ), |a (n + 1) / a n| ) L,
h₁ : L < 1,
h₂ : (1 - L) / 2 > 0,
N : ,
Hb :  (x : ), x  N  L - |a (x + 1) / a x| < (1 - L) / 2,
Ha :  (x : ), x  N  |a (x + 1) / a x| < L + (2⁻¹ + -L / 2)
 M1P1.is_limit a 0

I would like to do some simple rewrites on Ha, add_assoc and add_comm. I want to get (L + 1)/2 on RHS. From what I've understood rw doesnt work inside a forall statement, and in this case simp/simp only [add_assoc] at Ha does nothing. How do I proceed?

view this post on Zulip Calle Sönne (Feb 22 2019 at 14:13):

Thank you Patrick! I always seem forget the existence of linarith.

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:13):

The easy way here is to wait until you specialize Ha

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:16):

But if you really want it, you can

  have h :  z, z - L < (1 - L) / 2  z < (1+L)/2,
  by intro z ; split ; intro ; linarith,
  simp only [h] at Ha,

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:18):

except you shouldn't call it h because you already have an h in your context...

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:20):

For very short one-shots like this, you have the option to write something like:

simp only [show  z, z - L < (1 - L) / 2  z < (1+L)/2,
             by intro z ; split ; intro ; linarith] at Ha,

that won't clutter your context at any time

view this post on Zulip Calle Sönne (Feb 22 2019 at 14:22):

thats perfect! Was already getting annoyed at the hypothesis being in the way :)

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:51):

By the way @Calle Sönne your statement of ratio_test does not hold

view this post on Zulip Patrick Massot (Feb 22 2019 at 14:51):

It's a good exercise to look for a counter-example

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:27):

Once you'll have fixed the statement, my next advice will by to first state: theorem ratio_test_aux (a : ℕ → ℝ) (L : ℝ) (hL : L < 1) (INSERT MISSING ASSUMPTION HERE) (h : ∀ n, abs ((a (n+1))/(a n)) ≤ L) : M1P1.is_limit a 0. You'll probably also want to state theorem sandwich_zero (a b : ℕ → ℝ) (hb : is_limit b 0) (hab : ∀ n, abs (a n) ≤ b n) : is_limit a 0. This way you'll be able to keep low complexity proofs

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:32):

Yes :) I noticed after a while that I needed: lean (h₂ : ∀ (n : ℕ), (a n) ≠ 0) or where you hinting at something else?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:32):

Did you find the counter-example without this assumption? (this is not an exam, I'm asking because there is an important Lean lesson to learn here, and it's better if you can figure it out for yourself)

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:37):

I did not find a counterexample, I just noticed that after a while I needed this assumption to proceed. I am not sure about the counter-example... If the assumption wasn't true then the sequence λ n, abs ((a (n+1))/(a n)) is undefined right?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:37):

Lean doesn't let you write anything undefined

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:38):

That's a very important point

view this post on Zulip Mario Carneiro (Feb 22 2019 at 15:38):

hint: what if every other value is 0?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:39):

Mario: Calle is not there yet, still needs to figure out what happens in Lean if there is some zero value

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:40):

yes

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:46):

I found that the inverse for zero is zero in field.lean, and it was proved using discrete_field.inv_zero α

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:47):

discrete_field... thats just a finite field?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:47):

no, discrete_field means field

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:47):

oh

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:47):

I saw now that its by definition?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:47):

you don't want to know why it's called discrete_field

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:48):

Ok, so x/0 is defined to be zero.

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:48):

That's good to know

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:48):

but now I want to know of course... :grinning_face_with_smiling_eyes:

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:48):

You can now progress to Mario's hint

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:48):

but wait why define it to be zero?

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:49):

to not break lean if someone (like me) does something stupid?

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:49):

There are two parts: first it has to be defined to be something, because all functions are total in type theory

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:49):

then you get to choose the value for a/0. If you choose zero then some algebraic manipulations are valid in every case

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:50):

like (a+b)/c = a/c + b /c

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:50):

ah, makes (kind of) sense

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:50):

so you get a bonus: there is no proof to give when you apply (a+b)/c = a/c + b /c

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:51):

but of course Lean will ask for a non-vanishing proof if you want to use (a*b)/b = a

view this post on Zulip Patrick Massot (Feb 22 2019 at 15:51):

because that one needs non-vanishing b

view this post on Zulip Calle Sönne (Feb 22 2019 at 15:55):

I have noticed the absence of `b != 0 in some lemmas where I thought it should be before, so this is the reason.

view this post on Zulip Mario Carneiro (Feb 22 2019 at 16:02):

So one way to strengthen your theorem is to only assume that a is eventually nonzero, or eventually with ratio less than L

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:03):

Mario, there is no eventually L

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:04):

At least not in the original statement which assumes an+1/ana_{n+1}/a_n converges to L

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:04):

But then I suggested introducing the intermediate statement you're thinking of

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:07):

I was thinking about that as well, but then one might as well make the "eventually" non-zero into a new sequence and apply the theorem. Then I have proved a theorem saying that if a sequence a (n + k) converges for some fixed k, then a n converges.

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:08):

Yes, we've seen that limit_start_irrevelant lemma, that's a good one. You still need (I think) my other two intermediate statements

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:11):

Wait... two? I thought the first one was just mine but adding the missing assumption?

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:11):

Once you'll have fixed the statement, my next advice will by to first state: theorem ratio_test_aux (a : ℕ → ℝ) (L : ℝ) (hL : L < 1) (INSERT MISSING ASSUMPTION HERE) (h : ∀ n, abs ((a (n+1))/(a n)) ≤ L) : M1P1.is_limit a 0. You'll probably also want to state theorem sandwich_zero (a b : ℕ → ℝ) (hb : is_limit b 0) (hab : ∀ n, abs (a n) ≤ b n) : is_limit a 0. This way you'll be able to keep low complexity proofs

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:12):

I can see I haven't been consistent with using the M1P1 namespace. I meant M1P1.is_limit everywhere

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:12):

But you should probably open that namespace

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:18):

Okay, so you should generally try to split theorems into auxillary lemmas even though they may not be that useful?

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:18):

To reduce complexity

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:19):

Sometimes it helps. And in this case I'm not even sure it's not useful

view this post on Zulip Patrick Massot (Feb 22 2019 at 16:19):

both those intermediate lemmas are fairly useful

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:20):

I see that the second one is useful

view this post on Zulip Calle Sönne (Feb 22 2019 at 16:21):

Okay now I see that the first can be useful as well


Last updated: May 18 2021 at 16:25 UTC