Stream: Beginner Questions

Topic: equal summands ==> equal sums


view this post on Zulip Dustin Bryant (Jan 15 2023 at 04:17):

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?

view this post on Zulip Manuel Eberl (Jan 15 2023 at 11:53):

sum.cong

view this post on Zulip Manuel Eberl (Jan 15 2023 at 11:54):

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.

view this post on Zulip Manuel Eberl (Jan 15 2023 at 11:56):

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.

view this post on Zulip Dustin Bryant (Jan 15 2023 at 16:34):

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.

view this post on Zulip Jan van Brügge (Jan 15 2023 at 16:46):

you could use find_theorem "_ * sum _" to see what theorems fit. If there is none, you should be able to prove this via induction

view this post on Zulip Dustin Bryant (Jan 15 2023 at 17:29):

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?

view this post on Zulip Jan van Brügge (Jan 15 2023 at 17:48):

I think I missed an extra underscore with sum (because it has two arguments, not one)

view this post on Zulip Dustin Bryant (Jan 15 2023 at 17:58):

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.

view this post on Zulip Manuel Eberl (Jan 15 2023 at 18:23):

i=0..n is the same as i ∈ {0..n}. It's just syntax; internally it's exactly the same.


Last updated: Feb 27 2024 at 08:17 UTC