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

Re: [PVS-Help] Expected type TCC



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