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

*To*: David Coppit <sri@coppit.org>*Subject*: Re: [PVS-Help] Confused about proving extensionality of overriddenfunctions*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Fri, 23 Sep 2005 12:00:21 -0700*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <Pine.BSF.4.63.0509231143390.96138@www.provisio.net>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <Pine.BSF.4.63.0509231143390.96138@www.provisio.net>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla Thunderbird 0.7.3 (X11/20040803)

David Coppit wrote: > Hello all, > > I'm trying to learn PVS, and need a gentle push in the right direction. > > Assume this specification for a function-based implementation of stacks: > > stacks: THEORY BEGIN > > stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #] > empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #) > > push(x: int, s:stack): { s: stack | s`size>=1 } = > (# size:=s`size+1, > elements:=s`elements WITH [(s`size):=x] #) > > pop(s:stack | s`size>=1): stack = > (# size:=s`size-1, > elements:=s`elements WITH [(s`size-1):=0] #) > > % Hack for now > all_above_are_zero: LEMMA > FORALL (s: stack, x: int): x>s`size => s`elements(x) = 0 > > push_pop: THEOREM > FORALL (s: stack, x: int): pop(push(x, s))=s > > END stacks > > When proving push_pop, I start with > > (skolem!) > (expand* "push" "pop") > (lemma "all_above_are_zero" ("s" "s!1" "x" "s!1`size")) > (assert) > (apply-extensionality) > > This results in the sequent: > > [-1] s!1`elements(s!1`size) = 0 > |------- > {1} s!1`elements WITH [(s!1`size) := 0] = s!1`elements > [2] (# size := s!1`size, > elements := s!1`elements WITH [(s!1`size) := 0] #) > = s!1 > > Question #1: Now what? Shouldn't formula -1 be enough for formula 1? > Yes, but you need to apply extensionality once more (since the equality in {1} is between two functions). > Question #2: I tried writing all_above_are_zero as an axiom, but didn't > know how to utilize it in my proof. Is there some way to "use" an axiom? > An axiom can be used like any other lemma/theorem in your theory. Any proof command that takes lemma or theorem names as parameters also accepts axiom names. For example, you can do (lemma "all_above_are_zero" ...) if all_above_are_zero is stated as an axiom. > Question #3: How do I rewrite my axiom so that it is higher-level, stating > that all stacks are either the empty stack, or derived from it? > The problem here is that "all_above_are_zero" is not true in your theory, so turning it into an axiom will make the specification inconsistent. You can change the definition of type "stack" so that all stacks satisfy the constraint you want: stack: TYPE = { s: [# size: nat, elements: ARRAY[nat->int] #] | FORALL (x: nat): x > s`size => s`elements(x) = 0 } then there's no need for any axiom anymore. But you'll get more TCCs to show that empty/push/pop are type correct. Another approach is to define a subtype of well-formed stacks inductively (where well-formed means either empty, or obtained from empty by a sequence of push operations). You keep the original definition of stack then define a well-formed predicate by induction: well_formed(s: stack): INDUCTIVE bool = s = empty OR (EXISTS (s0: stack, x0: int): well_formed(s0) AND s = push(x0, s0)) Then you can define the type of well-formed stacks: good_stack: TYPE = { s: stack | well_formed(s) } and now you can prove a variant of all_above_are_zero: all_above_are_zero_var: LEMMA FORALL (s: good_stack, x: nat) : x > s`size => s`elements(x) = 0 Bruno > Thanks, > David > > _____________________________________________________________________ > David Coppit david@coppit.org > The College of William and Mary http://coppit.org/ > > "They have computers, and they may have other weapons of mass destruction." > Former Attorney General Janet Reno, speaking at LLNL of modern criminals > -- Bruno Dutertre | bruno@csl.sri.com CSL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

**References**:**[PVS-Help] Confused about proving extensionality of overriddenfunctions***From:*David Coppit <sri@coppit.org>

- Prev by Date:
**[PVS-Help] Confused about proving extensionality of overriddenfunctions** - Next by Date:
**Re: [PVS-Help] Confused about proving extensionality of overriddenfunctions** - Prev by thread:
**[PVS-Help] Confused about proving extensionality of overriddenfunctions** - Next by thread:
**Re: [PVS-Help] Confused about proving extensionality of overriddenfunctions** - Index(es):