# Trivial proofs and set lemmas

I seem to be having some difficulty in getting PVS to prove correct
a simple test using the built-in 'set' type.

When I apply GRIND to 'proof2' in this case, I get 2 subgoals, one
of which is as follows:

Trying repeated skolemization, instantiation, and if-lifting,
this yields  2 subgoals:
proof2.1:

{-1}  (intersection(f!1, emptyset) = emptyset)
{-2}  (union(f!1, emptyset) = f!1)
{-3}  f!1(v!1)
|-------
{1}   (union(remove(v!1, f!1), add(v!1, emptyset)) = f!1)

Rule?

Firstly, using the lemma "intersection_empty" in the theory "sets_lemmas"
why isn't {-1} trivially true? After being unable to use this lemma with
the USE proof command, I attemped to prove it correct by using EXPAND:

Rule? (expand "intersection")
Expanding the definition of intersection,
this simplifies to:
proof2.2:

{-1}  (({x: typ | member(x, f!1) AND member(x, emptyset)}) = emptyset)
[-2]  (union(f!1, emptyset) = f!1)
[-3]  f!1(v!1)
|-------
{1}   (({x: typ |
member(x, remove(v!1, f!1)) AND member(x, add(v!1, emptyset))})
= emptyset)

Rule? (grind)
...............
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
proof2.2:

{-1}  (({x: typ | FALSE}) = emptyset)
[-2]  (union(f!1, emptyset) = f!1)
[-3]  f!1(v!1)
|-------
{1}   (({x: typ | (NOT (v!1 = x) AND f!1(x)) AND v!1 = x}) = emptyset)

Rule? (expand "emptyset")
Expanding the definition of emptyset,
this simplifies to:
proof2.2:

{-1}  (({x: typ | FALSE}) = ({x: typ | FALSE}))
{-2}  (union(f!1, {x: typ | FALSE}) = f!1)
[-3]  f!1(v!1)
|-------
{1}   (({x: typ | (NOT (v!1 = x) AND f!1(x)) AND v!1 = x}) =
({x: typ | FALSE}))

Rule?

Surely {-1} must be trivially true at this stage? (I have included the full
PVS file below for reference.)

Malcolm Dowse
(Computer Science Dept., Trinity College Dublin, Ireland)

---

settest  % [ parameters ]
: THEORY

BEGIN

% ASSUMING
% assuming declarations
% ENDASSUMING

typ: TYPE
sys: TYPE = [set[typ], set[typ], set[typ]]
f, a, b: VAR set[typ]
v: VAR typ

Func(f, a, b, v): sys = (f, remove(v, a), add(v,b))

preFunc(f, a, b, v): bool = (member(v,f) & member(v, a) &
NOT member(v,b))

validSys((f, a, b)): bool = ((intersection(a,b) = emptyset) &
(union(a,b) = f))

proof1: CONJECTURE FORALL f, a, b, v:
(validSys((f,a,b)) AND preFunc(f,a,b,v)) =>
(validSys(Func(f,a,b,v)))

proof2: CONJECTURE FORALL f,v:
(validSys((f,f,emptyset)) AND preFunc(f,f,emptyset,v)) =>
(validSys(Func(f,f,emptyset,v)))

proof3: CONJECTURE FORALL f:
(intersection(f, emptyset) = emptyset)

END settest