Zulip Chat Archive

Stream: new members

Topic: not allowed to know the names of any theorems


view this post on Zulip 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 :=

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 27 2019 at 06:58):

We should resume work on the nat case bashing tactic

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 27 2019 at 07:03):

Remember this is based on code by Kenny

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 27 2019 at 08:17):

@Scott Morrison Your challenge was Kenny'd.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 08:18):

Why is the import necessary?

view this post on Zulip Mario Carneiro (Feb 27 2019 at 08:18):

I assume that's where the decidable instance is

view this post on Zulip Mario Carneiro (Feb 27 2019 at 08:19):

I think tactic.exact_dec_trivial can just be exact dec_trivial

view this post on Zulip Mario Carneiro (Feb 27 2019 at 08:19):

unless that counts as "the name of a theorem"

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 08:19):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 27 2019 at 08:20):

but mine is faster

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 08:20):

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

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 08:21):

Mario is right though, and now yours is the shortest

view this post on Zulip Mario Carneiro (Feb 27 2019 at 08:23):

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

view this post on Zulip Kenny Lau (Feb 27 2019 at 08:24):

you can make that a tactic!

view this post on Zulip Mario Carneiro (Feb 27 2019 at 08:24):

by exact

view this post on Zulip Patrick Massot (Feb 27 2019 at 08:38):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 27 2019 at 10:03):

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

view this post on Zulip Scott Morrison (Feb 27 2019 at 10:12):

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

view this post on Zulip 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!)

view this post on Zulip Scott Morrison (Feb 27 2019 at 10:51):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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