Many of these examples are derived from Steven Johnson at the University of Indiana. These are propositional logic examples. First, do these the "hard way", using only the (SPLIT) and (FLATTEN) commands.
You can do these by trial and error. Don't. Please look at what PVS is doing and understand how it is applying the rules from the lecture. After that see how quickly you can dispatch them with (grind).
hw1_prop : THEORY
%%% Declarations of propositional variables
%%% PVS accepts many synonyms for "THEOREM" or "LEMMA"
P_0: CLAIM ((p => q) AND p) => q
P_1: COROLLARY NOT (p OR q) IFF (NOT p AND NOT q)
P_2: FORMULA (p => (q => r)) IFF (p AND q => r)
P_3: SUBLEMMA ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))
%%% The next is not a theorem. Try to prove it. You will get stuck.
P_4: THEOREM ((p OR q) AND r) => (p AND (q AND r))
Task 2. First-order examples. Once again, prove each formula the "hard way". In addition to (flatten) and (split), you can use (inst ) and (skolem ). Then go back and try (skosimp*) and (grind) on the harder ones.
hw1_fo : THEORY
%%% Declarations for first-order examples
U: TYPE+ % Arbitrary nonempty type
a,b,c: U % Constants of type U
x,y,z: VAR U % Variables of type U
P,Q,R: [U -> bool] % Predicate names
F_0: LEMMA (FORALL x: P(x)) => P(a)
F_1: LEMMA ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a)
%%% PVS allows empty types.
F_2: LEMMA (FORALL x: P(x)) => (EXISTS y: P(y))
F_3: LEMMA (FORALL x: P(x)) OR (EXISTS y: NOT P(y))
F_4: LEMMA NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x))
F_5: LEMMA (FORALL x: P(x)) AND (FORALL x: Q(x))
IFF (FORALL x: P(x) AND Q(x))
F_6: LEMMA (FORALL y: (EXISTS x: (P(x) AND Q(y)))) IMPLIES
(FORALL y: (EXISTS x: P(x)) AND Q(y))
%%% What's the easiest way to prove this one?
F_7: LEMMA (FORALL x: (EXISTS y: (P(x) AND Q(y))))
IFF (EXISTS y: (FORALL x: (P(x) AND Q(y))))
These are some simple examples with even and odd numbers. In addition to commands seen in the previous exercises, commands dealing with arithmetic reasoning are used below. Feel free to use (SKOSIMP*) and (GRIND) in addition to previous commands. In particular, LEMMA, EXPAND, REPLACE, SIMPLIFY. You can experiment with other commands to see if there are easier ways to do them.
m, n: VAR int
%%% Here is one way to introduce a new predicate.
%%% Give it a name and axiomatize its properties.
even_predicate: [int -> bool]
defn_even_predicate: AXIOM even_predicate(n) IFF (EXISTS m: n = 2 * m)
%%% Or we may give a definition.
even?(n):bool = EXISTS m: n = 2 * m
odd?(n):bool = EXISTS m: n = 2 * m + 1
%%% PVS knows about 0, but...
D_1a: PROPOSITION even?(0)
D_1b: PROPOSITION even?(42)
%%% The predicate formulation is more primitive and
%%% harder to work with, but is used in some cases
%%% Hint: Use Lemma to introduce defn_even_predicate,
%% and make sure you instantiate "n" properly.
D_2a: PROPOSITION FORALL n: even_predicate(n + n)
%%% It is usually preferable to work with the functional
%%% form, if you can.
D_3: PROPOSITION FORALL n: even?(n + n)
%%% In theorems, universal quantification is implicit
D_5: PROPOSITION even?(n) IMPLIES even?(n * n)
D_6: PROPOSITION odd?(n) IMPLIES odd?(n * n)
D_7: PROPOSITION even?(n) AND even?(m) IMPLIES even?(n + m)
%%% The theorem below cannot be proved with the rules we have. Try.
D_8: THEOREM FORALL n: (not even?(n) IMPLIES odd?(n))
hw1_induction : THEORY
n: VAR nat
f: VAR [nat->nat]
square(n:nat) : nat = n*n
% Defining recursive functions
sum(n): RECURSIVE nat =
IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF
% This is the one I did in lecture. It is also done in
% the PVS documentation.
% First, do it "the hard way" with (LEMMA "nat_induction")
% Then do (INDUCT "n")
% Then do (INDUCT-AND-SIMPLIFY "n")
F_1: THEOREM sum(n) = (n * (n + 1))/2
% This is a general-purpose summation function. Note that
% f is a higher-order parameter. This will sum f(i) for all
% i from 0 to n.
% id is a pre-defined identity function, so this does the same
% thing as the previous example.
sum(n,f) : RECURSIVE nat =
IF n = 0 THEN f(0) ELSE f(n) + sum(n - 1,f) ENDIF
F_2: THEOREM sum(n,id) = (n*(n+1))/2
% As in Lisp, LAMBDA is used to express functions without giving them %names.
Fa_1: PROPOSITION sum(n, (LAMBDA (n:nat): 2 * n + 1)) = square(n + 1)
Fa_2: PROPOSITION sum(n,square) = (n*(n+1)*(2*n+1))