- 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:
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(n: nat): RECURSIVE nat
You may want to look at an example of a theory written by ENSEIRB students.
Try proving the theorem using Meta-x prove PVS command while the cursor is within the theorem.
- sum_formula: THEOREM
(FORALL (n: nat): ???)
- Hint: use induction as a first command: (INDUCT "n"); you may want to look at PVS inference summary.
A 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.