Splitting "and" inside a function.

Stream: new members

[Calle Sönne]

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]

cases H

[Calle Sönne]

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

[Mario Carneiro]

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

[Calle Sönne]

Thank you :)

[Patrick Massot]

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]

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

[Calle Sönne]

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?

[Calle Sönne]

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

[Patrick Massot]

The easy way here is to wait until you specialize Ha

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

Lean doesn't let you write anything undefined

[Patrick Massot]

That's a very important point

[Mario Carneiro]

hint: what if every other value is 0?

[Patrick Massot]

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

[Calle Sönne]

yes

[Calle Sönne]

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

[Calle Sönne]

discrete_field... thats just a finite field?

[Patrick Massot]

no, discrete_field means field

[Calle Sönne]

oh

[Calle Sönne]

I saw now that its by definition?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

That's good to know

[Calle Sönne]

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

[Patrick Massot]

You can now progress to Mario's hint

[Calle Sönne]

but wait why define it to be zero?

[Calle Sönne]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Calle Sönne]

ah, makes (kind of) sense

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

because that one needs non-vanishing b

[Calle Sönne]

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]

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]

Mario, there is no eventually L

[Patrick Massot]

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

[Patrick Massot]

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

[Calle Sönne]

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]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

But you should probably open that namespace

[Calle Sönne]

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

[Calle Sönne]

To reduce complexity

[Patrick Massot]

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

[Patrick Massot]

both those intermediate lemmas are fairly useful

[Calle Sönne]

I see that the second one is useful

[Calle Sönne]

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