# Re: [PVS-Help] Induction on FSA

```Diego,

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

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))))
ENDIF
MEASURE card(s)

n : VAR nat

evens_is_sound : LEMMA
every(even?,evens(s))

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

--
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,
>
>
>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]):
>RECURSIVE t_Label_STAR_y =
>	  IF empty?(newAuth) THEN
>	     null
>	  ELSE
>	      %Add the Belongs W.Bel(sub,org) <--> Y.Mat(sub, org, sk(sub,org))
>		(# e1:= choose(newAuth)`e1, e2 := org, e3 :=
>skolem_generator_belongs(choose(newAuth)`e1, org) #)
>	      ),
>	      alfa_helper_joinCoalitionCons_w(org, rest(newAuth))))
>	  ENDIF
>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
>elements.
>
>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,
>)
>
>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)))
>
>and on and on cdr(cdr(cdr( ...
>
>Suggestions?
>
>D.
>
>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.
>>
>>
>>
>>http://shemesh.larc.nasa.gov/PVSClass2012/pvsclass2012/lectures-printer/i
>>nd
>> uction.pdf
>>
>> A concrete example, which deals with a state automaton, can be found
>>here:
>>
>>   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>
>>wrote:
>>
>>>Dear all,
>>>
>>>Greetings.
>>>
>>>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
>>>ELSE
>>>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?
>>>
>>>Thanks,
>>>
>>>Diego Martinoia
>>>
>>

```

Attachment: diego.pvs
Description: diego.pvs

Attachment: diego.prf
Description: diego.prf