linarith substitution

Stream: new members

[Iocta]

Why doesn't linarith work at the bottom?

import analysis.specific_limits
import data.int.parity

attribute [instance] classical.prop_decidable

/-
Lemmas from that file were hidden in my course, or restating things which
were proved without name in previous files.
-/

notation `|`x`|` := abs x

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m



def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε


def cluster_point (u : ℕ → ℝ) (a : ℝ) :=
∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a

variable { φ : ℕ → ℕ}
variables {u : ℕ → ℝ} {a l : ℝ}

lemma near_cluster :
  cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
sorry
end

/-
The above exercice can be done in five lines.
Hint: you can use the anonymous constructor syntax when proving
existential statements.
-/

/-- If `u` tends to `l` then its subsequences tend to `l`. -/
-- 0041
lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) :
seq_limit (u ∘ φ) l :=
sorry



lemma unique_limit {u l l'} : seq_limit u l → seq_limit u l' → l = l' :=
sorry


/-- If `u` tends to `l` all its cluster points are equal to `l`. -/
-- 0042
lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l :=
sorry


/-- Cauchy_sequence sequence -/
def cauchy_sequence (u : ℕ → ℝ) :=
∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε



/-
In the next exercise, you can reuse
 near_cluster : cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε
-/
-- 0044
example (hu : cauchy_sequence u) (hl : cluster_point u l) : seq_limit u l :=
begin
intros ε ε_pos,
specialize hu (ε/2) (by linarith),
cases hu with N hN,
use N,
intros n hn,
have exists_N': ∃ N' ≥ N, | u N' - l | ≤ ε / 2,
  apply near_cluster hl (ε / 2) (by linarith),
cases exists_N' with N' hN',
cases hN' with N'_ge_N N'_close,
specialize hN N' n N'_ge_N hn,
calc | u n - l | = | u n - u N'  + (u N' - l) | : by ring
... ≤ | u n - u N' | + | u N' - l | : by apply abs_add
... ≤ ε / 2 + ε / 2 : by linarith -- XXX Doesn't work
... ≤ ε : by linarith
end

[Reid Barton]

what is the error, including the proof state?

[Iocta]

linarith failed to find a contradiction
state:
u : ℕ → ℝ,
l : ℝ,
hl : cluster_point u l,
ε : ℝ,
ε_pos : ε > 0,
N n : ℕ,
hn : n ≥ N,
N' : ℕ,
N'_ge_N : N' ≥ N,
N'_close : |u N' - l| ≤ ε / 2,
hN : |u N' - u n| ≤ ε / 2,
a : |u n - u N'| + |u N' - l| > ε / 2 + ε / 2
⊢ false
state:
u : ℕ → ℝ,
l : ℝ,
hl : cluster_point u l,
ε : ℝ,
ε_pos : ε > 0,
N n : ℕ,
hn : n ≥ N,
N' : ℕ,
N'_ge_N : N' ≥ N,
N'_close : |u N' - l| ≤ ε / 2,
hN : |u N' - u n| ≤ ε / 2
⊢ |u n - l| ≤ ε

[Reid Barton]

You have a hypothesis about |u N' - u n| not |u n - u N'| and linarith doesn't know they're equal?

[Alex J. Best]

What Reid said, you can do by by rw abs_sub; linarith instead

[Iocta]

Thanks

[Kevin Buzzard]

When I was using linarith to solve goals like this, I would incredulously ask the designer why linarith didn't just apply things like abs_sub automatically, given that it's clearly a linear inequality kind of thing. The answer is that tactics are there to do one job and to do it well, and job of linarith is to deal with goals and hypotheses of the form x<=y and x=y and x<y. The moment you start asking it to do more, eg hypotheses of the form a<b \and c<d you are facing the possibility of chaos as it starts unfolding everything in case it turns out to be an inequality. It's the user's job to reduce everything to plain a<=b statements because that's where the tactic starts it's work -- that's it's specification. Once all this sunk in I began to be able to use linarith much more effectively.

[Kevin Buzzard]

When working with absolute values you need to know stuff like abs_le and le_abs etc and apply them yourself to break everything into bare inequalities, so it's worth knowing the basic interface for abs with these kinds of question