linarith

Stream: general

[Johan Commelin]

Shouldn't linarith be able to take care of this?

n : ℕ,
i : fin (n + 1 + 1),
a b : fin (n + 1),
ha : ¬a.val < i.val,
h : b.val < i.val,
H : a.val ≤ b.val,
a_1 : nat.succ (a.val) > b.val
⊢ false

[Kenny Lau]

I thought it has been made clear that linarith doesn't deal with nat

[Patrick Massot]

After apply ha it should be an easy target for mono but it doesn't work :sad:

[Patrick Massot]

@Simon Hudon

import tactic.monotonicity

example (n : ℕ)
(i : fin (n + 1 + 1))
(a b : fin (n + 1))
(ha : ¬a.val < i.val)
(h : b.val < i.val)
(H : a.val ≤ b.val)
(a_1 : nat.succ (a.val) > b.val) : false :=
begin
  apply ha,
  mono*,  -- does nothing :-(
  exact calc a.val ≤ _ : H
  ... < _ : h,
end

[Rob Lewis]

Change nat.succ (a.val) to a.val + 1.

[Patrick Massot]

This is the first thing I tried, but it changes nothing

[Kenny Lau]

maybe stop (over)relying on tactics

[Rob Lewis]

Oh, change ha to a.val ≥ i.val.

[Patrick Massot]

that works

[Patrick Massot]

Kenny, the discussion is not really about how to prove that particular goal. It's about having a toolset which gets rid of hundred of stupid goals like this, that would otherwise break our proof flow and concentration

[Rob Lewis]

There's something wrong with the routine that makes linarith work for nat and the part that deals with negated hypotheses, I'll look into it when I have a minute.

[Patrick Massot]

Nice! In the mean time, Johan can use replace ha := le_of_not_lt ha ; linarith to close that goal

[Rob Lewis]

Or apply ha; linarith.

[Patrick Massot]

indeed

[Sebastien Gouezel]

Another linarithwishlist entry: if there is an assumption abs x ≤ c, convert it to x ≤ c and -x ≤ c.

[Rob Lewis]

There are various unfolding/preprocessing things like that, that linarith could do. Writing a separate tactic that unfolds abs would be very easy, and you could even add meta def linarith' := unfold_abs; linarith if you wanted. But I'm not sure that bundling all these things into the main tactic is a good idea.

[Rob Lewis]

There's now a PR open to fix Johan's problem, btw.

[Sebastien Gouezel]

OK, I understand. I can definitely unfold it by hand when needed. I am just motivated by the principle of maximal laziness.

[Johan Commelin]

@Rob Lewis Cool! Thanks a lot.

[Johan Commelin]

Now there is still the problem with nat.succ _ vs _ + 1. Could that be fixed as well?

[Johan Commelin]

Because then I could run split_ifs with foo bar; {ext, simp, linarith} and be done with it. Otherwise I need to explicitly change my goal for each goal. Or should I write a custom simp-lemma for this, that I use locally?

[Johan Commelin]

lemma δ_monotone (i : [n+1]) : monotone (δ i) :=
begin
  intros a b H,
  change a.val ≤ b.val at H,
  dsimp [fin.succ_above],
  split_ifs with ha hb;
  try { ext1, simp, linarith },
  { ext1, simp, change _ ≤ _ + 1, linarith },
  { ext1, simp, change _ + 1 ≤ _ + 1, linarith }
end

[Rob Lewis]

@Sebastien Gouezel If you don't want to do it by hand, you can finish this and use it (or modify it to fit your purposes). Just use unfold_abs; linarith in place of linarith, or define an alias for that.

open tactic
lemma le_and_le_of_abs_le {α} [decidable_linear_ordered_comm_group α] {a b : α} (h : abs a ≤ b) : a ≤ b ∧ -a ≤ b :=
sorry

meta def unfold_abs : tactic unit :=
local_context >>= list.mmap' (λ e, try (mk_app `le_and_le_of_abs_le [e] >>= cases))

example (a b c : ℤ) (h : abs a ≤ b) (h2 : abs b ≤ c) : true :=
begin
  unfold_abs
end

[Rob Lewis]

@Johan Commelin This falls into the same basket as Sebastien's request. There are lots of constants that can be unfolded or rewritten into a form that linarith will handle. I don't want to build them all in. You can just add nat.succ_eq_add_one to the simp call.

[Johan Commelin]

Ok, thanks, will do.

[Johan Commelin]

maybe stop (over)relying on tactics

@Kenny Lau Can you golf this?

lemma δ_monotone (i : [n+1]) : monotone (δ i) :=
λ a b (H : a.val ≤ b.val),
by dsimp [fin.succ_above]; split_ifs with ha hb; { ext1, simp [nat.succ_eq_add_one], linarith }

You can find it here: https://github.com/leanprover-community/mathlib/blob/simplicial/algebraic_topology/simplex_category.lean#L33-L35

[Johan Commelin]

@Rob Lewis So presumably goals of this form are also outside the scope of linarith?

n : ℕ,
i j : fin (n + 1 + 1),
H : i ≤ j,
a : fin (n + 1),
h : a.val < i.val,
h_1 : (fin.cast_succ a).val < (fin.succ j).val,
h_2 : ¬a.val < j.val,
h_3 : ¬(fin.succ a).val < i.val
⊢ a.val = 1 + (1 + a.val)

I have 7 goals that are all of this form or another... I would like to kill them all in one go.

[Johan Commelin]

Sorry, I should paste context...

[Kevin Buzzard]

So these are nats?

[Kevin Buzzard]

What is the argument in maths?

[Rob Lewis]

Um, linarith doesn't know anything about the relation between fin and fin.val, or anything about fin.succ or fin.cast_succ.

[Kevin Buzzard]

I am not sure you can ask linarith to start unfolding fin.succ or stuff like that

[Kevin Buzzard]

There will be a never-ending list of things you want it to unfold.

[Rob Lewis]

Basically, those are a bunch of random inequalities between distinct variables, not even all of the same type.

[Rob Lewis]

The only thing linarith will learn is that j.val < i.val.

[Kevin Buzzard]

What about x ∈ {a : ℕ | a > 5} ? That unfolds to an inequality, but it's surely not linarith's job to figure that out.

[Kenny Lau]

@Johan Commelin there must be such a function in mathlib

[Kenny Lau]

(or not)

[Kenny Lau]

(yes it’s decidable)

[Rob Lewis]

@Kevin Buzzard right, see my last few comments. :slight_smile: Infinitely many things can unfold to linear inequalities. If linarith tries everything possible it will be unpredictable and slow.

[Johan Commelin]

Cool, I'm getting the hang of this! @Rob Lewis Thanks for your help. I'm starting to understand how to play with linarith.
After:

lemma simplicial_identity₁ {i j : [n+1]} (H : i ≤ j) : δ j.succ ∘ δ i = δ i.cast_succ ∘ δ j :=
begin
  change i.val ≤ j.val at H,
  funext a,
  dsimp [fin.succ_above],
  split_ifs; { try {ext1}, try {simp [nat.succ_eq_add_one] at *}, try {linarith} },
end

Before:

lemma simplicial_identity₁ {i j : [n+1]} (H : i ≤ j) : δ j.succ ∘ δ i = δ i.cast_succ ∘ δ j :=
begin
  funext a,
  dsimp [fin.succ_above],
  by_cases hja : (j.val < a.val),
  { have hja' : ((fin.succ j).val < (fin.succ a).val) :=
    begin
      simp,
      exact nat.succ_le_succ hja,
    end,
    have hia : ((i.cast_succ).val < (fin.succ a).val) :=
    begin
      simp,
      refine (lt_of_le_of_lt H _),
      exact (nat.le_trans hja (nat.le_succ a.val))
    end,
    rw [if_pos hja, if_pos (nat.le_trans H hja), if_pos hja', if_pos hia]},
  { rw [dif_neg hja],
    by_cases hia : (i.val ≤ a.val),
    { have hia' : ((fin.raise i).val ≤ (fin.raise a).val) := hia,

      have hja' : ¬(j.succ.val ≤ a.succ.val) :=
      begin
        simp at *,
        exact nat.succ_le_succ hja
      end,
      rw [dif_pos hia, dif_pos hia', dif_neg hja'],
      simp [fin.raise],
      apply fin.eq_of_veq,
      simp},
    { have hja' : ¬(j.succ.val ≤ a.raise.val) :=
      begin
        simp at *,
        exact nat.le_trans hja (nat.le_succ j.val)
      end,
      have hia' : ¬((fin.raise i).val ≤ (fin.raise a).val) :=
      begin
        unfold fin.raise, exact hia
      end,
      rw [dif_neg hia, dif_neg hja', dif_neg hia']}}
end

[Johan Commelin]

@Kenny Lau Do you mean it should be provable by dec_trivial?

[Simon Hudon]

@Patrick Massot @Rob Lewis Did the problem turn out to be mono?

[Patrick Massot]

linarith doesn't use mono so the bug in linarith had nothing to do with mono (and is now fixed). But I'm still disappointed I can't get mono to help here

[Patrick Massot]

You can try, what I posted right after pinging you is a MWE

[Patrick Massot]

search for "does nothing" in this thread

[Simon Hudon]

I wouldn't expect it to do anything in that case. What would you expect it to do?

[Patrick Massot]

I would expect it to close the goal

[Simon Hudon]

You mean using mixed transitivity? It doesn’t do that. What it does is identify a monotonic function on either side of a relation. < is that relation in your case but it doesn’t have a monotonic function on both sides.

[Simon Hudon]

If you want, you can treat < as the monotonic function and -> as the relation.

[Simon Hudon]

To do that, you need to do revert h before mono.

[Patrick Massot]

This is sad. We need something like cc for inequality, working together with mono

[Simon Hudon]

Maybe something like what I did for tfae would work for that

[Patrick Massot]

Except tfae doesn't work :sad:

[Patrick Massot]

The following is ridiculous but gives hope:

example (p q r : ℕ) (h : p ≤ q) (h' : q ≤ r) : p ≤ r :=
begin
  refine le_trans _ _,
  swap,
  tauto,
  tauto
end

[Patrick Massot]

This is the kind goal I hope some "cc for inequalities" would solve

[Simon Hudon]

What is tricky for this kind of tactic is that one would expect it to work in the case of mixed transitivity which makes selecting a relation a bit more difficult. I could do it specifically for < and ≤ to simplify things but it's a bit disappointing in terms of generality

[Simon Hudon]

But in the situations that you're showing, it seems like the kind of stuff linarith should handle

[Rob Lewis]

Patrick, can you elaborate on what you mean by "cc for inequalities"?

[Chris Hughes]

I think he more or less means solvable using linear order axioms, without any algebra.

[Chris Hughes]

But I think linarith does those.

[Rob Lewis]

Ah. Yeah, linarith does those. But I guess it requires some extra algebraic structure on the type that isn't always necessary.

[Chris Hughes]

And maybe preorder axioms and partial order axioms would be nice as well.

[Rob Lewis]

Indeed. A tactic for this kind of transitivity reasoning would be a nice project for someone who wants to learn about writing tactics. :wink:

[Rob Lewis]

Note, I haven't really looked into mono yet, so I'm not sure how much overlap there is.

[Simon Hudon]

There isn't much overlap actually. To implement this tactic, tfae would be more helpful. It calculates the transitive closure of implication on the local assumptions.

[Simon Hudon]

You replace implication by a preorder and you'd get what Patrick is talking about with the additional difficulty of handling < properly

[Rob Lewis]

Ah, sure. Sounds reasonable enough.

[Patrick Massot]

I'd love to try to understand how to adapt tfae here, but again I don't think this would be reasonable before we get a deterministic behavior from tfae

[Kenny Lau]

@Johan Commelin I see someone has figured out the function in mathlib

[Johan Commelin]

@Kenny Lau Wait, which function in mathlib are you referring to?

[Kenny Lau]

@Johan Commelin fin.succ_above

[Johan Commelin]

Aah, yes, I'm using that one. Was that answering a question of mine?

[Johan Commelin]

Or maybe you just think it is confusing notation? It probably is...

[Kenny Lau]

never mind, ignore me

[Scott Morrison]

More requests: are these reasonable to expect from linarith?

n m : ℕ,
h₁ : n < m,
⊢ n + 1 ≤ m

and

n m l : ℕ,
a_left : n ≤ l,
a_right : l < n + (m - n)
⊢ l < m

and

a_left : n ≤ l,
a_right : l < m
⊢ l < n + (m - n)

[Kenny Lau]

The following is ridiculous but gives hope:

example (p q r : ℕ) (h : p ≤ q) (h' : q ≤ r) : p ≤ r :=
begin
  refine le_trans _ _,
  swap,
  tauto,
  tauto
end

This is the kind of goal I hope some "cc for inequalities" would solve

So like this?

import data.nat.basic

meta def tactic.interactive.cc_inequality : tactic unit :=
`[transitivity; tauto]

example (p q r : ℕ) (h : p ≤ q) (h' : q ≤ r) : p ≤ r :=
by cc_inequality

[Johan Commelin]

@Scott Morrison Your first question is exact h1, so I would hope that linarith could do it. The second and third are nasty because they use nat-subtraction. I think we still need a num_cast tactic that would lift it to int, and then linarith could do the job.

[Andrew Ashworth]

Cooper will kill these, if you're willing to use another dependency

[Scott Morrison]

Am I allowed to import cooper into data.nat.basic? :-)

[Scott Morrison]

Thanks for the suggestion, I will try out cooper!

[Rob Lewis]

linarith will not prove any of those. Think of it as a tactic for linear rational inequalities. If a goal over int is still provable when you replace int with rat, it will still work. Inequalities over nat are cast to inequalities over int, with extra assumptions that all atoms are nonnegative. Applications of nat subtraction are treated as atoms.

[Rob Lewis]

The first one isn't true in a dense order. The second ones involve properties of nat subtraction beyond nonnegativity.

[Rob Lewis]

cooper isn't in mathlib, it's in Seul's repository. Use it, of course, but incorporating it into mathlib is a bigger discussion.

[Bryan Gin-ge Chen]

Would it be possible to edit linarith so that it automatically knows that variables coerced from nat are nonnegative? Compare:

example (a : ℚ) (h:a≥0) : (3:ℚ)/4 ≤ (4:ℚ) + a := by linarith --works
example (a : ℕ) : (3:ℚ)/4 ≤ (4:ℚ) + ↑a := by linarith -- fails
example (a : ℕ) (h:a≥0) : (3:ℚ)/4 ≤ (4:ℚ) + ↑a := by linarith -- even this fails

[Rob Lewis]

linarith isn't a smart tactic. It does one thing (linear rational arithmetic) very well, and by coincidence, sometimes it can do things with nat and int. In your second example, it doesn't know any connection between a and ↑a, and why should it? Instead of a cast, that could be abs, or square, or any nonnegative function. In the very special case when it sees an inequality over nat, it will cast it to int and add the nonnegativity hypotheses. But it won't go digging through the input looking for things it can learn are nonnegative. That's a kind of preprocessing that can be done separately.

[Rob Lewis]

The third example is a little different. It sees the a >= 0 hypothesis, and casts it to int. But the overall problem is in rat.

[Rob Lewis]

In general, there's no well-defined type of the "overall problem," since you could have hypotheses over many different types.

[Rob Lewis]

It could try to guess what type to cast to, or it could cast to every type that appears. This wouldn't be so unreasonable.

[Bryan Gin-ge Chen]

Thanks for explaining! As always, there was a lot of complexity lurking here that I didn't appreciate.

[Sebastien Gouezel]

Linarith just failed me on a goal that seemed to me to be in its range of applicability. I know that it is not supposed to be extended further, but still I wanted to mention it here:

lemma zou (x : ℚ) (h : ¬ (x < 0)) (h' : ¬ (x = 0)) (h'' : ¬(0 < x)) : false :=
begin
  linarith, -- fails
end

[Sebastien Gouezel]

By the way, hint is not really happy with this lemma, as it complains

Cannot reify expr :
false

[Kenny Lau]

it might be note-worthy that apply h', linarith succeeds

[Kevin Buzzard]

What happens if you pushneg all the nots away first?

[Rob Lewis]

If there are n disequalities in the context then linarith would have to run 2^n times. "Not equals" isn't analogous to "not less than" in this context.

[Rob Lewis]

The same applies for = in a goal, except there can be at most one there.

[Scott Morrison]

Sebastien Gouezel said:

By the way, hint is not really happy with this lemma, as it complains

Cannot reify expr :
false

It seems that it is omega which prints this error message.

[Scott Morrison]

import tactic.omega

lemma zou (x : ℚ) (h : ¬ (x < 0)) (h' : ¬ (x = 0)) (h'' : ¬(0 < x)) : false :=
begin
  omega, -- prints "Cannot reify expr : false"
end

[Scott Morrison]

I can see where in omega to turn off printing this message (and just fail silently). Shall we do that?

[Mario Carneiro]

It shouldn't fail silently, it should fail with this as the error message rather than print + fail

[Mario Carneiro]

(it should also be fixed to be able to reify false)

[Paul Rowe]

I'm curious if anything ever happened with this. I have run into this situation plenty of times: the target is false, and omega is strong enough to deduce that the hypotheses are inconsistent. I've been using the following (admittedly very idiosyncratic) pattern to deal with it:

suffices d:1<0, by linarith only [d],
omega

It feels odd every time I do it because there must be a better way, but I haven't found it yet. Also, while linarith will often work in these situations, it's much more expensive than omega which is why I restrict it to deriving false from an obvious inconsistency just to enable omega.

[Jalex Stark]

does it work to revert one of the hypotheses (maybe one that looks like an inequality?) and then call omega? That should be both shorter and faster than your solution with linarith

[Paul Rowe]

Oh that's clever. Yes, it does work on the first example I found. It's certainly way better than invoking linarith but still seems a little odd that omega cannot be applied directly.

[Rob Lewis]

omega has many bugs and this is one of them. Unfortunately the person who wrote it is not available to fix it and it's a project. But linarith should not be slower than omega (when they both work). There are goals that omega should solve in principle that linarith can't.

[Paul Rowe]

I see. Well, I'm glad we at least have omega in the form it's in! My observation of omega being faster than linarith is anecdotal in that I haven't run any unit tests or anything to compare them. All I know is that when I first encountered the issue, my bloated proofs ran much better with omega than with linarith. In any case, I am mostly happy to learn that I am not missing something simple about omega that is obvious to others. Thanks for the replies!

[Rob Lewis]

Sebastien Gouezel said:

Linarith just failed me on a goal that seemed to me to be in its range of applicability. I know that it is not supposed to be extended further, but still I wanted to mention it here:

lemma zou (x : ℚ) (h : ¬ (x < 0)) (h' : ¬ (x = 0)) (h'' : ¬(0 < x)) : false :=
begin
  linarith, -- fails
end

#3786 . I'm not giving in to peer pressure here! Mario needed branching preprocessors for something else, and handling disequality hypotheses was the simplest example of a branching preprocessor I could think of, so it was a good test. Don't go crazy with the new toy.