## Stream: maths

### Topic: linarith failure

#### Kevin Buzzard (Jan 17 2019 at 19:47):

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 (Jan 17 2019 at 19:48):

that looks like a bug

#### Mario Carneiro (Jan 17 2019 at 19:49):

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

#### Rob Lewis (Jan 17 2019 at 19:50):

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 (Jan 17 2019 at 19:54):

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

#### Kevin Buzzard (Jan 17 2019 at 19:54):

Yes, generalizing works.

#### Kevin Buzzard (Jan 17 2019 at 19:54):

linarith takes arguments??

#### Rob Lewis (Jan 17 2019 at 19:54):

It might reject it at the parsing step though.

#### Rob Lewis (Jan 17 2019 at 19:55):

I'll look into it soon.

#### Rob Lewis (Jan 17 2019 at 19:55):

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

#### Kevin Buzzard (Jan 17 2019 at 20:12):

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 (Jan 17 2019 at 20:12):

You can replace that , repeat with a ;

#### Patrick Massot (Jan 17 2019 at 20:13):

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

#### Rob Lewis (Jan 17 2019 at 20:34):

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 (Jan 17 2019 at 20:35):

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 (Jan 17 2019 at 20:37):

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

#### Kevin Buzzard (Jan 17 2019 at 20:37):

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

#### Kevin Buzzard (Jan 17 2019 at 20:39):

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

#### Kevin Buzzard (Jan 17 2019 at 20:40):

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 (Jan 17 2019 at 20:40):

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

#### Kevin Buzzard (Jan 17 2019 at 20:40):

I want to just teach them ring instead

#### Kevin Buzzard (Jan 17 2019 at 20:43):

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

#### Mario Carneiro (Jan 17 2019 at 20:44):

wow, you really jumped right in

#### Mario Carneiro (Jan 17 2019 at 20:44):

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 (Jan 17 2019 at 20:45):

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 (Jan 17 2019 at 20:45):

This is why we need mathematicians to teach proof assistants

#### Kevin Buzzard (Jan 17 2019 at 20:46):

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 (Jan 17 2019 at 22:24):

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

#### Kevin Buzzard (Jan 24 2019 at 13:14):

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 (Jan 24 2019 at 14:52):

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 (Jan 24 2019 at 14:52):

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

#### Kevin Buzzard (Jan 28 2019 at 21:13):

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 (Jan 28 2019 at 21:16):

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 (Jan 28 2019 at 21:18):

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

#### Kevin Buzzard (Jan 28 2019 at 21:19):

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

#### Kevin Buzzard (Jan 28 2019 at 21:23):

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 (Jan 28 2019 at 21:25):

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 (Jan 28 2019 at 21:42):

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

#### Rob Lewis (Jan 28 2019 at 21:45):

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 (Jan 28 2019 at 21:56):

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 (Jan 28 2019 at 21:58):

Did you tried also using mono?

#### Kevin Buzzard (Jan 28 2019 at 21:59):

I don't know what that does.

#### Kevin Buzzard (Jan 28 2019 at 21:59):

Isn't it some disease in the US?

#### Patrick Massot (Jan 28 2019 at 22:01):

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

#### Patrick Massot (Jan 28 2019 at 22:06):

but apply_rules seems very slow

#### Patrick Massot (Jan 28 2019 at 22:08):

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" }

meta def obvious_ineq := [linarith <|> apply_rules ineq_rules]
-- 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 (Jan 28 2019 at 22:10):

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 (Jan 28 2019 at 22:27):

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

#### Kevin Buzzard (Jan 28 2019 at 22:27):

That was horrible

#### Kevin Buzzard (Jan 28 2019 at 22:27):

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

#### Kevin Buzzard (Jan 28 2019 at 23:00):

linarith seems to know add_lt_add for the reals.

#### Kevin Buzzard (Jan 28 2019 at 23:45):

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

#### Patrick Massot (Jan 29 2019 at 08:27):

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 (Jan 29 2019 at 08:27):

