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

Re: [PVS-Help] Pvs sets types



Kuijpers, T.J.H. wrote:
> Hello,
> 
> I try to prove a very simple conjecture w.r.t. sets and types.
> 
> The following is a part of the pvs theory:
> 
> <...>
> 
> % Definition 2.2
> 
>   setofNat: TYPE+ = {x:setof[nat] | NOT (subset?(x, singleton[nat](0))
> AND subset?(singleton[nat](0),x))}	
>   
>   N:  TYPE+ = {tE2Rp0, tE2Rp1, tE2Rp2, tR2Pp0, tR2Pp1, tR2Pp2, t0p0,
> t0p1, t0p2, t3p2, t4p2, t1p0, t1p1, t2p0, t2p1, t5p2, tP2Rp0, tP2Rp1,
> tP2Rp2, tR2Ep0, tR2Ep1, tR2Ep2, g0p2, c0p2}
> % finite, non-empty set of nodes (N = T union G union L)
> 
>   n1,n2,n3 : N
>   disj: AXIOM n1 /= n2 AND n1 /= n3 AND n2 /= n3
> 
>   T:  TYPE+ = {x:N | x /= g0p2 AND x /= c0p2} 
>   G:  TYPE+ = {x:N | x = g0p2}
>   L:  TYPE+ = {x:N | x = c0p2}
>   Ln: TYPE+ = [L -> setof[N]]			 			
>   Gn: TYPE+ = [G -> setof[N]]
> 
>   <...>
> 
> 
>   dynamicSystem: TYPE+ = [# 		
>     t:setof[T],
>     g:setof[G],
>     l:setof[L],
>     ln:Ln,
>     gn:Gn,
>     <...>
>   #]
>  
> ds: dynamicSystem = (#
>       t  := LAMBDA (t:T): TRUE,
>       g  := LAMBDA (g:G): TRUE,
>       l  := LAMBDA (l:L): TRUE,
>       ln := LAMBDA (l:L): COND l=c0p2 -> {x:N | x = t3p2 OR x = t4p2},
> ELSE -> emptyset ENDCOND,
>       gn := LAMBDA (g:G): COND g=g0p2 -> {x:N | x = t0p2 OR x = c0p2},
> ELSE -> emptyset ENDCOND,
>       <...>				   
>  #)
> 
> 
> % -1-
>   ancRel(ds:dynamicSystem)(n1:N, n:N): INDUCTIVE boolean =
> 
>     (member(n,ds`g) AND member(n1,ds`gn(n))) OR (member(n,ds`l) AND
> member(n1,ds`ln(n))) OR						
>     (EXISTS (n2:N): ancRel(ds)(n1,n2) AND ancRel(ds)(n2,n))
> 
> 
>   anc(ds:dynamicSystem)(n:N): setof[N] = LAMBDA(n1:N): ancRel(ds)(n1,n)
>    
> 
> % --- Tests ---
> 
> testAnc: CONJECTURE anc(ds)(tE2Rp2) = emptyset 
> 
> <...>
> 
> To prove the conjecture testAnc I need information about tE2Rp2.
> Unfortunatey, using typepred I don't get any further and I do not know
> how to prove this in any other way. 
> Has anyone a suggestion? Thanks in advance.
> 
> Best regards,
> Thijs
> 
> 

Thijs,

There are type problems with your specifications. The typechecker
will generate many TCCs, including

    FORALL (x: N): x = c0p2

or FORALL (x: N): x = g0p2

Both are obviously false. These TCCs come from the definition of ancRel:
you apply ds`ln and ds`gn to a variable n of type N but ds`ln and ds`gn
are of type [L -> setof[N]] and [G -> setof[N]], respectively.

There's also a type mismatch in "member(n, ds`g)" and "member(n, ds`l)"
but PVS will automatically apply a conversion in this case.



I've rewritten the spec as follows to fix these problems:

kuijpers: THEORY
   BEGIN

   N: TYPE = {
	tE2Rp0, tE2Rp1, tE2Rp2, tR2Pp0, tR2Pp1, tR2Pp2,
	t0p0, t0p1, t0p2, t3p2, t4p2, t1p0, t1p1, t2p0, t2p1, t5p2,
	tP2Rp0, tP2Rp1, tP2Rp2, tR2Ep0, tR2Ep1, tR2Ep2, g0p2, c0p2
   }

   x: VAR N

   T(x): bool = x /= g0p2 AND x /= c0p2
   G(x): bool = x = g0p2
   L(x): bool = x = c0p2
   Ln: TYPE = [N -> setof[N]]
   Gn: TYPE = [N -> setof[N]]

   dynamicSystem: TYPE+ = [#
     t: setof[N],
     g: setof[N],
     l: setof[N],
     ln: Ln,
     gn: Gn
   #]

   ds: dynamicSystem = (#
       t  := T,
       g  := G,
       l  := L,
       ln := LAMBDA (l: N): COND l = c0p2 -> {x | x = t3p2 OR x = t4p2},
                            ELSE -> emptyset ENDCOND,
       gn := LAMBDA (g: N): COND g=g0p2 -> {x | x = t0p2 OR x = c0p2},
                            ELSE -> emptyset ENDCOND
   #)

   ancRel(ds:dynamicSystem)(n1:N, n:N): INDUCTIVE boolean =
         (member(n,ds`g) AND member(n1,ds`gn(n)))
      OR (member(n,ds`l) AND member(n1,ds`ln(n)))
      OR (EXISTS (n2:N): ancRel(ds)(n1,n2) AND ancRel(ds)(n2,n))


   anc(ds:dynamicSystem)(n:N): setof[N] = LAMBDA (n1:N): ancRel(ds)(n1,n)

   testAnc: CONJECTURE anc(ds)(tE2Rp2) = emptyset

   END kuijpers



Then to prove testAnc, you need to use the induction axioms associated
with the definition of ancRel. You can see these axioms by using
the command "prettyprint-expanded":

   ancRel_weak_induction: AXIOM
     FORALL (ds: dynamicSystem, P: [[N, N] -> boolean]):
       (FORALL (n1, n: N):
          (member(n, ds`g) AND member(n1, ds`gn(n))) OR
           (member(n, ds`l) AND member(n1, ds`ln(n))) OR
            (EXISTS (n2: N): P(n1, n2) AND P(n2, n))
           IMPLIES P(n1, n))
        IMPLIES (FORALL (n1, n: N): ancRel(ds)(n1, n) IMPLIES P(n1, n));

   ancRel_induction: AXIOM
     FORALL (ds: dynamicSystem, P: [[N, N] -> boolean]):
       (FORALL (n1, n: N):
          (member(n, ds`g) AND member(n1, ds`gn(n))) OR
           (member(n, ds`l) AND member(n1, ds`ln(n))) OR
            (EXISTS (n2: N):
               (ancRel(ds)(n1, n2) AND P(n1, n2)) AND
                ancRel(ds)(n2, n) AND P(n2, n))
           IMPLIES P(n1, n))
        IMPLIES (FORALL (n1, n: N): ancRel(ds)(n1, n) IMPLIES P(n1, n));


The proof of testAnc is then as follows: apply-extensionality and
expand "anc" to get something like

   |-------
{1}   ancRel(ds)(x!1, tE2Rp2) = emptyset(x!1)


Then show that "ancRel(ds)(n1, n) implies n /= tE2Rp2" using
one of the induction axioms, e.g.,
   (use "ancReal_weak_induction"
	("ds" "ds" "P" "lambda (n1:N, n: N): n /= tE2Rp2"))

It should be easy to finish the proof after that.

Bruno