linarith failure

Stream: maths

[Kevin Buzzard]

I've started doing basic analysis in Lean with the undergraduates and I'm really using linarith a lot, it's really handy for this sort of thing. I was trying to prove that 1/n tended to zero using it, and I ran into this:

example (a b c : ℝ) (h1 : 1 / a < b) (h2 : b < c) : 1 / a < c := by linarith -- fails

Is that a bug, or am I asking too much?

[Mario Carneiro]

that looks like a bug

[Mario Carneiro]

does generalize : 1/a = x; linarith work?

[Rob Lewis]

Yeah, that should be within scope. I'm guessing it's still too aggressive about ignoring nonlinear things, instead of trying to work with the linear parts. I fixed something related a while back iirc, but maybe not enough.

[Mario Carneiro]

linarith h1 h2 should work if it's a filtering problem

[Kevin Buzzard]

Yes, generalizing works.

[Kevin Buzzard]

linarith takes arguments??

[Mario Carneiro]

apparently (reading the src now)

[Rob Lewis]

It might reject it at the parsing step though.

[Rob Lewis]

I'll look into it soon.

[Rob Lewis]

linarith takes arguments, in case you have lots of hypotheses and know which ones are contradictory.

[Kevin Buzzard]

PS this was great:

example (x y : ℝ) : abs (x + y) ≤ abs x + abs y :=
begin
  unfold abs, unfold max,
  -- goal with three ite's in
  split_ifs,
  -- 8 goals
  repeat {linarith},
end

[Johan Commelin]

You can replace that , repeat with a ;

[Johan Commelin]

But that's less readable

[Patrick Massot]

It requires knowing what ; does, but then it's readable

[Rob Lewis]

This is buried a little deeper than I expected. It's a mistake in the part of linarith that normalizes non-integer coefficients (in norm_hyp_aux I think). I'll fix it, but not tonight.

[Kevin Buzzard]

Thanks for chasing this up! I really want to let undergraduates see that doing basic analysis in Lean is really easy, the triangle inequality proof went down really well!

[Patrick Massot]

I'm also very interested in this. Do you have files to share?

[Kevin Buzzard]

I've only given one lecture so far and I've done barely anything.

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/M1P1-lean

[Kevin Buzzard]

I proved a sequence has at most one limit; I used ring to prove things like e + e = 2 * e and Kenny was in the front row exploding.

[Kevin Buzzard]

But I can't teach all the students the 100 lemmas each of which can be proved by ring

[Kevin Buzzard]

I want to just teach them ring instead

[Kevin Buzzard]

My plan is to track their lectures and prove the interesting theorems as they're proved in class.

[Mario Carneiro]

wow, you really jumped right in

[Mario Carneiro]

in the ITP class Jeremy and I are teaching we've barely got to what a def is, how variable and section work and so on

[Kevin Buzzard]

I asked the lecturer. He said that he was going to assume that the reals were a complete archimedean field and develop everything from that.

[Patrick Massot]

This is why we need mathematicians to teach proof assistants

[Kevin Buzzard]

so my plan was to spend the term trying to prove the things he proved, but in Lean. I would imagine that many of them are in mathlib already, but I didn't even look at the definition of a sequence tending to a limit in case it used cofinite filters. Of course I used the epsilon / N definition, because that's what they're told.

[Rob Lewis]

Never mind, I fixed it tonight. There could be some similar cases that this fix misses though.

[Kevin Buzzard]

I have another linarith failure. The hypotheses involving N and n are irrelevant to the goal, and if you comment out the line with them in then linarith succeeds, but if you leave them in then it fails.

example
(N : ℕ) (n : ℕ) (Hirrelevant : n > N) -- comment out this line to fix
(A : ℝ) (l : ℝ) (h : A - l ≤ -(A - l)) (h_1 : ¬A ≤ -A) (h_2 : ¬l ≤ -l)
(h_3 : -(A - l) < 1) :  A < l + 1 := by linarith
/-
done tactic failed, there are unsolved goals
...
⊢ ↑(2 * -1) + 2 = 0
-/

[Rob Lewis]

Yeah, I know what's going on here. linarith is actually "succeeding," but Hirrelevant convinced it it was working over int instead of real, so it builds the wrong proof of contradiction. I'm on it.

[Rob Lewis]

In the meantime, you can help it out by calling linarith {restrict_type := ℝ} instead.

[Kevin Buzzard]

