Email Gateway (Aug 19 2022 at 14:53): Email Gateway (Aug 19 2022 at 14:53):From: Felix Breuer <felix@fbreuer.de>
Hello Isabelle Community!
On Sunday I took my first steps with Isabelle at the very nice and useful Isabelle Tutorial at the Vienna Summer of Logic. Having finished the exercises I am now working on porting a toy proof that I did some time ago using Freek Wiedijk’s miz3 (based on HOL Light) to Isabelle/Isar. In this context, two questions came up:
1) Does Isabelle have a theory for finite sums of numbers?
What is the best way to represent in Isabelle/HOL the sum of all integers from 1 to n or the sum of all integers in a given list? Are there theorems for working with sums available? For example, is the rewrite rule (in mathematical/TeX notation):
\sum_{i=0}^n a_i = a_0 + \sum_{i=1}^n
proved somewhere in Isabelle’s library? A naive search of the library did not turn up anything.
2) In Isar proofs, is there a way to omit the “by” clause at the end of each statement?
I find that many steps in Isar proofs can be justified by one of the usual suspects (simp, auto, blast, force,…). Is there a way to omit the “by” clause and have Isabelle implicitly try the most common proof methods in some order? miz3 has this feature and it unclutters miz3 proofs considerably.
Thanks,
Felix
Email Gateway (Aug 19 2022 at 14:53):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle supports sums and products over index sets very generally, via axiomatic type classes (allowing just about all kinds of numbers). Index sets can be anything, but there is particular support for intervals of various kinds (over naturals, integers and other ordered types).
For some proofs over summations, see Convex.thy and Formal_Power_Series.thy in HOL/Library/.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:54):From: Lars Hupel <hupel@in.tum.de>
Hello Felix,
1) Does Isabelle have a theory for finite sums of numbers?
indeed it does:
term "∑i ∈ {0..n}. f i"
What is the best way to represent in Isabelle/HOL the sum of all
integers from 1 to n or the sum of all integers in a given list?
The sum of all integers from 1 to n can be written like this:
term "∑i ∈ {1..n}. i"
(although here, the types of "1", "n" and "i" are polymorphic; so they
can be "int" or "nat" or ...)
You can write the above even shorter:
term "∑{1..n}"
The underlying constant for sums of sets is called "setsum", and by
analogy, there's also "listsum" to compute the sum of the elements in a
list.
Are there theorems for working with sums available? For example, is the
rewrite rule (in mathematical/TeX notation):\sum_{i=0}^n a_i = a_0 + \sum_{i=1}^n
Let's state this more generally:
lemma "k ≤ n ⟹ (∑i ∈ {k..n}. f i) = f k + (∑i ∈ {Suc k..n}. f i)"
Isabelle/jEdit tells us:
Auto solve_direct: The current goal can be solved directly with
Set_Interval.setsum_head_Suc:
?m ≤ ?n ⟹ setsum ?f {?m..?n} = ?f ?m + setsum ?f {Suc ?m..?n}
Your original rule can be proved like this:
lemma "0 < (n::nat) ⟹ (∑i ∈ {0..n}. f i) = f 0 + (∑i ∈ {1..n}. f i)"
by (auto simp: setsum_head_Suc)
For these kinds of things, you might want to try the "find_theorems"
command. For example, the query
find_theorems "setsum ?f _ = ?f _ + setsum ?f _"
finds the relevant theorem and some more.
Cheers
Lars
Email Gateway (Aug 19 2022 at 14:57):From: Felix Breuer <felix@fbreuer.de>
Hi Lars and Larry,
thank you for your help! Just knowing that the right name to search for was “setsum” helped a lot. Just searching for theorems containing “sum” (in the JEdit Query Panel) - as I had done before - finds nothing.
After some more work, I am now thoroughly stuck again, though: I want to prove:
lemma "( ∑ k∈{0..m}. ((f (Suc k)) * (recip f (n - (Suc k)))) ) = ( ∑ k∈{(Suc 0)..(Suc m)}. ((f k) * (recip f (n - k))) )"
Whatever f and recip are, this should follow simply from setsum_shift_bounds_cl_Suc_ivl, which reads:
corollary setsum_shift_bounds_cl_Suc_ivl:
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}”
However, I cannot figure out how to get Isabelle to instantiate the corollary in the right way. When I try to prove the lemma using
by (simp add: setsum_shift_bounds_cl_Suc_ivl)
I get
Failed to finish proof⌂:
goal (1 subgoal):
So simp applies a wrong rewrite rule and then gets stuck. Using Sledgehammer to get some hints on how to do it right, only resulted in time outs. So what am I missing?
Thanks again,
Felix
Email Gateway (Aug 19 2022 at 14:57):From: Lars Noschinski <noschinl@in.tum.de>
On 18.07.2014 20:54, Felix Breuer wrote:
Hi Lars and Larry,
thank you for your help! Just knowing that the right name to search for was “setsum” helped a lot. Just searching for theorems containing “sum” (in the JEdit Query Panel) - as I had done before - finds nothing.
In such cases, it might help searching for theorems with a certain name,
e.g. "name: set". Also, you can search for constants of a certain type.
After some more work, I am now thoroughly stuck again, though: I want to prove:lemma "( ∑ k∈{0..m}. ((f (Suc k)) * (recip f (n - (Suc k)))) ) = ( ∑ k∈{(Suc 0)..(Suc m)}. ((f k) * (recip f (n - k))) )"
Whatever f and recip are, this should follow simply from setsum_shift_bounds_cl_Suc_ivl, which reads:
corollary setsum_shift_bounds_cl_Suc_ivl:
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}”However, I cannot figure out how to get Isabelle to instantiate the corollary in the right way. When I try to prove the lemma using
by (simp add: setsum_shift_bounds_cl_Suc_ivl)
There is "subst" which applies only a single rule at a single position.
You can also instruct simp to use only the given set of rules.
by (subst setsum_shift_bounds_cl_Suc_ivl) ..
(* where ".." equals "rule" for most purposes *)
or
by (simp only: setsum_shift_bounds_cl_Suc_ivl)
Last but not least, you can also identify the wrong rule by using the
simplifier trace:
using [[simp_trace]]
apply simp
(* Look in the tracing output to identify the wrong rule, then
replace apply simp by: *)
by (simp del: foo)
Best regards,
Lars
Last updated: Apr 26 2024 at 12:28 UTC