# Zulip Chat Archive

## Stream: new members

### Topic: not allowed to know the names of any theorems

#### Scott Morrison (Feb 27 2019 at 06:25):

Without knowing the names of any lemmas (tactics are allowed), prove

lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 :=

#### Kevin Buzzard (Feb 27 2019 at 06:57):

import tactic.linarith lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := begin change n + 1 ≤ 3 at h₁, -- Rob missed a trick linarith, end

#### Patrick Massot (Feb 27 2019 at 06:58):

We should resume work on the nat case bashing tactic

#### Kevin Buzzard (Feb 27 2019 at 07:01):

lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := begin cases n, cases h₂, cases n, cases h₂ with h₂ h₃, cases h₃, cases h₁ with h₁ h₃, refl, -- the proof cases h₃ with h₁ h₃, cases h₃ with h₁ h₃, cases h₃, end

#### Patrick Massot (Feb 27 2019 at 07:01):

The current state was:

import tactic.interactive open tactic meta def get_nat_ineq : expr → tactic (expr × expr × ℕ) | `(%%val < %%ebound) := prod.mk val <$> (prod.mk ebound <$> eval_expr ℕ ebound) | `(%%val ≤ %%ebound) := prod.mk val <$> (prod.mk ebound <$> nat.succ <$> eval_expr ℕ ebound) | _ := failed namespace tactic.interactive open lean.parser interactive meta def nat_cases (h : parse ident) : tactic unit := focus1 $ do e ← get_local h, ⟨val, ⟨ebound, bound⟩⟩ ← infer_type e >>= get_nat_ineq, expr.local_const _ nval _ _ ← return val, iterate_at_most bound $ do { val ← get_local nval, cases_core val, clear_lst [h], swap }, e ← get_local h, val ← get_local nval, proof ← to_expr ```(absurd %%e (not_lt_of_ge $ nat.le_add_left %%ebound %%val)), tactic.exact proof, goals ← get_goals, set_goals goals.reverse end tactic.interactive example (n : ℕ) (h : n ≤ 4) : n ≤ 10 := begin nat_cases h, do { goals ← get_goals, guard (goals.length = 5) }, all_goals { exact dec_trivial}, end example (n : ℕ) (h : n < 4) : n ≤ 10 := begin nat_cases h, do { goals ← get_goals, guard (goals.length = 4) }, all_goals { exact dec_trivial}, end

but it needed to be extended to handle also lower bounds

#### Patrick Massot (Feb 27 2019 at 07:03):

Remember this is based on code by Kenny

#### Kevin Buzzard (Feb 27 2019 at 08:11):

lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := begin cases h₁ with _ h₁, refl, cases h₁ with _ h₁, revert h₂, exact dec_trivial, cases h₁ with _ h₁, revert h₂, exact dec_trivial, cases h₁, end

Casing on the inequality is quicker than casing on `n`

.

#### Kenny Lau (Feb 27 2019 at 08:16):

import data.nat.basic lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := by revert n; tactic.exact_dec_trivial

#### Johan Commelin (Feb 27 2019 at 08:17):

@Scott Morrison Your challenge was Kenny'd.

#### Kevin Buzzard (Feb 27 2019 at 08:18):

Why is the import necessary?

#### Mario Carneiro (Feb 27 2019 at 08:18):

I assume that's where the decidable instance is

#### Mario Carneiro (Feb 27 2019 at 08:19):

I think `tactic.exact_dec_trivial`

can just be `exact dec_trivial`

#### Mario Carneiro (Feb 27 2019 at 08:19):

unless that counts as "the name of a theorem"

#### Kevin Buzzard (Feb 27 2019 at 08:19):

Well he'd better make some improvements because my first solution is shorter than his :P

#### Kevin Buzzard (Feb 27 2019 at 08:19):

import data.nat.basic import tactic.linarith lemma qux (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := by change n + 1 ≤ 3 at h₁; linarith lemma qux' (n : ℕ) (h₁ : n < 3) (h₂ : n ≥ 2) : n = 2 := by revert n; tactic.exact_dec_trivial

#### Kenny Lau (Feb 27 2019 at 08:20):

but mine is faster

#### Kevin Buzzard (Feb 27 2019 at 08:20):

however my longer solution is faster than yours so I'm beating you all ends up ;-)

#### Kevin Buzzard (Feb 27 2019 at 08:21):

Mario is right though, and now yours is the shortest

#### Mario Carneiro (Feb 27 2019 at 08:23):

these proofs make me weep though, compared to just using `le_antisymm`

#### Kenny Lau (Feb 27 2019 at 08:24):

you can make that a tactic!

#### Mario Carneiro (Feb 27 2019 at 08:24):

`by exact`

#### Patrick Massot (Feb 27 2019 at 08:38):

Again, we should have a complete `nat_cases`

tactic (and `int_cases`

)

#### Scott Morrison (Feb 27 2019 at 10:03):

Okay, I've added the "missing trick" to linarith, PR to follow once I've tested a bit more.

#### Scott Morrison (Feb 27 2019 at 10:03):

I'll see if I can do something with nat_cases, too.

#### Scott Morrison (Feb 27 2019 at 10:12):

https://github.com/leanprover-community/mathlib/pull/769

#### Sebastien Gouezel (Feb 27 2019 at 10:42):

Nice! If you're in a linarith mood, I would like to know if it is easy to add to the context used by linarith the inequalities `lfloor x rfloor <= x`

and `x < lfloor x rfloor + 1`

when `lfloor x rfloor`

appears in the context (or maybe I should do the exercise myself!)

#### Scott Morrison (Feb 27 2019 at 10:51):

I'd guess this isn't too bad. (One could do max and min, too.)

#### Scott Morrison (Feb 27 2019 at 10:52):

My preference would be to basically have a preprocessing step, that inspects hypotheses for these sorts of things appearing inside linear inequalities, and add all the extra lemmas. Then we could add a parsing flag to linarith to ask it to run the preprocessor (or do it by default anyway).

#### Scott Morrison (Feb 27 2019 at 10:53):

I'll add it to my list (I have a whole lot of students just getting started... maybe one of them will be trying it soon) :-) I'd like to think about a nice `nat_cases`

first.

#### Rob Lewis (Feb 27 2019 at 11:10):

I don't want the core `linarith`

tactic to do heuristic instantiation. There's no end to the lemmas that could be applicable. Same deal with unfolding constants, splitting conditionals, etc. A separate tactic that preprocesses for `linarith`

would be fine. But throwing lots of random features into the core tactic makes it unpredictable, slower, and harder to maintain.

#### Sebastien Gouezel (Feb 27 2019 at 15:34):

What about `linarith_ext`

(or something like that) for the tactic extended by a preparser massaging suitably the assumptions (maybe the nat and int preprocessing just commited by Scott would fit in this preprocessing step, for instance), and `linarith`

for the original unchanged robust tactic? And maybe later if one realizes that everyone uses the extended version and that the speed difference is not huge, rename them to `linarith`

and `linarith_core`

respectively?

#### Andrew Ashworth (Feb 27 2019 at 16:51):

hmm, wasn't this sort of thing what simp sets were for? I wonder what happened to that project

#### Rob Lewis (Feb 27 2019 at 20:21):

I want to keep the behavior of `linarith`

predictable. There's a very well-defined problem that it solves: `linarith`

will (or should) prove all provable statements in the theory of linear arithmetic over the rationals. The tactic is finished when it does this. It happens that some problems over `int`

and `nat`

can be solved by the same method with minimal preprocessing, and it doesn't hurt to try the very simple and obvious stuff, like what Scott added. But the step up from rational arithmetic to actual integer arithmetic is huge, it's a much harder problem. Adding more and more gadgets to the current one to make it do more on integers will lead to pain. The gadgets will have bugs, they'll interact in unexpected ways, people will keep wondering why a works but b doesn't. I've already fixed bad interactions in the nat/int preprocessing and there's not much there. And in the end, it will never be a replacement for an actual integer arithmetic tool.

Making it aware of certain constants is the same deal. Yeah, there are natural inequalities about floor that we all know. And ceiling, and abs, and max and min, and log and exp, and sin.... This is all a special case of heuristic lemma instantiation. You have terms, you have a library of universally quantified facts, which facts do you instantiate with which terms to get something useful? You can hardcode a few things into a preprocessing loop and call it a day. But there's a systematic way to do this kind of thing (that's partially implemented in Lean's SMT mode, actually), and it really has nothing to do with linear arithmetic. Trying to approximate it will lead to infinite feature requests, so prepare yourself.

#### Rob Lewis (Feb 27 2019 at 20:22):

Andrew, Sebastien's question has nothing to do with simplifying, he wants to add extra inequalities to the context based on the constants that appear there already.

#### Patrick Massot (Feb 27 2019 at 20:34):

We need a mathlib FAQ where Rob can paste this answer once and for all (I'm sure he wrote it at least five times already, although I'm clearly among people who would like linarith to close all their goals).

#### Bryan Gin-ge Chen (Feb 27 2019 at 21:28):

Maybe some portion of this can be added to the tactic docs.

Last updated: May 12 2021 at 23:13 UTC