not allowed to know the names of any theorems

Stream: new members

[Scott Morrison]

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

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

[Kevin Buzzard]

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]

We should resume work on the nat case bashing tactic

[Kevin Buzzard]

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]

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]

Remember this is based on code by Kenny

[Kevin Buzzard]

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]

import data.nat.basic

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

[Johan Commelin]

@Scott Morrison Your challenge was Kenny'd.

[Kevin Buzzard]

Why is the import necessary?

[Mario Carneiro]

I assume that's where the decidable instance is

[Mario Carneiro]

I think tactic.exact_dec_trivial can just be exact dec_trivial

[Mario Carneiro]

unless that counts as "the name of a theorem"

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

but mine is faster

[Kevin Buzzard]

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

[Kevin Buzzard]

Mario is right though, and now yours is the shortest

[Mario Carneiro]

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

[Kenny Lau]

you can make that a tactic!

[Mario Carneiro]

by exact

[Patrick Massot]

Again, we should have a complete nat_cases tactic (and int_cases)

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Sebastien Gouezel]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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

[Rob Lewis]

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]

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]

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]

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