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

*To*: chao qin <Chao.Qin@loria.fr>, pvs-help@csl.sri.com*Subject*: Re: can you give me command to prove test??*From*: "Ricky W. Butler" <R.W.Butler@larc.nasa.gov>*Date*: Mon, 07 Jul 2003 08:37:18 -0400*In-Reply-To*: <3F06EF8A.7050108@loria.fr>*Sender*: pvs-help-owner@csl.sri.com

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

**References**:**can you give me command to prove test??***From:*chao qin <Chao.Qin@loria.fr>

- Prev by Date:
**pb with measure in a recursive function** - Next by Date:
**Re: pb with measure in a recursive function** - Prev by thread:
**Re: can you give me command to prove test??** - Next by thread:
**License as ASCII text?** - Index(es):