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

[PVS-Help] Re: Dependent type related TCCs



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.