CODEWITHSUNDEEP
isabelleisar
Marco
Marco

Reputation: 330

Simplifying if-then-else in summations or products

While doing some basic algebra, I frequently arrive at a subgoal of the following type (sometimes with a finite sum, sometimes with a finite product).

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

This seems pretty obvious to me, but neither auto nor auto cong: sum.cong split: if_splits can handle this. What's more, sledgehammer also surrenders when called on this lemma. How can one efficiently work with finite sums and products containing if-then-else in general, and how to approach this case in particular?

Upvotes: 1

Views: 105

Answers (2)

Manuel Eberl
Manuel Eberl

Reputation: 8278

My favourite way to do these things (because it is very general) is to use the rules sum.mono_neutral_left and sum.mono_neutral_cong_left and the corresponding right versions (and analogously for products). The rule sum.mono_neutral_right lets you drop arbitrarily many summands if they are all zero:

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

The cong rule additionally allows you to modify the summation function on the now smaller set:

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

With those, it looks like this:

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

Upvotes: 3

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5790

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?

Upvotes: 1

Related Questions