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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] Re: Dependent type related TCCs*From*: Aditya Kanade <aditya@cse.iitb.ac.in>*Date*: Sat, 28 Feb 2004 16:29:02 +0530 (IST)*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 i1SAs8Re064436for <pvs-help@postal.csl.sri.com>; Sat, 28 Feb 2004 02:54:09 -0800 (PST)(envelope-from aditya@cse.iitb.ac.in)*Original-Received*: from mailgate-external2.sri.com (mailgate-external2.SRI.COM[128.18.85.102])by quarter.csl.sri.com (8.12.9/8.12.10) with SMTP id i1SAt56K029655for <pvs-help@csl.sri.com>; Sat, 28 Feb 2004 02:55:06 -0800*Original-Received*: (qmail 1368 invoked from network);28 Feb 2004 10:55:05 -0000*Original-Received*: from localhost (HELO mailgate-external2.SRI.COM) (127.0.0.1)by mailgate-external2.sri.com with SMTP; 28 Feb 2004 10:55:05 -0000*Original-Received*: from smtp2.iitb.ac.in ([203.199.81.149])by mailgate-external2.SRI.COM (SAVSMTP 3.1.2.35) with SMTP idM2004022802550407183for <pvs-help@csl.sri.com>; Sat, 28 Feb 2004 02:55:04 -0800*Original-Received*: (qmail 2661 invoked by uid 505); 28 Feb 2004 10:55:01 -0000*Original-Received*: from aditya@cse.iitb.ac.in by smtp2.iitb.ac.in by uid 502with qmail-scanner-1.16 (clamscan: 0.54. spamassassin: 2.54. Clear:. Processed in 2.405178 secs); 28 Feb 2004 10:55:01 -0000*Original-Received*: from unknown (HELO jeeves.cse.iitb.ac.in) (10.105.1.1)by smtp2.iitb.ac.in with SMTP; 28 Feb 2004 10:54:58 -0000*Original-Received*: from surya.cse.iitb.ac.in (surya.cse.iitb.ac.in[10.105.1.14])by jeeves.cse.iitb.ac.in (8.11.0/8.11.0) with ESMTP id i1SAswL04098for <pvs-help@csl.sri.com>; Sat, 28 Feb 2004 16:24:58 +0530*Original-Received*: from surya.cse.iitb.ac.in (surya.cse.iitb.ac.in [127.0.0.1])by surya.cse.iitb.ac.in (8.12.10/8.11.6) with ESMTP id i1SAx3ti009530for <pvs-help@csl.sri.com>; Sat, 28 Feb 2004 05:59:03 -0500*Original-Received*: from localhost (aditya@localhost)by surya.cse.iitb.ac.in (8.12.10/8.12.10/Submit) with ESMTP idi1SAx2K3009526for <pvs-help@csl.sri.com>; Sat, 28 Feb 2004 16:29:03 +0530*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

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? Thanks, -- Aditya Kanade. Research Scholar, CSE, IIT Bombay. Hi, For the following theory: t1: THEORY BEGIN t: TYPE = [# v: setof[nat], x: [nat -> {n: nat | member(n, v)}] #] a: VAR t f(a): t = (# v := union(a`v, {n: nat | n = 1}), x := a`x #) END t1 following TCC gets generated, which can easily be discharged using typepred. f_TCC1: OBLIGATION FORALL (a: t): FORALL (x1: nat): member[nat](a`x(x1), union[nat](a`v, {n: nat | n = 1})); On the other hand, for the following theory where the range of x is now a set, t2: THEORY BEGIN t: TYPE = [# v: setof[nat], x: [nat -> setof[{n: nat | member(n, v)}]] #] a: VAR t f(a): t = (# v := union(a`v, {n: nat | n = 1}), x := a`x #) END t2 following TCC gets generated, which is unprovable. f_TCC1: OBLIGATION FORALL (a: t): FORALL (x1: nat, x: nat): member[nat](x, a`v) IFF member[nat](x, union[nat](a`v, {n: nat | n = 1})); Here, just the range of "f" is being extended (as in earlier case). Why is it generating this TCC? Shouldn't a TCC with "IF" instead of "IFF" be generated for the above case? -- Aditya Kanade. Research Scholar, CSE, IIT Bombay.

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