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

Question

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

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 的有限和和乘积，以及如何处理这种情况？

Answer 1

假设左侧可以使用 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?

解决原始问题

Answer 2

我最喜欢做这些事情的方法（因为它非常通用）是使用规则 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

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

Simplifying if-then-else in summations or products

isabelle

isar