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

Re: can you give me command to prove test??



Chao,
      Here are some slides we use in our PVS class on how to prove theorems
involving sets.


Sets In PVS

   * It is important to bear in mind that a set is just a predicate (i.e.
         a function into bool):

       letters: TYPE = {a,b,c,d,e,f}
       S: set[letters]

   is just a function that maps each of the elements of the domain to
   true or false:

        a --> TRUE
        b --> FALSE
        c --> TRUE
        d --> TRUE
        e --> TRUE
        f --> FALSE

   * The above set is specified in PVS as follows:

        (LAMBDA (x: letters): (x=a) OR (x=c) OR (x=d) OR (x=e))

   * Alternatively, one could write:

        { x: letters | (x=a) OR (x=c) OR (x=d) OR (x=e) }

   * BUT, there is no PVS set constructor analogous to { a, c, d, e }.


Subset? Illustrated


   |-------
\{1\}    subset?(B, C)

Rule? {\color{blue}(expand "subset?" )}

   |-------
\{1\}    (FORALL (x: int): member(x, B) => member(x, C))

Rule? {\color{blue}(SKOLEM!)}

   |-------
\{1\}    member(x!1, B) => member(x!1, C)

Rule? {\color{blue}(expand "member" )}

   |-------
\{1\}    (B(x!1) => C(x!1))



Auto Rewriting


    |-------------
    [1]    factorial(12) = ...

Rule? {\color{blue}(AUTO-REWRITE "factorial")}

Rule? {\color{blue}(ASSERT)}

factorial rewrites factorial(0) to 1
factorial rewrites factorial(1) to 1
factorial rewrites factorial(2) to 2
factorial rewrites factorial(3) to 6
factorial rewrites factorial(4) to 24
factorial rewrites factorial(5) to 120
factorial rewrites factorial(6) to 720
factorial rewrites factorial(7) to 5040
factorial rewrites factorial(8) to 40320
factorial rewrites factorial(9) to 362880
factorial rewrites factorial(10) to 3628800
factorial rewrites factorial(11) to 39916800
factorial rewrites factorial(12) to 479001600




Set Union/Intersection Illustrated


x in B \cup C  = union(B, C)(x) = B(x) OR C(x)

x in B \cap C  = intersection(B, C)(x) = B(x) AND C(x)

Thus operations on sets can be reduced to propositional formulas
by set membership, i.e.

   * union(B, C) is a function
   * union(B, C)(x) is a propositional formula!


The reduction can be facilitated through use of

    (AUTO-REWRITE-THEORY "sets[T]")

which installs an entire theory as auto-rewrites, or

    (INSTALL-REWRITES :DEFS T)}

which installs all the definitions used directly or indirectly in the
original statement as auto-rewrite rules

AUTO-REWRITE-THEORY "sets[T]"



\{-1\}    A!1 = C!1
   |-------
\{1\}    intersection(union(A!1, B!1), union(C!1, B!1)) = union(A!1, B!1)

Rule? (apply-extensionality  :hide? t)

[-1]    A!1 = C!1
   |-------
\{1\}    intersection(union(A!1, B!1), union(C!1, B!1))(x!1) = union(A!1, 
B!1)(x!1)

Rule? (AUTO-REWRITE-THEORY "sets[T]")
Rewriting relative to the theory: sets[T], this simplifies to:

[-1]    A!1 = C!1
   |-------
[1]    intersection(union(A!1, B!1), union(C!1, B!1))(x!1) = union(A!1, 
B!1)(x!1)



AUTO-REWRITE-THEORY "sets[T] (cont.)"


Rule? (ASSERT)
member rewrites member(x!1, A!1) to  A!1(x!1)
member rewrites member(x!1, B!1) to  B!1(x!1)
union rewrites union(A!1, B!1)(x!1) to  A!1(x!1) OR B!1(x!1)
member rewrites member(x!1, union(A!1, B!1)) to  A!1(x!1) OR B!1(x!1)
member rewrites member(x!1, C!1) to  C!1(x!1)
union rewrites union(C!1, B!1)(x!1) to  C!1(x!1) OR B!1(x!1)
member rewrites member(x!1, union(C!1, B!1))
   to  C!1(x!1) OR B!1(x!1)
intersection rewrites intersection(union(A!1, B!1), union(C!1, B!1))(x!1)
   to  (A!1(x!1) OR B!1(x!1)) AND (C!1(x!1) OR B!1(x!1))

[-1]    A!1 = C!1
   |-------
\{1\}    ((A!1(x!1) OR B!1(x!1)) AND (C!1(x!1) OR B!1(x!1)))
           = (A!1(x!1) OR B!1(x!1))

  an easily proved propositional formula (i.e. use (GROUND))


RECOMMENDATION:


    (AUTO-REWRITE-THEORY "sets[T]" :exclude "choose")

    (GRIND :exclude "choose")

    (INSTALL-REWRITES :DEFS T :EXCLUDE "choose")


Set equality


   * To prove that two sets are equal we must use function
         extensionality:

             f = g  IFF   FORALL x: f(x) = g(x)

        because sets are just functions into bools (i.e. predicates)
   * The PVS command (APPLY-EXTENSIONALITY) will do the trick
   * Though you will probably want to type TAB E instead.


Set equality: Example

           A: set[posint] = { x: posint | (x=1) OR (x=2) OR (x=3) }

          ill_ext: LEMMA A = add(1,add(2,singleton(3)))


ill_ext :

   |-------
1    A = add(1, add(2, singleton(3)))

Rule? (APPLY-EXTENSIONALITY :HIDE? T)

   |-------
1    A(x!1) = add(1, add(2, singleton(3)))(x!1)

