简化求和或乘积中的 if-then-else

问题描述

在做一些基本的代数时，我经常达到以下类型的子目标（有时是有限的和，有时是有限的积）。

lemma foo:
  fixes N :: nat
  fixes a :: "nat ⇒ nat"
  shows "(a 0) = (∑x = 0..N. (if x = 0 then 1 else 0) * (a x))"

这对我来说似乎很明显，但 auto 和 auto cong: sum.cong split: if_splits 都无法处理。更重要的是，当调用这个引理时，sledgehammer 也会投降。一般而言，如何有效地处理包含 if-then-else 的有限和和乘积，以及如何特别处理这种情况？

解决方法

我最喜欢做这些事情的方法（因为它非常通用）是使用规则 sum.mono_neutral_left 和 sum.mono_neutral_cong_left 以及相应的 right 版本（产品类似）。规则 sum.mono_neutral_right 允许您删除任意多个都为零的被加数：

finite T ⟹ S ⊆ T ⟹ ∀i∈T - S. g i = 0
⟹ sum g T = sum g S

cong 规则还允许您修改现在较小的集合上的求和函数：

finite T ⟹ S ⊆ T ⟹ ∀i∈T - S. g i = 0 ⟹ (⋀x. x ∈ S ⟹ g x = h x)
⟹ sum g T = sum h S

有了这些，它看起来像这样：

lemma foo:
  fixes N :: nat and a :: "nat ⇒ nat"
  shows "a 0 = (∑x = 0..N. (if x = 0 then 1 else 0) * a x)"
proof -
  have "(∑x = 0..N. (if x = 0 then 1 else 0) * a x) = (∑x ∈ {0}. a x)"
    by (intro sum.mono_neutral_cong_right) auto
  also have "… = a 0"
    by simp
  finally show ?thesis ..
qed

,

假设左手侧可以使用之间的任意值0和N，什么有关添加更一般的引理

lemma bar:
  fixes N :: nat
  fixes a :: "nat ⇒ nat"
  assumes
    "M ≤ N"
  shows "a M = (∑x = 0..N. (if x = M then 1 else 0) * (a x))"
  using assms by (induction N) force+

和解决原来的含using bar by blast？