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

Re: [PVS-Help] Re: Dependent type related TCCs

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


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:

    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})].


> Thanks,
> -- Aditya Kanade. 
> Research Scholar, CSE, IIT Bombay.