如何在Lean中将自定义Vec类型的加法重写为操作定义？

代码背景 #

abbrev Vec (α : Type) (n : Nat) := Fin n → α

def Vec.map2 {α β φ n} (f : α → β → φ) (v₁ : Vec α n) (v₂ : Vec β n) : Vec φ n :=
  fun i ↦ f (v₁ i) (v₂ i)

def Vec.add {α n} [Add α] (v₁ v₂ : Vec α n) : Vec α n :=
  Vec.map2 (· + ·) v₁ v₂

instance {α n} [Add α] : Add (Vec α n) where
  add := Vec.add

theorem Vec.add_comm {α n} [AddCommMonoid α] {v₁ v₂ : Vec α n}
    : v₁ + v₂ = v₂ + v₁ := by
  ...

问题描述 #

我自定义了Vec类型（不满意内置版本），并为它实现了Add类型类。现在我要为这个类型证明定理，第一步想把目标重写成Vec.map2 (· + ·) v₁ v₂ = Vec.map2 (· + ·) v₂ v₁。没实现Add之前，我只用rw [Vec.add]就能改写Vec.add v₁ v₂ = Vec.add v₂ v₁，但加了Add实例后，这操作就难办了，找不到解决办法。

解决办法 #

核心问题是：实现Add实例后，v₁ + v₂会被Lean解析为Add.add v₁ v₂，而非直接的Vec.add v₁ v₂，所以原有的rw [Vec.add]无法匹配目标。这里提供两种直接的解决方式：

方式一：分步展开定义

先把+展开为Add.add，再展开为Vec.add，最终得到Vec.map2的形式：

theorem Vec.add_comm {α n} [AddCommMonoid α] {v₁ v₂ : Vec α n}
    : v₁ + v₂ = v₂ + v₁ := by
  rw [Add.add, Add.add] -- 将两边的+都替换为Add.add（也就是我们定义的Vec.add）
  rw [Vec.add, Vec.add] -- 进一步替换为Vec.map2的调用
  -- 后续证明步骤
  funext i
  rw [add_comm]

方式二：用simp一键展开

利用simp直接展开所有相关定义，一步到位：

theorem Vec.add_comm {α n} [AddCommMonoid α] {v₁ v₂ : Vec α n}
    : v₁ + v₂ = v₂ + v₁ := by
  simp [Add.add, Vec.add] -- 自动展开+和Vec.add的定义
  funext i
  apply add_comm

补充说明 #

如果想更直接地关联+和Vec.add，也可以用反向重写：rw [← Vec.add]，不过需要确保上下文匹配。本质上都是让Lean明确+对应的底层实现就是我们写的Vec.add，从而完成目标的改写。

内容的提问来源于stack exchange，提问作者user8203231