can't apply simple inequality by `rel`

Stream: new members

[rzeta0]

I'm working on a wider induction exercise but can't seem to apply an inequality. So I've constructed a smaller MWE which also illustrates the problem:

import Mathlib.Tactic

example {n: ℕ} (h: 5 ≤ n): 2^n ≥ 30 := by
  calc
    2^n ≥ 2^5 := by rel [h] -- < -- fails ---
    _ ≥ 30 := by norm_num

The error message is:

rel failed, cannot prove goal by 'substituting' the listed relationships.
The steps which could not be automatically justified were:
1 ≤ 2

I've tried adding hypothesis using have to say 1 ≤ 2 and also tried n ≥ 5 in case the direction matters - all to no avail.

[Kevin Buzzard]

Yes that error is surprising to me. I guess I object to your claim that the inequality is "simple" -- it's not true that $(0.5)^n \geq (0.5)^5$ because $0<0.5<1$ so somehow there is some content there, the content being that $2\geq 1$ as the error says. What surprises me is that explicitly adding this hypothesis to the context does not fix it. My instinct if you just want to work around the bug is to find the lemma which says that under certain hypotheses, x <= y implies a^x <= a^y using apply? or exact?. Indeed, replacing rel [h] by apply? gives the following fix:

import Mathlib.Tactic

example {n: ℕ} (h: 5 ≤ n): 2^n ≥ 30 := by
  have foo : (1 : ℕ) ≤ 2 := by norm_num -- add the relevant fact to the context
  calc
    2^n ≥ 2^5 := by exact Nat.pow_le_pow_of_le_right foo h
    _ ≥ 30 := by norm_num

Notwithstanding the fix, I think this is worth a bug report:

import Mathlib.Tactic

example {n: ℕ} (h: 5 ≤ n): 2^n ≥ 2^5 := by
  have foo : (1 : ℕ) ≤ 2 := by norm_num
  rel [h]
/-
rel failed, cannot prove goal by 'substituting' the listed relationships.
The steps which could not be automatically justified were:
1 ≤ 2
-/

or at least a comment that the error message is confusing.

[rzeta0]

reported on GitHub: https://github.com/leanprover/lean4/issues/6444

[Kevin Buzzard]

That is probably the wrong repo -- I doubt rel is defined in core lean.

[Kevin Buzzard]

Yeah if I ctrl-click on rel it takes me to Mathlib.Tactic.GCongr.Core so this should be a mathlib issue (I would close the Lean 4 issue, they're pretty busy keeping things running over there)

[rzeta0]

ok - I'll see if I can delete it and find the mathlib one

[Kevin Buzzard]

You can just close it no problem

[rzeta0]

closed, new one here: https://github.com/leanprover-community/mathlib4/issues/20232

[Daniel Weber]

This can be resolved by using

macro_rules | `(tactic| gcongr_discharger) => `(tactic| norm_num)

which makes gcongr and rel attempt to use norm_num to solve side goals. This will probably require some adaptation of Mathlib, though. I opened #20234

[Johan Commelin]

cc @Heather Macbeth

[Daniel Weber]

Daniel Weber said:

This can be resolved by using

macro_rules | `(tactic| gcongr_discharger) => `(tactic| norm_num)

which makes gcongr and rel attempt to use norm_num to solve side goals. This will probably require some adaptation of Mathlib, though. I opened #20234

This passes CI now, but the benchmark isn't great