Pain with WithBot

Stream: new members

[Vincent Beffara]

I have the following code, which works:

import Mathlib

def progression (a δ : ℝ) : ℕ → List ℝ
| 0 => [a]
| n+1 => a :: progression (a + δ) δ n

lemma maximum_progression (h : 0 ≤ δ) : (progression a δ n).maximum = a + n * δ := by
  induction n generalizing a with
  | zero => simp [progression]
  | succ n ih =>
    simp only [progression, List.maximum_cons, ih, Nat.cast_succ]
    have e1 : (1 : WithBot ℝ) = ((1 : ℕ) : ℝ) := by norm_cast
    have e2 : (n : WithBot ℝ) = (n : ℝ) := by norm_cast
    have e3 : 0 ≤ (n : ℝ) := n.cast_nonneg
    convert max_eq_right ?_ using 1
    · simp only [e1, e2, ← WithBot.coe_mul, ← WithBot.coe_add, WithBot.coe_eq_coe]
      ring
    · simp only [e1, e2, ← WithBot.coe_mul, ← WithBot.coe_add, WithBot.coe_le_coe]
      nlinarith [e3]

However, most of it is wrangling with WithBot.coe and convincing lean that everything is happening in the reals where it is obvious. Somehow I get the feeling that norm_cast is pushing in the wrong direction when I try to use it instead of applying coe_add and coe_mul backwards by hand. What am I doing wrong?

[Jireh Loreaux]

This isn't exactly an answer to your question, but here are my initial thoughts.

1. I probably would have defined progression as:

def progression (a δ : ℝ) (n : ℕ) : List ℝ := List.range (n + 1) |>.map (a + ((↑) : ℕ → ℝ) · * δ)

2. Then I would want to apply two library lemmas, but I don't think either of them exists currently. My suggestion: prove the following lemmas and use them to prove the result with the definition I gave of progression above.

lemma List.maximum_range_succ (n : ℕ) : (List.range (n + 1) |>.maximum) = n := sorry

lemma List.maximum_map (α β : Type*) [Preorder α] [Preorder β] [DecidableRel ((· : α) < ·)]
    [DecidableRel ((· : β) < ·)] (l : List α) (f : α → β) (hf : Monotone f) :
    (l.map f).maximum = .map f l.maximum := sorry

[Jireh Loreaux]

As an attempt to rewrite your proof slightly, I might do something like this:

lemma maximum_progression (h : 0 ≤ δ) (n : ℕ) : (progression a δ n).maximum = (a + n * δ : ℝ) := by
  induction n generalizing a with
  | zero => simp [progression]
  | succ n ih =>
    simp only [progression, List.maximum_cons, ih, Nat.cast_succ]
    convert max_eq_right ?_ using 1
    · congr 1; push_cast; ring
    · norm_cast; rw [add_assoc]; exact (add_zero a).symm.trans_le (by gcongr; positivity)

Note that it would have been nice if the last line could have been norm_cast; rw [add_assoc]; gcongr; I'm not sure why it needed positivity, but I think I know why it needed the add_zero bit.

[Jireh Loreaux]

@Heather Macbeth (a) do you know why gcongr didn't automatically use positivity above? (b) I guess there's no way to make le_add_of_nonneg_right into a gcongr lemma because there is no head symbol (besides a) on the left-hand side? :sad:

[Heather Macbeth]

Jireh Loreaux said:

(b) I guess there's no way to make le_add_of_nonneg_right into a gcongr lemma because there is no head symbol (besides a) on the left-hand side? :sad:

@Jireh Loreaux The goal here is

⊢ a ≤ a + (δ + ↑n * δ)

and that's not a generalized-congruence-type goal!

Actually, I have a teaching tactic called extra which solves this kind of goal, see Examples 1.4.7-1.4.10 and Examples 3.4.2-3.4.4 in my lecture notes. (It indeed wraps lemmas like le_add_of_nonneg_right.) I have been on the fence about whether to PR it -- it's currently hacky and would need a rewrite for robustness first.

[Heather Macbeth]

Jireh Loreaux said:

(a) do you know why gcongr didn't automatically use positivity above?

The initial goal at the point you're asking about is

⊢ a + 0 ≤ a + (δ + ↑n * δ)

and so the goal 0 ≤ δ + ↑n * δ generated by gcongr acting on it is a "main" rather than "side" goal -- gcongr uses positivity as a discharger only on "side" goals, not "main" goals (and I claim this is better, for predictability and speed).

[Jireh Loreaux]

Understood about positivity as only being automatically applied to side goals. That makes sense.

Yes, I know it isn't technically a gcongr' form, I was just hoping it might be able to insert the + 0`, or to apply that lemma, but I understand that's likely scope creep.