different behaviour of linarith

Stream: new members

[Shi Zhengyu]

Hi all, recently I noticed that linarith seems to have different behaviour based on where it's called.
e.g. have hint1: foo := by linarith then cases h (hint1) with u h'seems to have a better chance of finding solution than
cases h (by linarith) with u h' in my case.
Why?

Edit: This is the tutorial problem 0067:

-- 0067
example (u : ℕ → ℝ) (l : ℝ) (h : seq_limit u l) (h' : nondecreasing_seq u) :
  ∀ n, u n ≤ l :=
begin
  intro n, by_contradiction notub, push_neg at notub,
  let t := (u n - l) / 2,
  have hint : (u n - l) / 2 > 0 := by linarith,
  have hint2 : (u n - l) > (u n - l) / 2 := by linarith,
  unfold seq_limit at *,
  cases h t (hint) with N h'',
  clear hint h,
  let hm := max n N,
  have crit1 := h'' hm (le_max_right n N),
end

The hint and hint2 are in the situation I described above.

[Reid Barton]

Well, without looking at your example closely, you provided more information in the first case, namely the type foo.
It has to be definitionally equal to the expected argument type of h, but that definitional equality might involve some unfolding that linarith doesn't know it should do.