simply replace that by obvious_ineq with abs_add _ _

#### Patrick Massot (Jan 29 2019 at 08:28):

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 (Jan 29 2019 at 09:01):

Good luck Patrick!

#### Johan Commelin (Jan 29 2019 at 09:01):

And I really like your little tactics!

#### Jeremy Avigad (Jan 29 2019 at 13:26):

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 (Jan 29 2019 at 13:59):

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 (Jan 29 2019 at 14:27):

Looks good to me!

#### Kevin Buzzard (Jan 29 2019 at 14:42):

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

#### Rob Lewis (Jan 29 2019 at 14:43):

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

#### Kevin Buzzard (Jan 29 2019 at 14:44):

I remember always being muddled by generalize...

#### Rob Lewis (Jan 29 2019 at 14:45):

set n := x + y using h?

#### Kevin Buzzard (Jan 29 2019 at 14:45):

maybe that's better!

#### Kevin Buzzard (Jan 29 2019 at 14:45):

cool little parser exercise to do now :-)

#### Johan Commelin (Jan 29 2019 at 15:03):

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 (Jan 29 2019 at 17:18):

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

#### Patrick Massot (Jan 29 2019 at 19:41):

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 (Jan 29 2019 at 19:44):

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 (Jan 29 2019 at 20:17):

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 (Jan 29 2019 at 20:18):

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

#### Rob Lewis (Feb 01 2019 at 11:18):

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 (Feb 01 2019 at 11:19):

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

#### Mario Carneiro (Feb 01 2019 at 11:35):

how is this different from let?

#### Rob Lewis (Feb 01 2019 at 11:36):

It adds a hypothesis that states the new definition propositionally.

#### Mario Carneiro (Feb 01 2019 at 11:36):

is it also a let?

Yes.

#### Mario Carneiro (Feb 01 2019 at 11:37):

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

#### Mario Carneiro (Feb 01 2019 at 11:38):

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

#### Mario Carneiro (Feb 01 2019 at 11:39):

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 (Feb 01 2019 at 11:41):

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

#### Rob Lewis (Feb 01 2019 at 11:42):

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 (Feb 01 2019 at 11:43):

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

#### Rob Lewis (Feb 01 2019 at 11:43):

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

#### Rob Lewis (Feb 01 2019 at 11:43):

Or rather, it succeeds without doing anything.

#### Mario Carneiro (Feb 01 2019 at 11:44):

you have to do it somewhat manually with the noninteractive change

#### Mario Carneiro (Feb 01 2019 at 11:44):

you revert the relevant hypotheses then use tactic.change

#### Rob Lewis (Feb 01 2019 at 11:46):

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

#### Rob Lewis (Feb 01 2019 at 11:46):

Gotta run, lunchtime.

#### Sebastien Gouezel (Feb 01 2019 at 16:01):

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 (Feb 04 2019 at 10:45):

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 (Feb 04 2019 at 10:49):

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 (Feb 04 2019 at 10:50):

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 (Feb 04 2019 at 10:51):

Would cases complicated_expression with i hi be any different?

no

#### Mario Carneiro (Feb 04 2019 at 10:51):

rcases just looks a bit closer to the other syntax

#### Mario Carneiro (Feb 04 2019 at 10:53):

does abel work on those goals?

#### Kevin Buzzard (Feb 04 2019 at 10:54):

I'm going to move the floor_ring discussion elsewhere.

#### Kevin Buzzard (Feb 04 2019 at 10:54):

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

#### Mario Carneiro (Feb 04 2019 at 10:55):

My bet is that there are noncomm linear ordered rings

#### Rob Lewis (Feb 04 2019 at 10:56):

For the discharger question, use  [simp] instead.

#### Sebastien Gouezel (Feb 04 2019 at 11:01):

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 (Feb 04 2019 at 11:01):

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

#### Sebastien Gouezel (Feb 04 2019 at 11:02):

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

#### Mario Carneiro (Feb 04 2019 at 11:03):

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

Last updated: May 12 2021 at 07:17 UTC