## 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