Rule? (AUTO-REWRITE-THEORY "sets[posint]")

   |-------
[1]    A(x!1) = add(1, add(2, singleton(3)))(x!1)

Rule? (EXPAND "A")

   |-------
1    (((x!1 = 1) OR (x!1 = 2) OR (x!1 = 3))
            = add(1, add(2, singleton(3)))(x!1))


Set equality: Example (cont.)


Rule? (ASSERT)
singleton rewrites singleton(3)(x!1)
   to  x!1 = 3
member rewrites member(x!1, singleton(3))
  to  x!1 = 3
add rewrites add(2, singleton(3))(x!1)
   to  2 = x!1 OR x!1 = 3
member rewrites member(x!1, add(2, singleton(3)))
   to  2 = x!1 OR x!1 = 3
add rewrites add(1, add(2, singleton(3)))(x!1)
   to  1 = x!1 OR 2 = x!1 OR x!1 = 3
Simplifying, rewriting, and recording with decision procedures,

   |-------
1    (((x!1 = 1) OR (x!1 = 2) OR (x!1 = 3)) = (1 = x!1 OR 2 = x!1 OR x!1 = 3))

Rule? (GROUND)
No change on: (GROUND)


What happened here?  Any suggestions?


Set equality: Example (cont.)

Rule? (IFF 1)
Converting top level boolean equality into IFF form,
Converting equality to IFF,
this simplifies to:
ill_ext :

   |-------
1    (x!1 = 1) OR (x!1 = 2) OR (x!1 = 3) IFF 1 = x!1 OR 2 = x!1 OR x!1 = 3

Rule? (GROUND)
Applying propositional simplification and decision procedures,
Q.E.D.





Big Warning


     T_100: TYPE = { n: nat | n <= 100 }

          { t: T_100 | t = 50 }


  is not the same as

          { n: nat | n = 50 }


  Why?



Big Warning (cont.)

Because

       T_100: TYPE = { n: nat | n <= 100 }

       { t:T_100 | t = 50 }  ??  { n: nat | n = 50 }


is equivalent to:

       T_100: TYPE = { n: nat | n <= 100 }

       (LAMBDA (t:T_100): t = 50)  ??  (LAMBDA (n: nat): n = 50)


  THE DOMAINS ARE NOT EQUAL!


Big Warning (cont.)

If you give PVS

       T_100: TYPE = { n: nat | n <= 100 }

       ll: LEMMA {t:T_100 | t = 50} = {n: nat | n = 50}

it will recognize the domain mismatch and interpret this as

      ll :

        |-------
      {1}    {t: T_100 | t = 50} = restrict({n: nat | n = 50})

where restrict is defined in the prelude as:

        restrict [T: TYPE, S: TYPE FROM T, R: TYPE]: THEORY
         BEGIN

          f: VAR [T -> R]
          s: VAR S

          restrict(f)(s): R = f(s)
          CONVERSION restrict

         END restrict


This CONVERSION helps here, but will not help you when
you try something like ...


Big Warning (cont.)

     T_100: TYPE = {n: nat | n <= 100}

     lc: LEMMA card({t:T_100 | t = 50}) = card({n: nat | n = 50})


because this is really

     T_100: TYPE = {n: nat | n <= 100}

     lc: LEMMA card[T_100]({t:T_100 | t = 50}) = cardred[nat]({n: nat | n = 
50})


This will be clearer after we cover finite sets.

The Moral Of the Story


MORAL:  DEFINE SETS OVER THE PARENT TYPE UNLESS THERE IS A VERY GOOD REASON 
NOT TO.



USE

{ n: nat | P(n) AND n <= 100 }


RATHER THAN

     T_100: TYPE = { n: nat | n <= 100 }

     { t:T_100 | P(t) }



This will keep all the domains the same!


Some Thoughts About Sets in Type Theory



   * Type theory offers several advantages over set theory, not the least of
   which is that it avoids the classic paradoxes in an intuitive way.
   * Type checking uncovers errors
   * However, there are some disadvantages.
   * The most disturbing disadvantages are

       1 The emptyset is not unique (i.e. emptyset[T1] and
           emptyset[T2]) are not identical.
       2 There are different set operations for each basic element type.
           In other words, card[T1] is not the same function as
           card[T2].



More Thoughts About Sets in Type Theory

This can lead to some frustrating technical manipulations.
For example, the ``semantically-equivalent'' sets

                  {t:T | p(t) AND S(t)}

and
                   {t: (p) | S(t)}

are not the same in a formal sense.


   *  The first set is a function [T -> bool],
   * Whereas the second is a function [(p) -> bool].
   * Because they do not have the same domains, the
   APPLY-EXTENSIONALITY strategy will not show that they are the same,
   even though semantically they represent the same set.
   *  We recommend that one
   avoid mixing sets over a parent type with sets over a subtype of that
   parent type.

Rick
------------------------------------------------------------------------------------------


At 05:32 PM 7/5/03 +0200, chao qin wrote:
>Hi,everyone:
>
>I am just new beginner in PVS, I found the example in maillist ,but I 
>cann't prove it,after I used (grind) command, it need to prove :
>
>test :
>
>{-1}  b!1(x!1)
>  |-------
>{1}   a!1(x!1)
>
>
>I don't know how to do it,can you give me some advice. the follow is the 
>example given by John
>
>
>
>foo[T: TYPE]:THEORY
>BEGIN
>
>set1: TYPE = finite_set[T]
>set2: TYPE = {t: finite_set[T]| FORALL (s:set1): subset?(t,s)}
>
>a: VAR set1
>b: VAR set2
>
>test: LEMMA subset?(b,a)
>
>END foo
>
>You can then prove test from the type predicate on b.
>
>
>
>best regards
>
>
>