Nat.pred_le_pred

Stream: mathlib4

[Moritz Firsching]

I am encountering the following:

import Mathlib

lemma Nat.sub_one_le_sub_one {n m : ℕ} : n ≤ m → n - 1 ≤ m - 1 := fun h => Nat.pred_le_pred h

theorem works (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   calc 1 < 2^2 - 1 := by norm_num
        _  ≤ 2^p - 1 := Nat.sub_one_le_sub_one <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h

theorem does_not_work (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   calc 1 < 2^2 - 1 := by norm_num
        _  ≤ 2^p - 1 := Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h
/-
type mismatch
  Nat.pred_le_pred (Nat.pow_le_pow_of_le_right Nat.zero_lt_two (Nat.Prime.two_le h))
has type
  (2 ^ 2).pred ≤ (2 ^ p).pred : Prop
but is expected to have type
  2 ^ 2 - 1 ≤ 2 ^ p - 1 : Prop
-/

I would have expected Nat.pred_le_pred to also work in the second proof. I didn't manage to trigger this outside of the calc tactic. Does this mean we should maybe add Nat.sub_one_le_sub_one in addition to Nat.pred_le_pred?

[Ralf Stephan]

I also get the error outside calc:

import Mathlib
set_option autoImplicit false

theorem does_not_work (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   have : 2^2 - 1 ≤ 2^p - 1 := Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h

and it goes away with exact (leaving the goal ⊢ 1 < 2 ^ p - 1

theorem does_work (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   have : 2^2 - 1 ≤ 2^p - 1 := by
     exact Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h

[Ralf Stephan]

(deleted)

[Mitchell Lee]

What about docs#Nat.sub_le_sub_right ?

[Mitchell Lee]

I don't know why Nat.pred_le_pred works if you use exact, but I think it's probably best not to use it anyway.

[Ralf Stephan]

I think it's because exact has the conversion pred to/from minus 1 in its repertoir. And sometimes you don't have sub lemmata, so you have to do with the pred ones. But not here, right.

[Kyle Miller]

Just in case you think it's exact itself, Nat.pred n and n - 1 are definitionally equal:

example (n : Nat) : n.pred = n - 1 := rfl

(I'm actually a bit surprised that they are!)

[Damiano Testa]

I suspect that the issue is that Sub is a function of 2 arguments, while Pred is a function of 1 and this is confusing Lean at some point.

[Kyle Miller]

I think it would be good not to rely on n.pred being defeq to n - 1 and to have analogues like Nat.sub_one_le_sub_one.

Does Nat.pred need to exist? Is there a use of Nat.pred that can't be served by (· - 1)?

[Kevin Buzzard]

In NNG it exists to prove succ_inj (it's a one-sided inverse for succ) although in NNG pred 0 = 37.

[Mitchell Lee]

I agree that it is good not to use Nat.pred in mathematics, but I don't think there should be a theorem Nat.sub_one_le_sub_one because there's already docs#Nat.sub_le_sub_right.

[Moritz Firsching]

Why don't we have both?

[Mitchell Lee]

There's nothing special about subtracting the number 1 specifically.

[Damiano Testa]

While I agree that mathematically there is not much special about subtracting 1 or some other number, in Lean there may be a difference.

In general, numerals may get a different treatment than variables and among numerals, 0 and 1 are further special-cased. Also, there is an docs#Nat.atLeastTwo typeclass for dealing "with the rest"!

[Moritz Firsching]

I guess @Mitchell Lee has a point, at least we don't have add_one_eq_add_one, while we do have succ_eq_succ.

[Damiano Testa]

(Note that I am not arguing in favour of Nat.pred, I am simply pointing out that the numerals 0 and 1 may be a little more special than others.)

[Kim Morrison]

Historically the Nat API liked succ more than does now. This is still reflected in naming and the appearances or otherwise of lemmas, bit I hope further cleanup will continue.

[Kim Morrison]

I haven't looked recently at how pred is used in the lean4 repo, but generally I'm in favour of using it less when n-1 suffices.

[Kyle Miller]

I see, I should have looked at the definition of docs#Nat.sub before being surprised about the defeq. It's defined in terms of Nat.pred and is set up so that Nat.sub a 1 = Nat.pred (Nat.sub a 0) = Nat.pred a.

[Kyle Miller]

@Moritz Firsching I've investigated a bit more, and the reason does_not_work doesn't work is that there are some unassignable metavariables. You can use by exact to defer until they're solved for. This might be a bug in calc.

theorem does_not_work (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   calc 1 < 2^2 - 1 := by norm_num
        _  ≤ 2^p - 1 := by exact Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h

[Kyle Miller]

If you give enough type annotations, then it also goes through:

theorem does_not_work (p : ℕ) (h : p.Prime) : 1 < 2 ^ p - 1 := by
   calc 1 < (2^(2:Nat) - 1 : Nat) := by norm_num
        _  ≤ (2^p - 1 : Nat) := Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le h

These annotations give enough information for instance synthesis to complete.

[Moritz Firsching]

@Kyle Miller note also that this used to work and is a regression somewhere between 9125a0936fd86f4bb74bebe27f0b1cd0c5a2b7cf and aad19d883960cbdd1807a3c31ef7a351c3f0c733