Is this expected behaviour?

import tactic.linarith

example (a : ℤ) (b : ℤ) (h : a < b) : a < b :=
begin
  let c := b,
  show a < c,
  linarith, -- fails
/-
linarith failed to find a contradiction
state:
a b : ℤ,
h : a < b,
c : ℤ := b,
a_1 : a ≥ c
⊢ false
-/
  sorry
end

In practice I have some positive real eps := (b - a) / 2 which is mentioned in several hypotheses and the conclusion. I can close my goal with lots of change or show commands removing all the eps's and then running linarith after, but my understanding of the internals of linarith is sufficiently poor that I don't know whether I should expect the tactic to handle these variables defined in terms of other variables or whether they're my problem.

[Kevin Buzzard]

Aah, I can do have Heps : eps = (b - a) / 2 := rfl, rw Heps at * as a workaround :-) I don't know any other way of doing multiple substitutions at once.

[Reid Barton]

Do you need the rw? After all eps = (b - a) / 2 is also a linear constraint

[Kevin Buzzard]

Well spotted :-) Yes, it works fine in my (quite complicated) use case. Excellent trick!

[Kevin Buzzard]

import tactic.linarith

example (a : ℤ) (b : ℤ) (h : a < b) : a < b :=
begin
  let c := b,
  show a < c,
  -- linarith, -- fails
  have : c = b := rfl,
  linarith, -- works
end

[Kevin Buzzard]

It's funny that c := b shows up in my local context, but the hypothesis that c = b is apparently not in it. If the let were syntactic sugar, I wouldn't need the have, right? I'm not entirely sure what's going on here. Hmm, oh OK, maybe c is defined to be b, and Lean knows this but the fact isn't in the local context. I guess I'm showing my ignorance of how things really work here. I was hoping unfold eps would work in my case but it didn't.

[Reid Barton]

It seems like tactics like rw and simp sometimes "see through" let-bound variables, and I never understood exactly when or why

[Rob Lewis]

maybe c is defined to be b

This is roughly right, a let is like a local def. It's not syntactic sugar.

but the fact isn't in the local context

The information is in the type context, which is why you see c : Z := b. There's no term of type c = b until you add it manually. I don't think linarith should unfold let bindings, since they can be used to hide arbitrarily large terms. It's analogous to unfolding definitions (which linarith doesn't do and shouldn't do).

[Kevin Buzzard]

Thanks for the clarification Rob. I didn't like my original solution (lots of 'change') but I'm happy to add the hypothesis that c equals its definition to the context and then let linarith take over. I have over 20 occurrences of linarith in https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/limits.lean so far; it's an essential tactic for this sort of thing.

[Patrick Massot]

Did you tried also using mono?

[Kevin Buzzard]

I don't know what that does.

[Kevin Buzzard]

Isn't it some disease in the US?

[Patrick Massot]

https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#mono

[Patrick Massot]

There is also https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#apply_rules

[Patrick Massot]

but apply_rules seems very slow

[Patrick Massot]

You can try to stick the following into your limits file:

-- Next lemma could be either hidden of given a user-friendly proof
lemma zero_of_abs_lt_all (x : ℝ) (h : ∀ ε > 0, |x| < ε) : x = 0 :=
eq_zero_of_abs_eq_zero $ eq_of_le_of_forall_le_of_dense (abs_nonneg x) $ λ ε ε_pos, le_of_lt (h ε ε_pos)

