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

Re: [PVS-Help] Induction on FSA


I have a few comments regarding your specification. First, since "lw" is a
finite_set you cannot directly apply (induct "lw"). I suspect that you
have used the induction schema "finite_induction" provided in the prelude.
However, that's not the easiest way to proceed. My second comment is that
when you write alfa(sy,lw)(ly), PVS implicitly adds a conversion from
lists to sets, since the membership predicate l(x), where l is a list and
x is an element, is not directly supported by lists. This adds unnecessary
complications to what you are trying to prove. You can use instead
FORALL(k:below(length(l)): Š nth(l,k) Š to refer to a particular element
of the list. Or, even better, the predefined predicates "every" and "some"
already defined for lists.
Finally, as it is explained in the slides, PVS provides a simple way to
prove inductive properties without the use of explicit induction (look for
the section on "induction-free induction").

I have simplified your problem to this one:

diego : THEORY

  s : VAR finite_set[nat]

  evens(s) : RECURSIVE { l: list[nat] | every(even?,l) } =
    IF empty?(s) THEN null
    ELSE cons(2*card(s),cons(2*choose(s),evens(sets.rest(s))))
  MEASURE card(s)

  n : VAR nat

  evens_is_sound : LEMMA

END diego

Notice the return type of evens. Because of this type, the proof of the
lemma is just (subtype-tcc). There is no free lunch, but almost. PVS
generates 4 TCCs, all of which are easily proven. I attach the pvs and prf
files to this message.

Hope that this helps,


Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234

On 2/28/13 7:44 PM, "Diego Martinoia" <diego.martinoia@xxxxxxxxx> wrote:

>Dear Cesar,
>First of all, thanks for your reply.
>I had seen already that slides set as part of the Nasa virtual machine
>material. The project you linked me is very huge and I have quite some
>difficulties into following it (there are so many files that I hardly
>can find the beginning).
>The problem is that my theory is very convoluted, and recursive
>functions call other functions. I am now trying to prove them "step by
>step", by defining the inner behavior as lemmas to be proved from the
>inside out.
>But still, I get stuck even in the simplest cases. For example, I have
>a function defined as (t_Label_STAR_y is just a list of t_Label_y
>elements, which is a datatype that can be either addMatrix_y or
>removeMatrix_y, a disjoint union):
>alfa(org: t_Strings, newAuth: finite_set[t_TripleString]):
>	  IF empty?(newAuth) THEN
>	     null
>	  ELSE
>	      %Add the Auth
>	      cons(addMatrixCons_y(choose(newAuth)),
>	      %Add the Belongs W.Bel(sub,org) <--> Y.Mat(sub, org, sk(sub,org))
>	      cons(addMatrixCons_y(
>		(# e1:= choose(newAuth)`e1, e2 := org, e3 :=
>skolem_generator_belongs(choose(newAuth)`e1, org) #)
>	      ),
>	      alfa_helper_joinCoalitionCons_w(org, rest(newAuth))))
>MEASURE card(newAuth)
>As you can see here, all I'm doing is appending addMatrix elements.
>This means that the list is either empty or composed only of addMatrix
>So I have tried to prove the lemma:
>jc_help: LEMMA
>(FORALL (sy: t_States_y, lw: t_Labels_w):
>	joinCoalition_w?(lw) IMPLIES (FORALL (ly: t_Labels_y): alfa(sy,
>lw)(ly) IMPLIES addMatrix_y?(ly))
>And yet, if I use induct on lw I get stuck, after some trivial
>passages, as I don't have anything left quantified and I start "going
>down" in the recursion manually:
>{-1}  list2set(cdr(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH))))
>              (ly!1)
>  |-------
>[1]   null?(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH))
>{2}   null?(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH)))
>[3]   addMatrix_y?(ly!1)
>and on and on cdr(cdr(cdr( ...
>2013/2/26 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>:
>> Diego,
>> The technique depends on what you want to prove and how you defined your
>> recursive function. Please, take a look at this talk on recursion and
>> induction in PVS.
>> uction.pdf
>> A concrete example, which deals with a state automaton, can be found
>>   http://shemesh.larc.nasa.gov/people/cam/AirSTAR/
>> Hope that this helps,
>> Cesar
>> --
>> Cesar A. Munoz                             NASA Langley Research Center
>> Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
>> http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
>> Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
>> On 2/24/13 10:04 AM, "Diego Martinoia" <diego.martinoia@xxxxxxxxx>
>>>Dear all,
>>>I'm quite new to PVS, and I was wondering if anyone could help me:
>>>I am working on a theory that involves simulating finite state
>>>automaton, and I have to prove a lemma in the form:
>>>s1 = terminal ( s2, lx )
>>>where s1 and s2 are states of the automaton, lx is a list of inputs
>>>(the labels on the automaton arches) and terminal is a recursive
>>>function defined as:
>>>terminal(s, lx) =
>>>IF null?(lx) THEN s
>>>terminal (next (s, car(lx)) , cdr(lx))
>>>where next is the single step function of the automaton, car and cdr
>>>are the list accessors for the head and the rest of the list.
>>>Unfortunately, I can't figure out which commands allow me to deal with
>>>this kind of structure. I have tried launching a
>>>induct-and-simplify "lx"
>>>command, as well as similar form involving using the name and
>>>generalize-skolem-constants commands to have more possible argument
>>>for the induction rules, but I always fail.
>>>Anyone has any suggestions on the matter?
>>>Diego Martinoia

Attachment: diego.pvs
Description: diego.pvs

Attachment: diego.prf
Description: diego.prf