Dustin Bryant (Jan 15 2023 at 04:17): 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?
Manuel Eberl (Jan 15 2023 at 11:53):sum.cong
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.
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.
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.
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
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?
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)
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.
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: Apr 25 2024 at 20:15 UTC