-- The next few things should be hidden
@[user_attribute]
meta def ineq_rules : user_attribute :=
{ name := `ineq_rules,
  descr := "lemmas usable to prove inequalities" }

attribute [ineq_rules] add_lt_add le_max_left le_max_right

meta def obvious_ineq := `[linarith <|> apply_rules ineq_rules]
run_cmd add_interactive [`obvious_ineq]
-- end of scary things

-- We're ready to prove the theorem.
theorem limits_are_unique (a : ℕ → ℝ) (l m : ℝ) (hl : is_limit a l)
(hm : is_limit a m) : l = m :=
begin
  -- Let prove |l - m| is smaller than any positive number, since that will easily imply l = m
  suffices : ∀ ε : ℝ, ε > 0 → |l - m| < ε,
    from eq_of_sub_eq_zero (zero_of_abs_lt_all _ this),
  -- Let ε be any positive number, and let's prove |l - m| < ε
  intros ε ε_pos,
  -- Because aₙ → l, there exists Nₗ such that n ≥ Nₗ → |aₙ - l| < ε/2
  cases hl (ε/2) (by obvious_ineq) with Nₗ Hₗ,
  -- Because aₙ → m, there exists Nₘ such that n ≥ Nₘ → |aₙ - m| < ε/2
  cases hm (ε/2) (by obvious_ineq) with Nₘ Hₘ,
  -- The trick is to let N be the max of Nₗ and Nₘ
  let N := max Nₗ Nₘ,
  -- Now clearly N ≥ Nₗ...
  have H₁ : Nₗ ≤ N := by obvious_ineq,
  -- ... so |a_N - l| < ε/2
  have H : | a N - l| < ε/2 := Hₗ N H₁,
  -- similarly N ≥ Nₘ...
  have H₂ : Nₘ ≤ N := by obvious_ineq,
  -- ... so |a_N - m| < ε/2 too
  have H' : | a N - m| < ε/2 := Hₘ N H₂,
  -- We now combine
  exact calc |l - m| ≤ |a N - m| + |a N - l| : triangle' _ _ _
   ... < ε/2 + ε/2 : by obvious_ineq
   ... = ε : by ring,
end

[Patrick Massot]

Note that you can put triangle' into the list of obvious inequalities and get all inequalities proved for free, but this would probably be cheating

[Kevin Buzzard]

Can this do the product of limits is limit of product?

[Kevin Buzzard]

That was horrible

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/M1P1-lean/blob/87f2b5b4dc741c5d44751678e37229c1964799e3/src/limits.lean#L299 That was where it started going wrong

[Kevin Buzzard]

linarith seems to know add_lt_add for the reals.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nonlinarith/near/157067630 Got it, thanks to you and Reid.

[Patrick Massot]

Actually I also don't like your triangle'. Remembering 10 versions of the triangle inequality is not how we teach this. You can do:

  calc
    |l - m| = |(l - a N) + (a N - m)| : by ring
        ... ≤ |l - a N| + |a N - m|   : by obvious_ineq
        ... = |a N - l | + |a N - m|  : by rw abs_sub
        ... < ε/2 + ε/2               : by obvious_ineq
        ... = ε                       : by ring,

where the only painful part is this rw abs_sub. I added abs_add, which is the regular triangle inequality for abs, to the obvious_ineq rules, but it's probably better to explicitly use it since it's a key part of the argument

[Patrick Massot]

simply replace that by obvious_ineq with abs_add _ _

[Patrick Massot]

I'll do limits of products tonight if I have time, and if I'm not too depressed about trying to use Lean for teaching (my first lecture using Lean will be at the end of this afternoon)

[Johan Commelin]

Good luck Patrick!

[Johan Commelin]

And I really like your little tactics!

[Jeremy Avigad]

A thought: it might be useful to have a tactic set that does what Kevin wants, i.e. a version of let that puts an equality in the context. For example, set h : a = t would create a new variable a, and put h : a = t into the context. Under the hood, set changes the goal G to forall a, a = t -> G, and then introduces the hypotheses. It's a combination of noting t = t, reverting, generalizing, and introducing. (But maybe there is already a nice way to do this?)

[Rob Lewis]

It seems more natural to use a let to do that. Why not preserve the definitional equality?

open tactic lean.parser interactive interactive.types

meta def tactic.set (a h : name) (v : expr) : tactic unit :=
do tp ← infer_type v,
   nv ← definev a tp v,
   to_expr ``(%%nv = %%v) >>= assert h,
   reflexivity

meta def tactic.interactive.set (h : parse ident) (_ : parse (tk ":")) (a : parse ident)
  (_ : parse (tk ":=")) (v : parse texpr) :=
i_to_expr v >>= tactic.set a h

example (x y : ℕ) : x + y + x + y + x + y = 5 :=
begin
  set h : n := x + y,
end

[Jeremy Avigad]

Looks good to me!

[Kevin Buzzard]

The syntax looks a bit funny, it looks like h has type n :-/

[Rob Lewis]

It is unfortunately not analogous to let h : n := x + y. Better suggestion?

[Kevin Buzzard]

I remember always being muddled by generalize...

[Rob Lewis]

set n := x + y using h?

[Kevin Buzzard]

maybe that's better!

[Kevin Buzzard]

cool little parser exercise to do now :-)

[Johan Commelin]

set n := x + y with h in analogy with cases ... with etc.
I think using will "use" one of your current hypotheses, or some expression (like in simpa),
whereas with gives names for new hypotheses.

[Sebastien Gouezel]

Is it possible to even get let n := x + y with h?

[Patrick Massot]

In addition to syntax discussions, the question is whether this tactic should replace x+y by n everywhere, or only in the goal, or nowhere.

[Johan Commelin]

In the example that Rob posted, associativity would prevent a naive replacement to yield n+n+n = 5, right? So then the replacement algorithm needs to know about associativity, and it becomes complicated.

[Rob Lewis]

Yeah, the example doesn't illustrate this very well. Maybe a variant set! n := x + y with h could try simp only [h.symm] at * at the end. But I think it's better not to do this by default, to match the behavior of let.

[Rob Lewis]

@Sebastien Gouezel tactic.interactive.let is defined in core, so I'm afraid not.

[Rob Lewis]

I've added this. The basic syntax is set n := x + y with h. Alternatives: set! n := x + y with h will rewrite x + y to n everywhere it can. set n := x + y with h⁻¹ will make the equality proof face the other direction.

[Rob Lewis]

I ended up needing this tactic for something I was doing yesterday, heh. It also led me to another bug in linarith.

[Mario Carneiro]

how is this different from let?

[Rob Lewis]

It adds a hypothesis that states the new definition propositionally.

[Mario Carneiro]

is it also a let?

[Rob Lewis]

Yes.

[Mario Carneiro]

I think the set n := x + y variant may also be useful - no equality assumption, but x + y gets replaced by n

[Mario Carneiro]

I think that set! should be the default behavior, I'm not sure where the set behavior is better

[Mario Carneiro]

also I suggest <- h instead of h⁻¹ for the reversed proof - we haven't used the inverse symbol for symmetry since lean 2

[Kenny Lau]

Next time could we discuss the details before making changes to the mathlib in order to minimize changes to tactic/interactive.lean?

[Rob Lewis]

I chose this as the default because set! sometimes reorders hypotheses, which is a little annoying if you don't care. It's not a big deal though, I can change it. Sure, the behavior without an equality hypothesis sounds good, as well as the notation.

[Mario Carneiro]

I hope that the changes can be obtained by change rather than rw

[Rob Lewis]

change at * seems to have a bug, it fails completely.

[Rob Lewis]

Or rather, it succeeds without doing anything.

[Mario Carneiro]

you have to do it somewhat manually with the noninteractive change

[Mario Carneiro]

you revert the relevant hypotheses then use tactic.change

[Rob Lewis]

I'll give it another shot. I tried this first, but it was behaving strangely.

[Rob Lewis]

Gotta run, lunchtime.

[Sebastien Gouezel]

set-related question, although indirectly. I have an element of fin n given by a complicated formula, to which I would like to give a name for clarity. let x := complicated_expression works fine, but it would even be more useful for me to give a name to the fields of x directly, i.e., to write let ⟨i, hi⟩ := complicated_expression. This does not work. I can define x, and then let i := x.1, let hi := x.2, but then the fact that ⟨i, hi⟩ = complicated_expression is not refl, it requires a proof based for instance on fin.ext_iff. All this looks like useless plumbing to me. Is there a nice syntax to do this that I am unaware of?

[Kevin Buzzard]

Sebastien's question above deserves some expert comment but perhaps it's not in the right thread.

Independent of all this, here's an interesting session:

import tactic.linarith

example (α : Type*) [linear_ordered_ring α] (r s : α) :
-s + (r - (r - s)) = 0 := by ring -- fails, I think because α is not commutative

example (α : Type*) [linear_ordered_ring α] (r s : α) :
-s + (r - (r - s)) = 0 := by simp -- works

example (α : Type*) [linear_ordered_ring α] (r s : α) (h : s ≥ 0) :
r - s ≤ r := by linarith -- fails because of unsolved goal -s + (r - (r - s)) = 0

example (α : Type*) [linear_ordered_ring α] (r s : α) (h : s ≥ 0) :
r - s ≤ r := by linarith {discharger := simp} -- "unknown identifier 'simp'"

I have been building the theory of decimal expansions so that I can formalise last year's M1F final exam in Lean, and I was surprised to find that linear_ordered_rings were not commutative! Does anyone know an example of a linearly ordered ring which is not commutative? It is not even entirely impossible that they are all commutative, although I've not thought about this; it's probably more likely that there are pathological examples. Is every linearly ordered floor ring commutative though?? Hmm, I seem to have wandered off topic myself.

Anyway, of course I could just take the lame way out and restrict to linear_ordered_comm_rings, which ultimately I will surely end up doing, but I tried to work my way around this using simp and realised that I could not get the discharger argument to linarith working. Unfortunately my knowledge of meta lean is still sufficiently poor that I basically grind to a halt here when trying to debug why {discharger := simp} fails. Did I do something wrong or is there a bug?

[Mario Carneiro]

To sebastian's question: it is impossible to achieve exactly the defeqs that he would want. In general it is not possible to get ⟨i, hi⟩ = complicated_expression to be defeq, unless complicated_expression has a particular form that allows reduction to a constructor

[Mario Carneiro]

However rcases complicated_expression with ⟨i, hi⟩ will often achieve the desired result, provided you don't need to refer back to any more properties of complicated_expression after this point. (If you do, you can make sure to state them before the cases)

[Kevin Buzzard]

Would cases complicated_expression with i hi be any different?

[Mario Carneiro]

no

[Mario Carneiro]

rcases just looks a bit closer to the other syntax

[Mario Carneiro]

does abel work on those goals?

[Kevin Buzzard]

I'm going to move the floor_ring discussion elsewhere.

[Kevin Buzzard]

abel -> r + gsmul (-1) s ≤ r

[Mario Carneiro]

My bet is that there are noncomm linear ordered rings

[Rob Lewis]

For the discharger question, use `[simp] instead.

[Sebastien Gouezel]

However rcases complicated_expression with ⟨i, hi⟩ will often achieve the desired result, provided you don't need to refer back to any more properties of complicated_expression after this point. (If you do, you can make sure to state them before the cases)

This is not an option in my case, I need to keep all information on complicated_expression. Fine, I'll go with my basic ugly (but working) solution, letting the components separately and proving the equality.

[Mario Carneiro]

you should be able to get the equality on the components if you use set

[Sebastien Gouezel]

To try this, I have to rebase on a recent mathlib version :)

[Mario Carneiro]

I need to keep all information on complicated_expression.

This is almost certainly not true, it's just a question of how much information about the expression you need to retain. Of course the limiting case is where you keep the fact that the expression is equal to complicated_expression, in which case you get that equality ⟨i, hi⟩ = complicated_expression you said originally

[Kevin Buzzard]

I'm reclaiming #maths for Lean maths questions.

I was surprised that the following didn't work:

import Mathlib.Tactic

example (a b : ℕ) (h1 : b ≠ a) (h2 : b ≤ a) : b < a := by linarith -- fails
example (a b : ℕ) (h1 : b ≠ a) (h2 : ¬a < b) : b < a := by linarith -- fails

Is this to be expected? I tried it in Lean 3 and they don't work there either.

[Kyle Miller]

If you add set_option trace.linarith true you can see that in both of them it filters and transforms the hypotheses down to [b ≤ a, b ≥ a] . I guess it filters out b ≠ a?

[Alex J. Best]

There is a commented out preprocessor for this in the code (as it wasn't ported yet), but it was never part of the deafult preprocessor set (possibly as you get a quadratic growth in number of goals with number of ne's).
In lean 3 you could do the very succinct

import tactic

set_option trace.linarith true

example (a b : ℕ) (h1 : b ≠ a) (h2 : b ≤ a) : b < a := by linarith {preprocessors := some  ([linarith.remove_ne] ++ linarith.default_preprocessors)}
example (a b : ℕ) (h1 : b ≠ a) (h2 : ¬a < b) : b < a := by linarith {preprocessors := some  ([linarith.remove_ne] ++ linarith.default_preprocessors)}

[Kevin Buzzard]

I think I'll stick to push_neg at h2; exact lt_of_le_of_ne _ _ :-)

[Alex J. Best]

Ok I missed something actually, its not as bad as I made it look, the following works in lean 3, and we should port it to lean 4

import tactic

set_option trace.linarith true

example (a b : ℕ) (h1 : b ≠ a) (h2 : b ≤ a) : b < a := by linarith {split_ne:=true}
example (a b : ℕ) (h1 : b ≠ a) (h2 : ¬a < b) : b < a := by linarith {split_ne:=true}

[Alex J. Best]

I implemented this at #6014 and added your examples as tests