Suppose that f _i = g_i (where i is an indexing variable) we want to show that sum f_i = sum g_i

Is there an appropriate lemma for this?

`sum.cong`

Generally, theorems of the form ‘Given that x and x' are in some relation and y and y' are in some relation, `f x y = f x' y'`

are called congruence rules.

Typically that relation of the arguments is some kind of equality (and only then can the simplifier use it as congruence rules). But it can also be e.g. an equality with some extra assumptions, e.g. in your case `A = B ⟹ (⋀x. x ∈ B ⟹ g x = h x) ⟹ sum g A = sum h B`

.

Thank you that worked..... and last question if you can: How do I factor a constant out of a sum like sum c*f_i = c * sum f_i.

you could use `find_theorem "_ * sum _"`

to see what theorems fit. If there is none, you should be able to prove this via induction

I really am very new so I apologize if my questions are basic: but this throws the following error (after adding s to end of find_theorem):

Type unification failed: No type arity fun :: times

Type error in application: incompatible operand type

Operator: (*) _ :: ??'a ⇒ ??'a

Operand: sum _ :: ??'b set ⇒ ??'c

I suppose I could try proving this by induction but I feel it should be proven by now. I imagine I need to specify types for the wild cards?

I think I missed an extra underscore with `sum`

(because it has two arguments, not one)

That worked! thank you. It was the first result and I simply had to change my sum from i=0...n to i \in {0...n} to satisfy the theorem's requirements. Awesome.

`i=0..n`

is the same as `i ∈ {0..n}`

. It's just syntax; internally it's exactly the same.

Last updated: Dec 07 2023 at 20:16 UTC