1

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

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，特别是如何处理这种情况？

4

2 回答 2

3

我最喜欢做这些事情的方法（因为它非常通用）是使用规则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
于 2021-01-07T18:21:13.203 回答
1

Assuming the left-hand side could use an arbitrary value between 0 and N, what about adding a more general lemma

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+

and solving the original one with using bar by blast?

于 2021-01-07T16:25:21.393 回答