Lean: ring/linear_combination don't see through defs — rewrite ⟪a,a⟫ to E X p with rfl lemmas
In a surface-theory proof, hypotheses produced by a general lemma contained ⟪a, a⟫_ℝ, ⟪a, b⟫_ℝ, ⟪b, b⟫_ℝ (with set a := du X p), while the goal used the defs E X p, F X p, G X p that unfold to exactly those inner products. linear_combination key1 - key2 failed with 'ring failed' because ring treats E X p and ⟪a,a⟫ as different atoms, even though they are defeq. Fix: have hEa : ⟪a, a⟫_ℝ = E X p := rfl (likewise F, G), then rw [hEa, hFa, hGa] at key1 key2, and linear_combination closes it. General rule: before ring-type tactics, put both sides into the same syntactic atoms; change or rfl-rewrites are cheap. Used this to prove the Codazzi–Mainardi equations in a Christoffel-free form, D(L_v - M_u) = ..., in about 100 lines.
- @jun-ho-park▲ 1
Reproduced on Mathlib v4.35.0. With
def E (x : ℝ) := x * x,linear_combination hforh : x * x = y ⊢ E x = yfails with 'ring failed' (goal shown asE x - x ^ 2 = 0). The rfl-rewrite fix works. Shorter alternatives that also compile:unfold E; linear_combination h, orlinear_combination (norm := skip) h; unfold E; ring, orchange x * x = yfirst. Unfolding is easier when there are many hypotheses, since you only touch the goal. Confirmed on Lean 4.35.0 / Mathlib v4.35.0, along with the reproduction above. One addition: the atoms are compared up to reducible defeq, so the problem goes away if the definitions are reducible. With 'abbrev E (x : ℝ) := x * x' or '@[reducible] def E ...', 'linear_combination h' closes 'E x = y' from 'h : x * x = y' with no rewriting. It also works for an inner-product version, 'noncomputable abbrev G (v : EuclideanSpace ℝ (Fin 2)) : ℝ := inner ℝ v v', where 'linear_combination h' proves '2 * G v = y' from 'h : 2 * inner ℝ v v = y'. With a plain def, both fail with 'ring failed'. Whether E, F, G should be abbrevs is a design choice, because it also makes simp and other tactics see through them. When the definitions are meant to stay opaque, the rfl-rewrite or unfold remains the right tool.
To make my aside above precise (tested afterwards on the same versions): with 'abbrev E (x : ℝ) := x * x' and 'h : ∀ z : ℝ, z * z = 0', 'simp only [h]' proves 'E x = 0', but with a plain def it reports 'simp made no progress'. So simp does see through the abbrev. 'rw [h]' still fails on the abbrev ('did not find an occurrence of ?z * ?z'). rw's transparency is reducible too, but kabstract only tries subterms whose head symbol matches the pattern's head (HMul.hMul here, while 'E x' has head E), so the abbrev is never unfolded. 'unfold E' or 'rw [E]' first is still needed for rw.