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

Re: [PVS-Help] How to continue this proof?



Sjaak,

As you have noticed, when you tried C-u M-x show-expanded-sequent, the
"map" in formula -1 and the "map" in formula 1 don't have the same
parameter type. In formula -1 you have

map[list[T],list[T]]

whereas in formula 1 you have

map[list[T],(cons?[T])]

The "map" in formula 1 comes from your definition "inject":

	inject(e:T)(l: list[T]): RECURSIVE list[list[T]] =
        CASES l OF
            null        : cons(cons(e,null),null),
            cons(h,t)   : cons(cons(e,l), map(LAMBDA(l2:list[T]):
cons(h,l2))(inject(e)(t)))
		ENDCASES
	MEASURE length(l)



PVS always infers the most restrictive type of an expression. For the
occurrence of "map" in "inject", the most restrictive type of the second
theory parameter happens to be a non-null list. In general this is what
you want. However, in some specifications, specially when you are dealing
with collection types,  the less restrictive type is preferable. There are
a few ways to address this issue. The simplest one is to explicitly
provide the type of "map" in "inject", e.g.,

	inject(e:T)(l: list[T]): RECURSIVE list[list[T]] =
        CASES l OF
            null        : cons(cons(e,null),null),
            cons(h,t)   : cons(cons(e,l),
map[list[T],list[T]](LAMBDA(l2:list[T]): cons(h,l2))(inject(e)(t)))
		ENDCASES
	MEASURE length(l)

The proof proceeds as you expect. If you don't want to provide the type of
map in the definition of inject, you have to be more careful when
providing the type parameters of your lemmas.

Regards,

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 10/23/12 7:32 AM, "Sjaak Smetsers" <s.smetsers@xxxxxxxxxxxxx> wrote:

>Dear Cesar, Rick
>
>I've attached the pvs and proof files. There are indeed some differences
>in
>the expanded sequences, but I is not clear to me how these can be avoided
>without adding too much type info. The steps in the proof seem quite
>trivial
>to me but they end in a situation from which I cannot proceed anymore. My
>question is actually more general: what is wrong in the proof (or in the
>definitions I've given)?
>
>Cheers,
>
>Sjaak
>
>-----Original Message-----
>From: MUNOZ, CESAR (LARC-D320) [mailto:cesar.a.munoz@xxxxxxxx]
>Sent: dinsdag 23 oktober 2012 1:07
>To: Sjaak Smetsers; pvs-help@xxxxxxxxxxx
>Subject: Re: [PVS-Help] How to continue this proof?
>
>Sjaak,
>
>What do you get when you issue the command C-u M-x show-expanded-sequent?
>My wild guest is that the two inject functions don't have the same type.
>
>Cesar
>
>
>On 10/19/12 10:24 AM, "Sjaak Smetsers" <s.smetsers@xxxxxxxxxxxxx> wrote:
>
>>Especially when dealing with lists, I now end then get stuck in a
>>situation like this:
>> 
>>[-1]  length[list[T]]
>>          (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
>>               inject(x!1)(cons2_var!1)))
>>       = 1 + length[T](cons2_var!1)
>>  |-------
>>[1]   1 +
>>       length[list[T]]
>>           (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
>>                inject(x!1)(cons2_var!1)))
>>       = 2 + length[T](cons2_var!1)
>> 
>>I don¹t understand why PVS is not able to derive 1 from -1. It seems as
>>if it considers the applications of map as different, but I do not see
>>why. But more annoyingly, there seems to way to continue. How should I
>>proceed? E.g. if I type (name-replace STUPIDTHING ³map(LAMBDA (l2:
>>list[T]): cons(cons1_var!1, l2), inject(x!1)(cons2_var!1))²) it will
>>replace just one of the map expressions by  STUPIDTHING.
>> 
>>Sjaak
>> 
>> 
>