PVS‎ > ‎exercises‎ > ‎

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

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
  1. Start PVS under a new context such as ~login/pvs/sum/;
  2. Create a new theory named sum (like the directory) using Meta-x new-pvs-file PVS command;
  3. 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.
  4. Try to type check the theory, using Meta-x tc PVS command; does it correctly type check?
  5. Introduce the initial formula as a theorem:
    • sum_formula: THEOREM
        (FORALL (n: nat): ???)
  6. 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.
Variant
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.
Comments