Zulip Chat Archive

Stream: new members

Topic: linarith substitution


Iocta (Jul 21 2020 at 19:59):

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) ( : 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 (Jul 21 2020 at 20:00):

what is the error, including the proof state?

Iocta (Jul 21 2020 at 20:01):

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 (Jul 21 2020 at 20:02):

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 (Jul 21 2020 at 20:03):

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

Iocta (Jul 21 2020 at 20:04):

Thanks

Kevin Buzzard (Jul 21 2020 at 20:40):

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 (Jul 21 2020 at 20:42):

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


Last updated: Dec 20 2023 at 11:08 UTC