[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.)

Thanking you in advance,

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