**TUTORIAL 3**
Task 1.
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
BEGIN
%%% Declarations of propositional variables
p,q,r: bool;
%%% 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))
END hw1_prop
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
BEGIN
%%% 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))))
END hw1_fo
hw1_num: THEORY
**TUTORIAL 4**
Task 1
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.
BEGIN hw1_num
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))
END hw1_num
hw1_induction : THEORY
BEGIN
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
MEASURE n
% 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
MEASURE n
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))
END hw1_induction |