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

Re: [PVS-Help] Induction on FSA



Cesar,

Thanks for your help. I understand now that (rightfully) PVS doesn't
know how to induct on my custom structures (i.e. it doesn't have the
right induction scheme).

I have changed my strategy and, using the naturals weak induction
scheme as example, I'm building my own scheme for my personal needs.

I have two more questions for you. The first one is if you know if
it's possible to have syntax highlighting also in the prover view, not
just in the theory editing (i.e. after you M-x pr).

The second one, more related to the topic, is somehow linked to
partial functions. Suppose I have a function such that returns a
default value if the argument doesn't respect a predicate, otherwise
returns the value linked to the predicate:

y0: T2
P : [T1, T2 -> boolean]

f ( x: T1) : T2 =
IF (EXISTS (y: T2): P(x,y)) THEN
y
ELSE
y0
ENDIF

How can I specify this in PVS? The return value of y is outside the
scoping of the EXISTS, and so PVS doesn't know where to look for it. I
know this could be solved by changing P into [T1 -> T2] and returning
P(x), but this would be a problem for my setup. Is there a way to
preserve P as is?

Thanks,

Diego

2013/3/1 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>:
> 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"
> 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
> 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,
>>
>>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]):
>>RECURSIVE t_Label_STAR_y =
>>         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))))
>>         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,
>>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( ...
>>
>>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
>>>>
>>>
>