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

```