Stuck again

Stream: new members

[Christopher Hoskin]

Previously (e.g. with lean 3.28.0 and mathlib commit 2ad4a4ce6afc3008272627320370f74cd2020c7f) lean was happy to write goal accomplished at the end of

import analysis.normed_space.basic

variables (β : Type*) [normed_group β] (b : β)

lemma group_pow_le_N (n:ℕ): ∥n • b∥ ≤ n * ∥b∥ :=
begin
  induction n with n ih,
  { norm_num, },
  { rw nat.succ_eq_add_one,
    calc ∥(n + 1) • b∥ = ∥ n•b + b ∥ : by { rw add_smul, simp,  }
    ... ≤ ∥n•b∥ + ∥b∥ : by { apply norm_add_le, }
    ... ≤ n * ∥b∥ + ∥b∥ : by { rw add_le_add_iff_right, exact ih, }
    ... ≤ (n+1)*∥b∥ : by { rw add_mul, simp, }
    ... ≤ (n.succ)*∥b∥ : by { rw nat.succ_eq_add_one, simp, }
  }
end

lemma group_pow_le_Z  : ∀ a:ℤ, ∥a • b∥ ≤ ∥a∥ * ∥b∥
  | (int.of_nat n) := by { simp,
    calc ∥n•b∥ ≤ n * ∥b∥ : by { apply group_pow_le_N,  }
    ... ≤ (abs n) * ∥b∥ : by { rw nat.abs_cast n, }
    ... ≤ ∥↑n∥ * ∥b∥ : by { rw ← real.norm_eq_abs n, exact rfl.ge, },
  }
  |(int.neg_succ_of_nat n)   :=
    begin
      rw [int.neg_succ_of_nat_coe, neg_smul, norm_neg, norm_neg],
      simp,
      -- Is there a way to avoid repeating the argument above?
      calc ∥(n+1)•b∥ ≤ (n+1) * ∥b∥ : by { apply group_pow_le_N,  }
      ... ≤ (abs (n+1)) * ∥b∥ : by { norm_cast, }
      ... ≤ ∥↑(n+1)∥ * ∥b∥ : by { rw ← real.norm_eq_abs (n+1), exact rfl.ge, },
    end

It wasn't very pretty, but it worked. Now (lean 3.31.0, mathlib commit 0c024a6270e43657c28aaf9664565a85593b3865) lean objects to the final calc with

invalid type ascription, term has type
  ∥(n + 1) • b∥ ≤ ∥↑(n + 1)∥ * ∥b∥
but is expected to have type
  ∥(↑n + 1) • b∥ ≤ ∥↑n + 1∥ * ∥b∥

I've spent hours playing around rewriting this in different ways, but I don't seem to be able to fix it. Please can someone give me a hint?

It's rather disheartening to be stuck on something one thought one had already proved.

Thanks,

Christopher

[Yakov Pechersky]

The casting logic got changed so it went a level deeper than before. Direct helper lemma here would be <-int.coe_nat_succ. In terms of repeating the argument, you could case on whether a <= -a or -a <= a, wlog extract the natural that corresponds to the nonnegative element.

[Eric Rodriguez]

Put exact_mod_cast before the calc, for a quick and dirty solution. Your main issue, however, is that you're using non-terminal simps; the simp lemmata can change between pull to pull and so it's considered to change all simps not at the end of the proof into simp only using squeeze_simp, so this exact issue doesn't happen

[Eric Rodriguez]

(@zulip mods: is there a link like #nng for non-terminal simps?)

[Yakov Pechersky]

I don't think the simp is directly the issue here, because each calc step explicitly sets the goal up.

[Eric Rodriguez]

Yes, but the issue seems to be that the overall calc isn't defeq to the goal,no?

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

Sorry, let me rephrase. The culprit here is the explicit coercion arrow. Just because the arrow is outside the parens doesn't mean the coercion is limited to the n + 1 term. The logic changed such that the arrow automatically pushes in to the n term.

[Yakov Pechersky]

So yes, it's not defeq to the goal like you said.

[Ruben Van de Velde]

Casing on the of_nat/neg_succ_of_nat constructors tends to lead to somewhat annoying proofs; one other approach is

lemma group_pow_le_Z (a : ℤ) : ∥a • b∥ ≤ ∥a∥ * ∥b∥ :=
begin
  cases int.nat_abs_eq a with h h;
  { conv_lhs { rw [h] },
    simp only [neg_smul, norm_neg, gsmul_coe_nat],
    apply le_trans (group_pow_le_N _ _ _) _,
    simp only [norm, int.cast_nat_abs] }
end

[Yakov Pechersky]

There's also int.induction_on

[Kyle Miller]

@Christopher Hoskin Are you wanting to prove these yourself, or would you be happy to use the mathlib lemmas?

lemma group_pow_le_N (n:ℕ): ∥n • b∥ ≤ n * ∥b∥ :=
begin
  apply norm_nsmul_le,
end

lemma group_pow_le_Z  : ∀ a:ℤ, ∥a • b∥ ≤ ∥a∥ * ∥b∥ :=
begin
  intro a,
  apply norm_gsmul_le a,
end

[Kyle Miller]

(These are newer than the version of mathlib you were previously using, having been added 2 months ago.)

[Christopher Hoskin]

@Kyle Miller Thanks - I'd be happy to use the mathlib lemmas. I fear my progress is so slow that mathlib will keep overtaking me!

[Kevin Buzzard]

You can keep bumping mathlib -- this is what I usually do with a longer project.