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

[PVS-Help] Dependent type related TCCs



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.