Zulip Chat Archive

Stream: general

Topic: linarith


view this post on Zulip Johan Commelin (Nov 21 2018 at 08:53):

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

view this post on Zulip Kenny Lau (Nov 21 2018 at 09:00):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:05):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:06):

@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

view this post on Zulip Rob Lewis (Nov 21 2018 at 09:07):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:08):

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

view this post on Zulip Kenny Lau (Nov 21 2018 at 09:09):

maybe stop (over)relying on tactics

view this post on Zulip Rob Lewis (Nov 21 2018 at 09:10):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:11):

that works

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:12):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 09:14):

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.

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:18):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 09:18):

Or apply ha; linarith.

view this post on Zulip Patrick Massot (Nov 21 2018 at 09:18):

indeed

view this post on Zulip Sebastien Gouezel (Nov 21 2018 at 09:49):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 10:36):

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.

view this post on Zulip Rob Lewis (Nov 21 2018 at 10:37):

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

view this post on Zulip Sebastien Gouezel (Nov 21 2018 at 10:45):

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

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:34):

@Rob Lewis Cool! Thanks a lot.

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:35):

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

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:36):

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?

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:37):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 11:40):

@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

view this post on Zulip Rob Lewis (Nov 21 2018 at 11:41):

@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.

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:42):

Ok, thanks, will do.

view this post on Zulip Johan Commelin (Nov 21 2018 at 11:47):

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

view this post on Zulip Johan Commelin (Nov 21 2018 at 12:00):

@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.

view this post on Zulip Johan Commelin (Nov 21 2018 at 12:00):

Sorry, I should paste context...

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 12:00):

So these are nats?

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 12:03):

What is the argument in maths?

view this post on Zulip Rob Lewis (Nov 21 2018 at 12:03):

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

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 12:03):

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

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 12:03):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 12:04):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 12:04):

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

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 12:05):

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

view this post on Zulip Kenny Lau (Nov 21 2018 at 12:05):

@Johan Commelin there must be such a function in mathlib

view this post on Zulip Kenny Lau (Nov 21 2018 at 12:06):

(or not)

view this post on Zulip Kenny Lau (Nov 21 2018 at 12:06):

(yes it’s decidable)

view this post on Zulip Rob Lewis (Nov 21 2018 at 12:07):

@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.

view this post on Zulip Johan Commelin (Nov 21 2018 at 12:09):

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

view this post on Zulip Johan Commelin (Nov 21 2018 at 12:15):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 16:48):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 16:54):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 16:56):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 16:57):

search for "does nothing" in this thread

view this post on Zulip Simon Hudon (Nov 21 2018 at 17:23):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 17:25):

I would expect it to close the goal

view this post on Zulip Simon Hudon (Nov 21 2018 at 18:23):

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.

view this post on Zulip Simon Hudon (Nov 21 2018 at 18:23):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 18:25):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 19:18):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 19:19):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 19:19):

Except tfae doesn't work :sad:

view this post on Zulip Patrick Massot (Nov 21 2018 at 19:20):

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

view this post on Zulip Patrick Massot (Nov 21 2018 at 19:21):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 19:23):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 19:25):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 20:36):

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

view this post on Zulip Chris Hughes (Nov 21 2018 at 20:38):

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

view this post on Zulip Chris Hughes (Nov 21 2018 at 20:39):

But I think linarith does those.

view this post on Zulip Rob Lewis (Nov 21 2018 at 20:41):

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

view this post on Zulip Chris Hughes (Nov 21 2018 at 20:45):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 20:59):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 20:59):

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

view this post on Zulip Simon Hudon (Nov 21 2018 at 21:03):

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.

view this post on Zulip Simon Hudon (Nov 21 2018 at 21:04):

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

view this post on Zulip Rob Lewis (Nov 21 2018 at 21:06):

Ah, sure. Sounds reasonable enough.

view this post on Zulip Patrick Massot (Nov 21 2018 at 22:16):

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

view this post on Zulip Kenny Lau (Nov 22 2018 at 15:30):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 17:24):

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

view this post on Zulip Kenny Lau (Nov 22 2018 at 18:39):

@Johan Commelin fin.succ_above

view this post on Zulip Johan Commelin (Nov 22 2018 at 19:07):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 19:08):

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

view this post on Zulip Kenny Lau (Nov 22 2018 at 19:29):

never mind, ignore me

view this post on Zulip Scott Morrison (Nov 23 2018 at 23:59):

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)

view this post on Zulip Kenny Lau (Nov 24 2018 at 01:16):

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

view this post on Zulip Johan Commelin (Nov 24 2018 at 05:33):

@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.

view this post on Zulip Andrew Ashworth (Nov 24 2018 at 06:27):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 06:42):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 06:42):

Thanks for the suggestion, I will try out cooper!

view this post on Zulip Rob Lewis (Nov 24 2018 at 09:54):

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.

view this post on Zulip Rob Lewis (Nov 24 2018 at 09:55):

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

view this post on Zulip Rob Lewis (Nov 24 2018 at 09:56):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 24 2018 at 10:13):

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

example (a : ) (h:a0) : (3:)/4  (4:) + a := by linarith --works
example (a : ) : (3:)/4  (4:) + a := by linarith -- fails
example (a : ) (h:a0) : (3:)/4  (4:) + a := by linarith -- even this fails

view this post on Zulip Rob Lewis (Nov 24 2018 at 11:07):

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.

view this post on Zulip Rob Lewis (Nov 24 2018 at 11:08):

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.

view this post on Zulip Rob Lewis (Nov 24 2018 at 11:08):

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

view this post on Zulip Rob Lewis (Nov 24 2018 at 11:09):

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.

view this post on Zulip Bryan Gin-ge Chen (Nov 24 2018 at 16:24):

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

view this post on Zulip Sebastien Gouezel (May 29 2020 at 16:32):

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

view this post on Zulip Sebastien Gouezel (May 29 2020 at 16:33):

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

Cannot reify expr :
false

view this post on Zulip Kenny Lau (May 29 2020 at 16:35):

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

view this post on Zulip Kevin Buzzard (May 29 2020 at 17:18):

What happens if you pushneg all the nots away first?

view this post on Zulip Rob Lewis (May 29 2020 at 18:31):

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.

view this post on Zulip Rob Lewis (May 29 2020 at 18:32):

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

view this post on Zulip Scott Morrison (May 30 2020 at 03:35):

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.

view this post on Zulip Scott Morrison (May 30 2020 at 03:36):

import tactic.omega

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

view this post on Zulip Scott Morrison (May 30 2020 at 03:38):

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

view this post on Zulip Mario Carneiro (May 30 2020 at 03:50):

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

view this post on Zulip Mario Carneiro (May 30 2020 at 03:51):

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

view this post on Zulip Paul Rowe (Jul 23 2020 at 16:29):

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.

view this post on Zulip Jalex Stark (Jul 23 2020 at 16:33):

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

view this post on Zulip Paul Rowe (Jul 23 2020 at 16:36):

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.

view this post on Zulip Rob Lewis (Jul 23 2020 at 16:43):

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.

view this post on Zulip Paul Rowe (Jul 23 2020 at 16:50):

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!

view this post on Zulip Rob Lewis (Aug 15 2020 at 12:00):

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.


Last updated: May 06 2021 at 21:09 UTC