Goal- Formalize and prove the following formula of arithmetics in PVS:
0+...+n = n*(n+1)/2 . *Improve your specification and proof skills.*
Step by step- Start PVS under a new context such as ~login/pvs/sum/;
- Create a new theory named sum (like the directory) using Meta-x new-pvs-file PVS command;
- Define a sum function (recursively) that will look like:
- sum(n: nat): RECURSIVE nat
= ??? MEASURE identity
*You may want to look at an**example of a theory**written by ENSEIRB students.* - Try to type check the theory, using Meta-x tc PVS command;
*does it correctly type check?* - Introduce the initial formula as a theorem:
- sum_formula: THEOREM
(FORALL (n: nat): ???) - Try proving the theorem using Meta-x prove PVS command while the cursor is within the theorem.
*Hint: use induction as a first command:**(INDUCT "n")**; you may want to look at PVS inference summary.*
VariantA variant of this exercise consists on using built-in finite set sum theory from finite_sets built-in PVS library, in order to compute 0+...+n, without defining a recursive sum function, then proving the result using finite set induction provided in the same built-in library. |