Proving false based on several inequalities automatically

Stream: new members

[Bob Rubbens]

I've got a few proof goals that all have the following structure:

image.png

In this case I can combine h4 and hss_oe and h1 to get False. Is there a tactic that does this automatically? The types for self.start etc. are all LinearOrder from Mathlib. I know most proof goals have a simple solution like this, because the inequalities arise from intervals that I know overlap. I just would like to avoid having to write out all 8 cases explicitly... Grind, aesop and try? unfortunately have no suggestions.

[A.]

Have you tried linarith?

[Robin Arnez]

I would've guessed order, grind or omega

[Markus Himmel]

linarith, order, grind and omega all solve this on a sufficiently recent Lean/mathlib (for example the 4.23.0 stable release)

[Darij Grinberg]

I have myself been doing it with linarith only [the relevant ineqs], which seems more human-readable and stable to me

[Bob Rubbens]

Thanks, omega did the trick for my 8 proof goals!

Some more questions if that's okay:

• Why doesn't try? use linarith, order, or omega, but does use grind?
• In my repro, grind does the job:

theorem repro
  (self other : Interval ℤ)
  (x : ℤ)
  (h1 : self.start ≤ x)
  (h2 : x < self.end)
  (h3 : other.start ≤ x)
  (h4 : x < other.end)
  (hos_se : other.start < self.end)
  (hos_ss : other.start < self.start)
  (hoe_hse : other.end < self.end)
:
  self.start ≤ other.start ∧ other.start < self.end ∨
    self.start < other.end ∧ other.end ≤ self.end ∨
      self.start < other.end ∧ other.end < self.end ∨
        other.start ≤ self.start ∧ self.start ≤ self.end ∧ self.end < other.end
:= by
  grind

But in a deeper context, with exactly the same proof obligation as far as I can tell (I copy-pasted it enirely), it fails on the same proof obligation:

image.png

Here I'm just focusing the first of eight proof goals. Does grind get confused about those other proof goals somehow, or does it adjust its search parameters when used more deeply in a proof? Accoridng to my lean-toolchain file I'm on version leanprover/lean4:v4.24.0-rc1.

[Bob Rubbens]

FWIW, if I replace grind there with omega, the proof is finished.

[Robin Arnez]

Well... grind (or specifically cutsat) is supposed to replace omega for regular use

[Robin Arnez]

It would be helpful if you could make an #mwe

[Bob Rubbens]

It's not super small but I'm not too sure how to make it much smaller. But it might be enough to illustrate the point:

import Mathlib.Order.Defs.LinearOrder
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Nat.Basic
import Aesop
import Mathlib.Tactic

structure Interval α [LinearOrder α] where
  mk :: (start : α) («end» : α) (non_empty : start < «end»)

def contains [LinearOrder α] (i : Interval α) (a : α) : Bool :=
  i.start ≤ a ∧ a < i.«end»

def overlaps_spec [LinearOrder α] (self : Interval α) (other : Interval α) : Prop :=
  ∃a, (contains self a) ∧ (contains other a)

def overlaps_straightforward (self : Interval Int) (other : Interval Int) : Bool :=
  self.start ≤ other.start ∧ other.start < self.«end» ∨
  self.start < other.«end» ∧ other.«end» ≤ self.«end» ∨
  self.start < other.«end» ∧ other.«end» ≤ other.«end» ∧ other.«end» < self.«end» ∨
  other.start ≤ self.start ∧ self.start ≤ self.«end» ∧ self.«end» < other.«end»

theorem overlaps_straightforward_ok (self other) :
  overlaps_spec self other → overlaps_straightforward self other
:= by
  simp [overlaps_spec, overlaps_straightforward, contains]
  intro x h1 h2 h3 h4
  -- grind
  omega

My lean version is leanprover/lean4:v4.24.0-rc1. I can also post my lake-manifest.json if necessary.

[Vlad Tsyrklevich]

The pretty printer hides some of the complex reality, you can see the real terms using set_option pp.all true. It's harder to interpret, but it shows that actually the states are not the exact same, the instances in the LE of the hypotheses differ. If you specialize contains/overlap_spec to use Int instead of an arbitary \a, the hypotheses are then equal and grind works. e.g. using

def contains (i : Interval Int) (a : Int) : Bool :=
  i.start ≤ a ∧ a < i.«end»

def overlaps_spec (self : Interval Int) (other : Interval Int) : Prop :=
  ∃a, (contains self a) ∧ (contains other a)

[Bob Rubbens]

Oh, I see!

I would've hoped that changing overlaps_straightforward to use an \alpha would make it work, but in that case neither omega or grind can solve it. :( I guess there's something about Int that makes it a little bit easier to solve...?

[Vlad Tsyrklevich]

I'm not sure what you mean about changing them to not use \a, an example is easier to understand than a description. I'm not familiar with grind internals, but I wouldn't say Int 'is easier', just that grind appears to be missing some logic to look through that particular LE.

[Bob Rubbens]

I mean, just using a LinearOrder \alpha everywhere, instead of in only one place and Int everywhere else. E.g.:

structure Interval α [LinearOrder α] where
  mk :: (start : α) («end» : α) (non_empty : start < «end»)

def contains [LinearOrder α] (i : Interval α) (a : α) : Bool :=
  i.start ≤ a ∧ a < i.«end»

def overlaps_spec [LinearOrder α] (self : Interval α) (other : Interval α) : Prop :=
  ∃a, (contains self a) ∧ (contains other a)

def overlaps_straightforward [LinearOrder α] (self : Interval α) (other : Interval α) : Bool :=
  self.start ≤ other.start ∧ other.start < self.«end» ∨
  self.start < other.«end» ∧ other.«end» ≤ self.«end» ∨
  self.start < other.«end» ∧ other.«end» ≤ other.«end» ∧ other.«end» < self.«end» ∨
  other.start ≤ self.start ∧ self.start ≤ self.«end» ∧ self.«end» < other.«end»

set_option pp.all true

theorem overlaps_straightforward_ok [LinearOrder α] (self other : Interval α) :
  overlaps_spec self other → overlaps_straightforward self other
:= by
  simp [overlaps_spec, overlaps_straightforward, contains]
  intro x h1 h2 h3 h4
  omega

[Vlad Tsyrklevich]

omega is specialized to Nat/Int. I believe grind also has specialized logic though there has been talk of adding the ability to work with orders. There is a general order (docs#Mathlib.Tactic.Order) tactic, but it does not seem to account for conjunctions/disjunctions, e.g. to use it I had to do

def overlaps_straightforward [LinearOrder α] (self : Interval α) (other : Interval α) : Bool :=
  self.start ≤ other.start ∧ other.start < self.«end» ∨
  self.start < other.«end» ∧ other.«end» ≤ self.«end» ∨
  other.start ≤ self.start ∧ self.«end» < other.«end»

theorem overlaps_straightforward_ok [LinearOrder α] (self other : Interval α) :
  overlaps_spec self other → overlaps_straightforward self other
:= by
  simp [overlaps_spec, overlaps_straightforward, contains]
  intro x h1 h2 h3 h4
  have n1 := other.non_empty
  have n2 := self.non_empty
  rcases lt_trichotomy self.start other.start with h' | h' | h'
  · rcases lt_trichotomy self.end other.end with h'' | h'' | h''
    · left
      constructor <;> order
    · simp_all
    · right; left
      constructor <;> order
  · simp_all
  · rcases lt_trichotomy self.end other.end with h'' | h'' | h''
    · right; right;
      constructor <;> order
    · simp_all
    · right; left
      constructor <;> order

That's unfortunate since it does seem that order could actually derive the necessary facts.