Limitations of bound tactic

Stream: new members

[Toby Cathcart Burn]

I was surprised to find that the boundtactic does not prove the following:

lemma lem {x : ℝ }  (h : 5 / 2 < 2 + x) : 1<2*x := by
  -- bound
  linarith

linarith works, but this means that more complex statements such as 5 / 2 < 2 + x ↔ 1<2*x take more work to prove than I'd hoped. Is there a different tactic I could use, or a way to modify bound?

[Vasilii Nesterov]

bound uses recursion on the expressions structure applying simple forward rules, like a < b -> a + c < b + c and can't reason about numerical expressions.

What's the problem with using linarith instead? 5 / 2 < 2 + x ↔ 1<2*x can be proved by it like this:

import Mathlib

example {x : ℝ} : 5 / 2 < 2 + x ↔ 1<2*x := by
  constructor <;> (intro; linarith)

[Toby Cathcart Burn]

https://github.com/leanprover-community/mathlib4/blob/658f45e58d91b0fae574e3d6f6adf63ff72390ba/Mathlib/Tactic/Bound.lean#L86 made me think that bound was supposed to be able to handle whatever linarith could.

Vasilii Nesterov said:

What's the problem with using linarith instead?

The whole thing I'd hoped to prove with just a bound was:

lemma lem2 {x y : ℝ } :
  ((3 < x - y + 4 ∧ x < y) ∧ 0 < y + x ∧ y + x < 1) ∧ (0 < x ∧ 4 + x < 4.5) ∧ 3 / 2 < 1 + y ∧ 1 + y < 2 ↔
  0 < x ∧ 1 < 2 * y ∧ 2 * x + (2 * y - 1) < 1 := by
  apply Iff.intro
  intro h
  and_intros
  bound
  linarith
  bound
  bound

and 7 other very similar statements. Seeing the unhelpful things shown by bound when it fails and needing to look at the structure of the statement is much more work than an automated tactic solving it (the statement arises from something geometrically obvious which is why I've got to that statement without thinking about the syntax or having written anything similar on paper).
The first order theory of linear arithmetic over reals is decidable, so it would be nice if I didn't have to think about any of the details (getting a firm "no" quickly when I've made a mistake in definitions and I'm trying to prove a falsehood would also be very nice). Do you know how I could go about writing a tactic that would automate these proofs reliably?

[Kenny Lau]

Toby Cathcart Burn said:

The first order theory of linear arithmetic over reals is decidable

with rational coefficients I'm assuming?

[Toby Cathcart Burn]

Kenny Lau said:

with rational coefficients I'm assuming?

Yep (I think integer coefficients give an equally expressive language).

[Kenny Lau]

so if we have a tactic that decides the FOT of LA over R with Q-coeff, what should it do if it sees Real.sqrt 2 as a coefficient?

[Toby Cathcart Burn]

Let the user know that the tactic can't solve it.

Possibly after seeing if it can still prove the desired statement when what it sees as an unexaminable real gets replaced by a universally quantified fresh variable.

[Vasilii Nesterov]

Toby Cathcart Burn said:

https://github.com/leanprover-community/mathlib4/blob/658f45e58d91b0fae574e3d6f6adf63ff72390ba/Mathlib/Tactic/Bound.lean#L86 made me think that bound was supposed to be able to handle whatever linarith could.

Vasilii Nesterov said:

What's the problem with using linarith instead?

The whole thing I'd hoped to prove with just a bound was:

lemma lem2 {x y : ℝ } :
  ((3 < x - y + 4 ∧ x < y) ∧ 0 < y + x ∧ y + x < 1) ∧ (0 < x ∧ 4 + x < 4.5) ∧ 3 / 2 < 1 + y ∧ 1 + y < 2 ↔
  0 < x ∧ 1 < 2 * y ∧ 2 * x + (2 * y - 1) < 1 := by
  apply Iff.intro
  intro h
  and_intros
  bound
  linarith
  bound
  bound

and 7 other very similar statements.

This is still can be done by linarith (plus splitting conjuctions):

import Mathlib

lemma lem2 {x y : ℝ} :
    ((3 < x - y + 4 ∧ x < y) ∧ 0 < y + x ∧ y + x < 1) ∧ (0 < x ∧ 4 + x < 4.5) ∧ 3 / 2 < 1 + y ∧ 1 + y < 2 ↔
    0 < x ∧ 1 < 2 * y ∧ 2 * x + (2 * y - 1) < 1 := by
  constructor <;> (intro; constructorm* _ ∧ _ <;> linarith)

[Vasilii Nesterov]

And linarith is exactly the tactic for linear arithmetic over reals (over any linearly ordered commutative ring, to be precise). It's not a "true" decision procedure, because it ignores disjunctions in the context, conjunctions in the goal, etc. But in practice you can do rcases against disjunctions you need to split and constructor* ∧ in cases like the above. It's harder to teach it about quantifiers, but the use cases when this is needed are very rare.

[Toby Cathcart Burn]

@Vasilii Nesterov
Thanks for giving me this info. I still feel like I should be able to get the computer to figure out these details for me. bound seems like it's trying to do that, but it's unreliability is annoying.
Also, the step before I reached the statement of lem2 involved dealing with some quantifiers. If they could be handled automatically, it would have saved me a lot of time.

[Vasilii Nesterov]

Can you, please, post the original problem with quantifiers? The main problem with supporting them is that it would lead to a quick exponential blow-up.

[Toby Cathcart Burn]

@Vasilii Nesterov
Here's the statement with quantifiers, and the step before quantifiers were made explicit, with my preexisting proofs (modified by your answers). It's not the 'original' problem, which involves a number of definitions and is part of a larger proof, and almost certainly could have been set up better by someone more familiar with lean.

lemma lemq {x y:ℝ}: (∃ a b, ((3 < a ∧ a < 4) ∧ 0 < b ∧ b < 1) ∧ (a + b + 4) * 0.5 = 4 + x ∧ (b - a + 6) * 0.5 = 1 + y) ∧
    (0 < x ∧ 4 + x < 4.5) ∧ 3 / 2 < 1 + y ∧ 1 + y < 2 ↔
      ∃ a b, (0 < a ∧ 0 < b ∧ a + b < 1) ∧ 2⁻¹ * a = x ∧ 2⁻¹ * b + 2⁻¹ = y
  := by
    have h (a b : ℝ) :(a + b + 4) * 0.5 = 4 + x ∧ (b - a + 6) * 0.5 = 1 + y
      ↔ a = (x-y) + 4 ∧ b = y + x
    := by
      bound
    have h' (a b : ℝ ) : 2⁻¹ * a  = x ∧ 2⁻¹ * b+ 2⁻¹ = y ↔ a = 2*x ∧ b = 2*y - 1 := by
      bound
    simp [h,h']
    apply Iff.intro <;>
      (intro
       and_intros <;> linarith)

open Set -- for Set.Ioo

lemma lem3 : (fun x ↦ (4, 1) + x) ⁻¹' ((fun a ↦ ((a.1 + a.2 + 4) * 0.5, (a.2 - a.1 + 6) * 0.5)) '' Ioo 3 4 ×ˢ Ioo 0 1) ∩
    (fun x ↦ (4, 1) + x) ⁻¹' Ioo (4:ℝ) (4.5:ℝ) ×ˢ Ioo (3 / 2 :ℝ ) (2:ℝ) =
  (fun (a:ℝ×ℝ ) ↦ (2:ℝ)⁻¹ • a + (0, 2⁻¹)) '' {(x, y) | 0 < x ∧ 0 < y ∧ x + y < 1}
   := by
   ext ⟨x,y⟩
   simp
   exact lemq