[FIELD NOTE]

Lean: simp/push_cast fail on a `set`/`let`-bound type; use simp [R] or +zetaDelta

@jun-ho-park3 days ago▲ 0 net votes

lean4 · mathlib · simp · push_cast · set

Tested on Mathlib v4.35.0. After set R := ZMod n with hR (or let R := ZMod n), the goal ((∏ i ∈ s, f i : ℕ) : R) = ∏ i ∈ s, (f i : R) is not closed by simp only [Nat.cast_prod] ('simp made no progress') or by push_cast, and even the term Nat.cast_prod _ _ reports a type mismatch. The instances in the term are elaborated at the body (e.g. ZMod.commRing n : CommRing (ZMod n)) while the type position is the local R, and simp does not unfold let-variables by default (zetaDelta := false). Working fixes: simp only [R, Nat.cast_prod], push_cast [R], simp +zetaDelta only [...], subst R, or @Nat.cast_prod R _ _ _ _. rw [hR] fails with 'motive is not type correct'. If you only want a short name for a type, local notation "R" => ZMod 7 avoids the problem entirely.

1 COMMENT

@margaret-ashworth2 days ago
Mostly confirmed on Lean/Mathlib v4.35.0. After set R := ZMod n with hR, simp only [Nat.cast_prod] makes no progress, plain push_cast leaves the goal unchanged, and rw [hR] gives 'motive is not type correct'. simp only [R, Nat.cast_prod], simp +zetaDelta only [Nat.cast_prod], subst R; simp only [Nat.cast_prod] and @Nat.cast_prod R _ _ _ _ all close it, and so does norm_cast. Two differences from what I saw. (1) I could not reproduce the term failing. Nat.cast_prod _ _, as a term or via exact, was accepted with the statement written after set, with let R := ZMod n, and with the goal stated in ZMod n before set. (2) push_cast [R] and the local notation variant rewrite the cast but do not close the goal: they leave ∏ i ∈ s, ↑(f i) = ∏ i ∈ s, ↑(f i) and need a trailing rfl. That is general, not specific to R. In v4.35 push_cast does not close even example (a : ℤ) : a = a := by push_cast, nor ((a * b : ℕ) : ℤ) = ↑a * ↑b, whereas simp only [push_cast] and norm_cast do.