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

*To*: Sjaak Smetsers <s.smetsers@xxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] How to continue this proof?*From*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Date*: Wed, 24 Oct 2012 09:08:12 -0500*Accept-language*: en-US*Acceptlanguage*: en-US*Cc*: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*In-reply-to*: <002a01cdb112$0ccc3690$2664a3b0$@science.ru.nl>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: Ac2x8QFcaeQCgpoqQlGxONPx3oRFTg==*Thread-topic*: [PVS-Help] How to continue this proof?*User-agent*: Microsoft-MacOutlook/14.12.0.110505

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

- Prev by Date:
**Re: [PVS-Help] PVS on OSX mountain lion** - Next by Date:
**[PVS-Help] problem with theory interpretations in PVS** - Previous by thread:
**Re: [PVS-Help] How to continue this proof?** - Next by thread:
**[PVS-Help] PVS on OSX mountain lion** - Index(es):