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

*To*: Aditya Kanade <aditya@cse.iitb.ac.in>*Subject*: Re: [PVS-Help] Re: Dependent type related TCCs*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Sat, 28 Feb 2004 10:48:48 -0800*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <Pine.LNX.4.58.0402281618040.9247@surya.cse.iitb.ac.in>*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>*Original-Received*: from quarter.csl.sri.com (mx0.csl.sri.com [130.107.1.30])by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id i1SIlpRe072905for <pvs-help@postal.csl.sri.com>; Sat, 28 Feb 2004 10:47:51 -0800 (PST)(envelope-from bruno@sdl.sri.com)*Original-Received*: from sdl.sri.com (box.csl.sri.com [130.107.15.210])by quarter.csl.sri.com (8.12.9/8.12.10) with ESMTP id i1SImm6K016837;Sat, 28 Feb 2004 10:48:52 -0800*References*: <Pine.LNX.4.58.0402281618040.9247@surya.cse.iitb.ac.in>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3.1) Gecko/20030425

Aditya Kanade wrote: > Hi, > > This is regarding my earlier question. I've tried to construct a simpler > example based on the hunch that the TCC is generated because of use of > setof type constructor, which is interpretated as a predicate [T->bool]. > Please see if my interpretation is correct. > > <interpretation> > > PVS interpretes setof[T] as a predicate [T->bool]. So it becomes > inevitable to prove that the domains are equal, i.e., it leads to the > equality (casted as IFF) TCC on the type of set. In our case, we need to > prove equality of a`v with union(a`v,{n:nat|n=1}), which is unprovable. So > whenever we use setof as a type constructor on a depedent type, we would > face this problem. > > > For example, t3:theory's TCC requires us to prove that > member(a`x,union{a`v,{n:nat|n=1}), which is easily provable (by typepred). > > t3: THEORY > BEGIN > t: TYPE = [# v: setof[nat], x: [{n: nat | member(n, v)}] #] > a: VAR t > f(a): t = (# v := union(a`v, {n: nat | n = 1}), x := a`x #) > END t3 > > > In t4:theory's TCC, we need to prove that a`x has same type as that of x > which is setof[union(a`v, {n: nat | n = 1}]. On the other hand, declared > type of a`x is setof[{n: nat | member(n, v)}]. So we've to prove that > [a`v->bool] and [union(a`v,{n:nat|n=1})->bool] are equal. This leads > to proof obligation that a`v and union(a`v,{n:nat|n=1}) are equal. This > cannot be proven. > > t4: THEORY > BEGIN > t: TYPE = [# v: setof[nat], x: setof[{n: nat | member(n, v)}] #] > a: VAR t > f(a): t = (# v := union(a`v, {n: nat | n = 1}), x := a`x #) > END t4 > > > Thus, if sets are interpretated as sets then the subtype TCC would lead to > "implication" (subtype TCC) instead of "double-implication" (equality > TCC?), whereas the interpretation as a "predicate" generates this subtype > TCC (which is probably unnecessary in the given context). > > </interpretation> > > If this is correct, then can someone suggest a remedy over it? Is there > any other reason behind this TCC? Is it inevitable? In that case, are we > required to write some axioms/theories to get around this? > Hi, A trick that works in these situations is to replace set[(v)] by { s: set[nat] | subset?(s, v) }. set[(v)] is a shorter way or writing setof[{n: nat | member(n, v)}]. In theory t4 above, that would give: t4: THEORY BEGIN t: TYPE = [# v: setof[nat], x: { s: set[nat] | subset?(s, v) } #] a: VAR t f(a): t = (# v := union(a`v, {n: nat | n = 1}), x := a`x #) END t4 and there should be no problem showing the tcc. If you want to keep the type t as defined before, then you can change the definition of f(a) by converting (a`x) to the expected type, i.e., set[(union(a`v, {n: nat | n = 1})]. Bruno > Thanks, > -- Aditya Kanade. > Research Scholar, CSE, IIT Bombay.

**References**:**[PVS-Help] Re: Dependent type related TCCs***From:*Aditya Kanade <aditya@cse.iitb.ac.in>

- Prev by Date:
**[PVS-Help] Re: Dependent type related TCCs** - Next by Date:
**[PVS-Help] the proof of recursive process** - Prev by thread:
**[PVS-Help] Re: Dependent type related TCCs** - Next by thread:
**[PVS-Help] Dependent type related TCCs** - Index(es):