smul diamond

Stream: mathlib4

[Patrick Massot]

I am writing the linear algebra chapter of MIL and I was very disappointed to see that all our diamond infrastructure is not giving rfl for

import Mathlib

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (v : V) : (4 : ℤ) • v = (4 : K) • v := by
  exact_mod_cast zsmul_eq_smul_cast K (4 : ℤ) v

example (v : V) : 4 • v = (4 : K) • v :=
  nsmul_eq_smul_cast K 4 v

Am I missing something? Is this a well-known unsolvable issue?

[Jireh Loreaux]

I don't think I understand. The whole point of forgetful inheritance is that we store the low-level data in the high-level structure so that when you go back down you don't forget the original definition (and make up a new one built from the bigger structure).

Point being: you've got an SMul ℕ V instance, a SMul K V instance and a NatCast V (or OfNat) instance, all of which could have arbitrarily complicated definitions, and you somehow want, for n : ℕ, v : V, for n • v = (Nat.cast n : K) • v to hold definitionally? Admittedly, because they have Field and Module instances, they obviously hold propositionally, but I'm just not clear why you think these arbitrary structures should be expected to be definitionally equal.

[Jireh Loreaux]

If you didn't do forgetful inheritance, then you could ensure this was true definitionally for Field and Module, but then you would be creating diamonds.

[Jireh Loreaux]

Ah, I think I totally missed the point of your question. You didn't mean you wanted the proofs to be rfl, you meant that you didn't want to need exact_mod_cast, correct?

[Yury G. Kudryashov]

The issue here is that Int.cast is defined using a typeclass, not by cases on the integer number.

[Yury G. Kudryashov]

BTW, I don't know if some of these typeclasses can be discarded in Lean 4, since it inserts explicit *.casts

[Yury G. Kudryashov]

Of course, this will make something like (Nat.cast n : Nat) = n a non-rfl.

[Yury G. Kudryashov]

UPD: no, Algebra Nat Nat needs it to be rfl.

[Yury G. Kudryashov]

(or we need to drop the algebraMap from Algebra and define it in terms of SMul)

[Eric Wieser]

I think the right proofs here are:

import Mathlib

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (v : V) : (4 : ℤ) • v = (4 : K) • v := by
  rw [ofNat_smul_eq_nsmul ℤ, ofNat_smul_eq_nsmul K]

example (v : V) : 4 • v = (4 : K) • v :=
  (ofNat_smul_eq_nsmul _ _ _).symm

[Eric Wieser]

This isn't Nat.cast or Int.cast, but OfNat.ofNat so you should be using the ofNat lemma

[Eric Wieser]

So I think your problem is not about smul at all, and actually that

example : (4 : K) = ((4 : ℤ) : K) := rfl -- fails

since you're treating the LHS as though it were the RHS

[Kevin Buzzard]

I think the problem is that we have all these cast tactics but they don't prove the examples in Patrick's post (neither of of norm_cast, push_cast prove it, even though it looks like it's of the form x=x). Presumably what one would want to tell a beginner here is "just use this tactic". All the proofs which work above are pretty horrible (e.g. I think I might have struggled to find any of them, exact? and hint don't work for the first one so this is a pretty poor user experience here).

[Eric Wieser]

I think the difficulty with solving norm_cast is choosing what the norm form is. Usually when you use norm_cast, the rule is just "make the outer expression the simplest type you can". When your expression is about a module over multiple rings, you now need to pick which ring to normalize inner expressions into

[Kevin Buzzard]

To make matters worse, the proofs in Patrick's code sample use deprecated functions and when I replace the functions with what Lean tells me to replace them with, the proofs no longer work :-(

import Mathlib

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (v : V) : (4 : ℤ) • v = (4 : K) • v := by
  exact_mod_cast zsmul_eq_smul_cast K (4 : ℤ) v
/-
`zsmul_eq_smul_cast` has been deprecated, use `Int.cast_smul_eq_nsmul` instead
-/

example (v : V) : (4 : ℤ) • v = (4 : K) • v := by
  exact_mod_cast Int.cast_smul_eq_nsmul K (4 : ℤ) v
/-
mod_cast has type
  4 • ?m.15669 = 4 • ?m.15669 : Prop
but is expected to have type
  4 • v = 4 • v : Prop
-/

[Eric Wieser]

The deprecated versions are the reverse of the new versions (I guess it was awkward to convey that with deprecated)

[Eric Wieser]

(also it looks like you're behind the web editor, Int.cast_smul_eq_nsmul was a typo and no longer exists, it is now Int.cast_smul_eq_zsmul)

[Eric Wieser]

We could teach simp to solve this specific problem with ofNat_smul_eq_ofNat_smul, but this doesn't compose to anything more useful in more complex cases

[Patrick Massot]

Yes, the point is that there doesn’t seem to be any nice proof for such an obvious statement. This is really super frustrating.

[Eric Wieser]

I think the answer here is that we need to write the module tactic analogous to ring

[Jireh Loreaux]

I guess with this module tactic it would accept a type argument for the scalar ring?

[Eric Wieser]

Optimistically it could just work it out

[Eric Wieser]

If your rings all form a directed graph into a single Algebra, you can just keep promoting till they match

[Eric Wieser]

Probably the only cases that are crucial to handle are mixtures of Nat, Int, Rat, and K

[Patrick Massot]

Eric Wieser said:

I think the answer here is that we need to write the module tactic analogous to ring

Yes, this is one of the first things I wrote in this chapter.

[Antoine Chambert-Loir]

Did somebody do the mathematical work for that? (= a normal form algorithm for expressions in modules)