PVS‎ > ‎exercises‎ > ‎

### 0+...+n = n*(n+1)/2

 GoalFormalize 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.