diff options
| -rw-r--r-- | assignment7/D.prf | 414 | ||||
| -rw-r--r-- | assignment7/D.pvs | 104 | ||||
| -rw-r--r-- | assignment7/D.status | 24 | ||||
| -rw-r--r-- | assignment7/E.prf | 386 | ||||
| -rw-r--r-- | assignment7/E.pvs | 109 | ||||
| -rw-r--r-- | assignment7/E.status | 19 |
6 files changed, 1056 insertions, 0 deletions
diff --git a/assignment7/D.prf b/assignment7/D.prf new file mode 100644 index 0000000..d41d2b2 --- /dev/null +++ b/assignment7/D.prf @@ -0,0 +1,414 @@ +(th_D + (sum_TCC1 0 + (sum_TCC1-1 nil 3667129223 ("" (subtype-tcc) nil nil) nil nil)) + (sum_TCC2 0 + (sum_TCC2-1 nil 3667129223 ("" (termination-tcc) nil nil) nil nil)) + (D_1 0 + (D_1-1 nil 3667129225 + ("" (induct n) + (("1" (assert) (("1" (grind) nil nil)) nil) + ("2" (skeep) (("2" (expand sum 1) (("2" (assert) nil nil)) nil)) + nil)) + nil) + ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (D_2 0 + (D_2-1 nil 3667129345 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (expand id 1 1) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil) + ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (id_preserves application-judgement "S" identity_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (id const-decl "(bijective?[T, T])" identity nil) + (bijective? const-decl "bool" functions nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (pow_TCC1 0 + (pow_TCC1-1 nil 3667129223 ("" (skeep) (("" (assert) nil nil)) nil) + ((int_minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil)) + nil)) + (pow_TCC2 0 + (pow_TCC2-1 nil 3667144387 ("" (termination-tcc) nil nil) nil nil))) +(th_Da + (Da_1 0 + (Da_1-1 nil 3667129545 + ("" (induct n1) + (("1" (expand sum) + (("1" (expand square) (("1" (propax) nil nil)) nil)) nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) + (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (odd_plus_even_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_times_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (square const-decl "nat" th_Da nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) nil + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers + nil)) + shostak)) + (Da_2 0 + (Da_2-1 nil 3667129831 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil) + ((posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (even_plus_even_is_even application-judgement "even_int" integers + nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_times_posint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (square const-decl "nat" th_Da nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (Da_3 0 + (Da_3-1 nil 3667129862 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1 1) + (("2" (expand sum 1 2) + (("2" (replace -1 1) + (("2" (expand square 1) + (("2" (expand cube 1) + (("2" (lemma D_1) + (("2" (inst -1 j) + (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((mult_divides2 application-judgement "(divides(m))" divides nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (D_1 formula-decl nil th_D nil) + (even_plus_even_is_even application-judgement "even_int" integers + nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) nil + (square const-decl "nat" th_Da nil) + (cube const-decl "nat" th_Da nil) nil + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (Da_4 0 + (Da_4-1 nil 3667130517 + ("" (induct n1) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) + (("2" (expand pow 1 3) (("2" (propax) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (>= const-decl "bool" reals nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (pred type-eq-decl nil defined_types nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (sum def-decl "nat" th_D nil) (pow def-decl "nat" th_D nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nat_induction formula-decl nil naturalnumbers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (odd_minus_odd_is_even application-judgement "even_int" integers + nil)) + shostak)) + (Da_5 0 + (Da_5-1 nil 3667130601 + ("" (induct n1) + (("1" (expand sum 1) (("1" (propax) nil nil)) nil) + ("2" (skeep) (("2" (expand sum 1) (("2" (propax) nil nil)) nil)) + nil)) + nil) + ((nat_induction formula-decl nil naturalnumbers nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil)) + shostak))) +(th_Db + (geom_TCC1 0 + (geom_TCC1-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil)) + (geom_TCC2 0 + (geom_TCC2-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil)) + (geom_TCC3 0 + (geom_TCC3-1 nil 3667129224 ("" (termination-tcc) nil nil) nil nil)) + (geom_sum 0 + (geom_sum-1 nil 3667130791 + ("" (induct a) + (("1" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (split -1) + (("1" (expand geom 1) + (("1" (replace -1 1) (("1" (grind) nil nil)) nil)) nil) + ("2" (propax) nil nil)) + nil)) + nil)) + nil) + ("2" (skeep) + (("2" (induct n) + (("1" (grind) nil nil) + ("2" (skolem 1 k) + (("2" (flatten 1) + (("2" (split -1) + (("1" (expand geom 1) + (("1" (replace -1 1) + (("1" (expand pow 1 3) (("1" (propax) nil nil)) nil)) + nil)) + nil) + ("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (even_minus_odd_is_odd application-judgement "odd_int" integers + nil) + (nzint_times_nzint_is_nzint application-judgement "nzint" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (pow def-decl "nat" th_D nil) (geom def-decl "posnat" th_Db nil) + (posnat nonempty-type-eq-decl nil integers nil) + (nonneg_int nonempty-type-eq-decl nil integers nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (> const-decl "bool" reals nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak))) + diff --git a/assignment7/D.pvs b/assignment7/D.pvs new file mode 100644 index 0000000..19ff64f --- /dev/null +++ b/assignment7/D.pvs @@ -0,0 +1,104 @@ +%%% NAME/LOGIN-ID Camil Staps / s4498062_ +%%% ACKNOWLEDGMENTS: + +%%% +%%% INDUCTION +%%% These examples of induction can be proven using the arithmetic decision procedures +%%% (ASSERT). You will need to EXPAND definitions selectively: (EXPAND "name" FN ON ...) +%%% expands Occurance N of the function "name" in formula number FN (see the help listing +%%% for more information. +%%% +%%% It is highly recommended that you prove the results by hand before trying to explain +%%% them to PVS. However, most of the proofs yield to a systematic application of induction. +%%% + +th_D: THEORY + BEGIN + + n: VAR nat + f: VAR [nat->nat] + +%%% +%%% Defining recursive functions. Here is the form of a recursive function definition +%%% over the natural numbers. The MEASURE clause is used to prove well-definedness. +%%% We will discuss this later on. +%%% + + sum(n): RECURSIVE nat = + IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF + MEASURE n + +%%% +%%% Use (INDUCT "n") to start the proof of Theorem F_1. +%%% ~~~~~~~~~~~~ + +D_1: THEOREM 2 * sum(n) = (n * (n + 1)) + +%%% +%%% Higher order parameters. Here is a slightly more general version of "summation" +%%% + + sum(n,f) : RECURSIVE nat = + IF n = 0 THEN f(0) ELSE f(n) + sum(n - 1,f) ENDIF + MEASURE n + +D_2: THEOREM 2 * sum(n,id) = (n*(n+1)) + + pow(a, n: nat) : RECURSIVE nat = + IF n=0 + THEN 1 + ELSE a * pow(a, n-1) + ENDIF + MEASURE n + +END th_D + +%%% +%%% PVS source files can contain more than one theory. +%%% Theories can include other theories. +%%% + +th_Da : THEORY + + BEGIN + + importing th_D % Use THEORY D + + n : var nat + i : var nat + f : var [nat -> nat] + + square(n:nat) : nat = n*n + cube(n:nat) : nat = n*n*n + +%%% +%%% As in Scheme, LAMBDA is used to express functions without giving them names. +%%% WARNING: at least one of these requires insightful thinking. +%%% HINT: If you get stuck, try EXPAND +%%% + +Da_1: PROPOSITION sum(n, (LAMBDA (n:nat): 2 * n + 1)) = square(n + 1) + +Da_2: PROPOSITION 6 * sum(n,square) = (n*(n+1)*(2*n+1)) + +Da_3: PROPOSITION sum(n,cube) = square(sum(n)) + +Da_4: PROPOSITION sum(n,LAMBDA (n:nat) : pow(2,n)) = pow(2,n+1) - 1 + +Da_5: LEMMA i * sum(n, f) = sum(n, (LAMBDA (n : nat) : i * f(n))) + +END th_Da + +th_Db : THEORY +BEGIN + importing th_D + + geom(a: nat, n:nat) : RECURSIVE nat = + IF n = 0 + THEN 0 + ELSE pow(a, n-1) + geom(a, n-1) + ENDIF + MEASURE n + + geom_sum : THEOREM FORALL(a,n:nat): a > 1 IMPLIES (a-1) * geom(a,n) = pow(a, n)-1 +END th_Db diff --git a/assignment7/D.status b/assignment7/D.status new file mode 100644 index 0000000..668b813 --- /dev/null +++ b/assignment7/D.status @@ -0,0 +1,24 @@ + Proof summary for theory th_D + sum_TCC1..............................proved - complete [shostak](0.02 s) + sum_TCC2..............................proved - complete [shostak](-.00 s) + D_1...................................proved - complete [shostak](0.09 s) + D_2...................................proved - complete [shostak](0.09 s) + pow_TCC1..............................proved - complete [shostak](0.01 s) + pow_TCC2..............................proved - complete [shostak](-.01 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.20 s) + + Proof summary for theory th_Da + Da_1..................................proved - complete [shostak](0.13 s) + Da_2..................................proved - complete [shostak](0.28 s) + Da_3..................................proved - complete [shostak](0.23 s) + Da_4..................................proved - complete [shostak](0.06 s) + Da_5..................................proved - complete [shostak](0.06 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.77 s) + + Proof summary for theory th_Db + geom_TCC1.............................proved - complete [shostak](0.01 s) + geom_TCC2.............................proved - complete [shostak](0.01 s) + geom_sum..............................proved - complete [shostak](0.14 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.16 s) + +Grand Totals: 14 proofs, 14 attempted, 14 succeeded (1.13 s) diff --git a/assignment7/E.prf b/assignment7/E.prf new file mode 100644 index 0000000..38c0cb0 --- /dev/null +++ b/assignment7/E.prf @@ -0,0 +1,386 @@ +(th_E + (fac_TCC1 0 + (fac_TCC1-1 nil 3667132061 ("" (subtype-tcc) nil nil) nil nil)) + (fac_TCC2 0 + (fac_TCC2-1 nil 3667132061 ("" (termination-tcc) nil nil) nil nil)) + (thm_E_0 0 + (thm_E_0-1 nil 3667136110 + ("" (induct k) + (("1" (flatten) (("1" (assert) nil nil)) nil) + ("2" (skeep) + (("2" (split -1) + (("1" (expand fac 1 2) (("1" (assert) nil nil)) nil) + ("2" (case "j=0") + (("1" (expand fac 2) + (("1" (expand fac 2) + (("1" (assert 2) + (("1" (expand fac 2) + (("1" (assert 2) (("1" (grind 2) nil nil)) nil)) + nil)) + nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil) + ((= const-decl "[T, T -> boolean]" equalities nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (int_plus_int_is_int application-judgement "int" integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (fac def-decl "nat" th_E nil) (< const-decl "bool" reals nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil)) + shostak)) + (thm_E_1 0 + (thm_E_1-1 nil 3667132062 + ("" (induct k) + (("1" (assert) (("1" (grind) nil nil)) nil) + ("2" (skeep) (("2" (expand fac 1) (("2" (assert) nil nil)) nil)) + nil)) + nil) + ((mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) (<= const-decl "bool" reals nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (thm_E_2 0 + (thm_E_2-1 nil 3667133505 + ("" (induct k) + (("1" (expand fac) (("1" (assert) nil nil)) nil) + ("2" (skeep) + (("2" (lemma thm_E_0) + (("2" (inst -1 j) + (("2" (split -1) + (("1" (assert) nil nil) + ("2" (assert) + (("2" (case "j=0") + (("1" (expand fac 2) + (("1" (expand fac 2) (("1" (assert 2) nil nil)) nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (thm_E_0 formula-decl nil th_E nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) (<= const-decl "bool" reals nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (tfac_TCC1 0 + (tfac_TCC1-1 nil 3667133493 ("" (subtype-tcc) nil nil) nil nil)) + (tfac_TCC2 0 + (tfac_TCC2-1 nil 3667133493 ("" (termination-tcc) nil nil) nil nil)) + (lemma_E_3 0 + (lemma_E_3-1 nil 3667135000 + ("" (induct m) + (("1" (skeep) + (("1" (expand tfac) + (("1" (expand fac) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (expand tfac 1) + (("2" (inst -1 "j*n+n") + (("2" (replace -1 1) + (("2" (expand fac 1 2) (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (tfac def-decl "nat" th_E nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (th_E_4 0 + (th_E_4-1 nil 3667136822 + ("" (skeep) + (("" (lemma lemma_E_3) + (("" (inst -1 k 1) (("" (assert) nil nil)) nil)) nil)) + nil) + ((lemma_E_3 formula-decl nil th_E nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak)) + (fib_TCC1 0 + (fib_TCC1-1 nil 3667132061 ("" (subtype-tcc) nil nil) nil nil)) + (fib_TCC2 0 + (fib_TCC2-1 nil 3667132061 ("" (termination-tcc) nil nil) nil nil)) + (lem_E_Camil_1 0 + (lem_E_Camil_1-1 nil 3667137364 + ("" (induct i) + (("1" (skeep) + (("1" (expand tfib) + (("1" (expand fib) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (expand tfib 1) (("2" (postpone) nil nil)) nil)) nil)) + nil)) + nil) + nil shostak)) + (lem_E_Camil_2_TCC1 0 + (lem_E_Camil_2_TCC1-1 nil 3667140798 ("" (subtype-tcc) nil nil) nil + nil)) + (lem_E_Camil_2_TCC2 0 + (lem_E_Camil_2_TCC2-1 nil 3667140798 ("" (subtype-tcc) nil nil) nil + nil)) + (lem_E_Camil_2 0 + (lem_E_Camil_2-1 nil 3667137463 + ("" (induct i) + (("1" (skeep) (("1" (expand tfib) (("1" (propax) nil nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (case "j=0") + (("1" (assert) + (("1" (expand tfib) + (("1" (expand tfib) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (assert 2) + (("2" (expand tfib 2) + (("2" (inst -1 p (m+p)) + (("2" (replace -1 2) + (("2" (case "j=1") + (("1" (assert) + (("1" (expand fib 2) (("1" (assert) nil nil)) + nil)) + nil) + ("2" (assert 3) + (("2" (lift-if) + (("2" (assert) + (("2" (expand fib 3 3) + (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (skeep 1) (("3" (assert) nil nil)) nil) + ("4" (skeep 1) (("4" (assert) nil nil)) nil)) + nil) + ((real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fib def-decl "nat" th_E nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (IF const-decl "[boolean, T, T -> T]" if_def nil) + (tfib def-decl "nat" th_E nil) + (pred type-eq-decl nil defined_types nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (>= const-decl "bool" reals nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (int_minus_int_is_int application-judgement "int" integers nil)) + shostak)) + (thm_E_6 0 + (thm_E_6-1 nil 3667137014 + ("" (skeep) + (("" (lemma lem_E_Camil_2) + (("" (inst -1 i 1 1) + (("" (assert) + (("" (replace -1 1) + (("" (assert) + (("" (case "i=0") + (("1" (assert) + (("1" (expand fib 1) (("1" (propax) nil nil)) nil)) + nil) + ("2" (case "i=1") + (("1" (assert) + (("1" (expand fib 2) (("1" (propax) nil nil)) nil)) + nil) + ("2" (assert) + (("2" (expand fib 3 3) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((lem_E_Camil_2 formula-decl nil th_E nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (fib def-decl "nat" th_E nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + shostak))) + diff --git a/assignment7/E.pvs b/assignment7/E.pvs new file mode 100644 index 0000000..5f02082 --- /dev/null +++ b/assignment7/E.pvs @@ -0,0 +1,109 @@ +%%% NAME/LOGIN-ID Camil Staps / s4498062 +%%% ACKNOWLEDGMENTS: + +th_E: THEORY + +BEGIN + +%%% +%%% Standard development of iterative factorial-with-accumulator. +%%% Start with a "specification" of the factorial function. +%%% + +fac(n:nat): RECURSIVE nat = + IF n = 0 + THEN 1 + ELSE fac(n-1) * n + ENDIF + MEASURE n + +%%% +%%% A few simple facts about the factorial function. +%%% + +thm_E_0: LEMMA (FORALL (k:nat): k>=1 IMPLIES fac(k) < fac(k+1)) + +thm_E_1: THEOREM (FORALL (k:nat): 1 <= fac(k)) +thm_E_2: THEOREM (FORALL (k:nat): k <= fac(k)) + +%%% +%%% In tfac, below, all recursive calls are in the tail position. In operational terms, +%%% tfac "improves" fac because a no space is needed for a recursion stack. In other +%%% words, tfac is and instance of the "implementation model" for sequential execution. +%%% + +tfac(n:nat, m:nat): RECURSIVE nat = + IF n = 0 + THEN m + ELSE tfac(n - 1, m * n) + ENDIF + MEASURE n + +%%% +%%% We should prove, though, that tfac is equivalent to fac. They are not "equal" because, +%%% for one thing, tfac takes two arguments and fac takes only one. In fact, tfac(n, m) +%%% only computes fac(n) when m = 1. +%%% +%%% However, in trying to prove this, we run into a problem... +%%% In the inductive case, we'll get something like this: +%%% +%%% [-1] fac(J) = tfac(J, 1) +%%% |------------------------ +%%% [1] (J+1) * fac(J) = tfac(J, J+1) +%%% +%%% To complete the proof, we need to "distribute" J+1 outside fact. But attempting +%%% to prove this, for just "J+1" will fail. A _generalization_ is needed... +%%% + +lemma_E_3: LEMMA (FORALL (m:nat, n:nat): tfac(m, n) = n * fac(m)) + +%%% +%%% On the strength of this lemma, we can prove the correctness of tfac. + +th_E_4: THEOREM (FORALL (k:nat): fac(k) = tfac(k, 1)) + +%%% +%%% Below, we'll do the same standard development for iterative the Fibonacci function. +%%% Except this time, YOU have to find the appropriate lemma! Although there are several +%%% reasonable possibilities for the needed lemma, it is not easy to think of one. +%%% +%%% Remember that the lemma must GENERALIZE the desired result. +%%% + +fib(n:nat): RECURSIVE nat = + (IF n = 0 THEN 1 + ELSIF n = 1 THEN 1 + ELSE fib(n - 1) + fib(n - 2) + ENDIF) + MEASURE n + +%%% +%%% Tail-recursive version of fib. +%%% + +tfib(n:nat, m:nat, p:nat): RECURSIVE nat = + (IF n = 0 + THEN m + ELSE tfib(n - 1, p, p + m) + ENDIF) + MEASURE n + +%%% +%%% YOU will need to discover a nontrivial lemma to prove thm. +%%% Place your lemma just below, before thm_E_6. +%%% + +lem_E_Camil_2: LEMMA + (FORALL (i:nat, m:nat, p:nat): + tfib(i, m, p) = + IF i = 0 THEN m + ELSIF i = 1 THEN p + ELSE fib(i-2)*m + fib(i-1)*p + ENDIF) + +thm_E_6: THEOREM + (FORALL (i:nat): + tfib(i, 1, 1) = fib(i)) + +END th_E + diff --git a/assignment7/E.status b/assignment7/E.status new file mode 100644 index 0000000..5b939ed --- /dev/null +++ b/assignment7/E.status @@ -0,0 +1,19 @@ + Proof summary for theory th_E + fac_TCC1..............................proved - complete [shostak](0.02 s) + fac_TCC2..............................proved - complete [shostak](0.01 s) + thm_E_0...............................proved - complete [shostak](0.30 s) + thm_E_1...............................proved - complete [shostak](0.03 s) + thm_E_2...............................proved - complete [shostak](0.06 s) + tfac_TCC1.............................proved - complete [shostak](0.01 s) + tfac_TCC2.............................proved - complete [shostak](0.01 s) + lemma_E_3.............................proved - complete [shostak](0.06 s) + th_E_4................................proved - complete [shostak](0.03 s) + fib_TCC1..............................proved - complete [shostak](0.01 s) + fib_TCC2..............................proved - complete [shostak](0.01 s) + lem_E_Camil_2_TCC1....................proved - complete [shostak](0.01 s) + lem_E_Camil_2_TCC2....................proved - complete [shostak](0.02 s) + lem_E_Camil_2.........................proved - complete [shostak](0.31 s) + thm_E_6...............................proved - complete [shostak](0.06 s) + Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.97 s) + +Grand Totals: 15 proofs, 15 attempted, 15 succeeded (0.97 s) |