linarith tactic understanding

Stream: new members

[Ayush Agrawal]

Hi guys! I wanted to understand the code of high level tactics such as linarith, simp etc. at a very basic level. I am facing a lot of difficulty as I am new to functional paradigm and there seems to be a lot of dependencies (or various functions) pertaining to a single tactic. Can someone please guide me through this? by taking example of a linarith tactic?

[Scott Morrison]

@Ayush Agrawal, have you read https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html yet?

[Ayush Agrawal]

Oh thanks for the resource! I didn't read this.

[Scott Morrison]

You accidentally picked one of the better documented tactics. :-) If you want to know what linarith is actually doing (rather than just how it is implemented) you'll need to read up on Fourier-Motzkin elimination. But there are many good sources. (From memory wikipedia is okay. :-)

[Ayush Agrawal]

I saw that the linarith basically looks for the 0 < 0 contradiction for observing the unsatisfiability. Is it the case that it is not able to check for the unsatisfiability when all the inequalities (including the one formed by negation ) are \< = ? Because I think that if it does not contain atleast one inequality as < , it cannot conclude that the linear combination of these hypotheses ( search for 0) should be < 0. I hope I was able to explain my doubt, please let me know if I am wrong..

[Yaël Dillies]

Well, it can generate some. Typically, you get a < b from a + 1 ≤ b

[Ayush Agrawal]

And if it not able to generate such kind? Is there some other treatment it uses?

[Yaël Dillies]

If it can't generate any contradiction, it fails. I don't know much more unfortunately... but you should really look up Fourier-Motzkin.

[Ayush Agrawal]

I was reading the mathlib documentation of the linarith tactic https://leanprover-community.github.io/mathlib_docs/tactic/linarith/elimination.html (after understanding the FM elimination). Although I am not understanding a lot of stuff going on (which I'll post gradually), I wanted to understand this line - "Any comparison whose history is not minimal is redundant, and need not be included in the new set of comparisons. elimed_ge : ℕ is a natural number such that all variables with index ≥ elimed_ge have been removed from the system." mentioned under a meta function meta def linarith.pcomp.maybe_minimal (c : linarith.pcomp) (elimed_ge : ℕ) : bool. I think this is related to some maths concept I am not familiar with. Can anyone please help in this?

[Mario Carneiro]

The maybe_minimal function references theorem 7 of http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51.493&rep=rep1&type=pdf ; I would guess that the "minimal history" terminology is coming from that paper

[Mario Carneiro]

Although you should read the paper (and possibly its citations...) to see the whole story, I believe the basic idea is that a non-minimal inequality is dominated by a combination of minimal inequalities, so it can be removed from the system without sacrificing completeness. From an implementation standpoint it's just a heuristic, and dropping hypotheses is easy to do and obviously correct (which is the only thing that matters for a tactic implementation, completeness is just icing on the cake)

[Ayush Agrawal]

I see, thanks for pointing out the paper @Mario Carneiro . what do u mean by non-minimal inequality ( < , <= ?)

[Mario Carneiro]

I think it is something like, if you know $a \le 2$ and $b \le 1$ then $a + b \le 4$ is not helpful

[Mario Carneiro]

But the terminology is from the paper. There are lots of examples in the paper that talk about what it means for a constraint to be minimal, and I don't have that much insight into the notion

[Ayush Agrawal]

Thanks Mario! I'll look into it :)