## Stream: new members

### Topic: Splitting "and" inside a function.

#### 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?

#### Mario Carneiro (Feb 22 2019 at 13:54):

cases H

#### 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

#### 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

Thank you :)

#### 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

#### Patrick Massot (Feb 22 2019 at 14:10):

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

#### 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,
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?

#### Calle Sönne (Feb 22 2019 at 14:13):

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

#### Patrick Massot (Feb 22 2019 at 14:13):

The easy way here is to wait until you specialize Ha

#### 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,


#### Patrick Massot (Feb 22 2019 at 14:18):

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

#### 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

#### Calle Sönne (Feb 22 2019 at 14:22):

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

#### Patrick Massot (Feb 22 2019 at 14:51):

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

#### Patrick Massot (Feb 22 2019 at 14:51):

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

#### 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

#### 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?

#### 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)

#### 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?

#### Patrick Massot (Feb 22 2019 at 15:37):

Lean doesn't let you write anything undefined

#### Patrick Massot (Feb 22 2019 at 15:38):

That's a very important point

#### Mario Carneiro (Feb 22 2019 at 15:38):

hint: what if every other value is 0?

#### 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

yes

#### 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 α

#### Calle Sönne (Feb 22 2019 at 15:47):

discrete_field... thats just a finite field?

#### Patrick Massot (Feb 22 2019 at 15:47):

no, discrete_field means field

oh

#### Calle Sönne (Feb 22 2019 at 15:47):

I saw now that its by definition?

#### Patrick Massot (Feb 22 2019 at 15:47):

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

#### Patrick Massot (Feb 22 2019 at 15:48):

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

#### Patrick Massot (Feb 22 2019 at 15:48):

That's good to know

#### Calle Sönne (Feb 22 2019 at 15:48):

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

#### Patrick Massot (Feb 22 2019 at 15:48):

You can now progress to Mario's hint

#### Calle Sönne (Feb 22 2019 at 15:48):

but wait why define it to be zero?

#### Calle Sönne (Feb 22 2019 at 15:49):

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

#### 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

#### 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

#### Patrick Massot (Feb 22 2019 at 15:50):

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

#### Calle Sönne (Feb 22 2019 at 15:50):

ah, makes (kind of) sense

#### 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

#### 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

#### Patrick Massot (Feb 22 2019 at 15:51):

because that one needs non-vanishing b

#### 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.

#### 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

#### Patrick Massot (Feb 22 2019 at 16:03):

Mario, there is no eventually L

#### Patrick Massot (Feb 22 2019 at 16:04):

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

#### Patrick Massot (Feb 22 2019 at 16:04):

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

#### 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.

#### 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

#### Calle Sönne (Feb 22 2019 at 16:11):

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

#### 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

#### 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

#### Patrick Massot (Feb 22 2019 at 16:12):

But you should probably open that namespace

#### 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?

#### Calle Sönne (Feb 22 2019 at 16:18):

To reduce complexity

#### Patrick Massot (Feb 22 2019 at 16:19):

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

#### Patrick Massot (Feb 22 2019 at 16:19):

both those intermediate lemmas are fairly useful

#### Calle Sönne (Feb 22 2019 at 16:20):

I see that the second one is useful

#### 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