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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Expected type TCC*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Sun, 27 Apr 2008 01:47:17 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Jerome <jerome@cs.caltech.edu> message dated "Sat, 26 Apr 2008 22:55:20 -0700."*In-reply-to*: <20080427055520.GB2305@cs.caltech.edu>*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>*References*: <20080423002424.GB7342@cs.caltech.edu> <20080427055520.GB2305@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Jerome, This one is not so difficult, but grind expands choose, which loses type information. To see what was going on, I did the steps below, and noticed that the last assert fails when choose is expanded. This is because choose(I) is known to be of type (I), but it's expansion, epsilon(I), is only known to be of type posnat. ("" (skosimp*) (expand "remove") (expand "empty?") (expand "singleton?") (expand "member") (inst 1 "i!1") (("1" (skosimp) (inst -2 "y!1") (assert)) ("2" (assert)))) With this understanding, the proof can be shortened to (grind :exclude "choose") Regards, Sam Jerome <jerome@xxxxxxxxxxxxxx> wrote: > I have a similar recursive definition presented in my earlier email: > > >example: THEORY BEGIN > > index: TYPE = posnat > > value: TYPE = real > > indices: TYPE = non_empty_finite_set[index] > > myset: TYPE = [index -> value] > > fun: TYPE = FUNCTION[value, value -> value] > > > > curry(f: fun, m: myset, I: indices): RECURSIVE value = > > LET i: index = choose(I) IN > > IF singleton?(I) THEN m(i) > > ELSE f(m(i), curry(f, m, remove(i, I))) > > ENDIF > > MEASURE card(I) > >END example > > My question, again, is in regards to the TCC's generated. In my last > email, I asked about TCC2; this time I could use some help with TCC1: > > curry_TCC1: OBLIGATION > FORALL (I: indices, i: index): > NOT singleton?(I) AND i = choose(I) IMPLIES > NOT empty?[index](remove[index](i, I)); > > Using finite_sets_sum as an example (as Jerry had mentioned), a > similar TCC is discharge using '(SUBTYPE-TCC)'. Unfortunately, > applying the same rule to my curry_TCC1 isn't as successful. > > What exactly does SUBTYPE-TCC do (that it's so successful in the > finite_sets_sum case)? Is there a similar method I can use in my case? > Thanks again. > > jerome

**References**:**[PVS-Help] Termination TCC***From:*Jerome

**Re: [PVS-Help] Expected type TCC***From:*Jerome

- Prev by Date:
**Re: [PVS-Help] Expected type TCC** - Next by Date:
**[PVS-Help] The problem with self-stability example** - Previous by thread:
**Re: [PVS-Help] Expected type TCC** - Next by thread:
**[PVS-Help] The problem with self-stability example** - Index(es):