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

Re: [PVS-Help] How to continue this proof?



Hi Sjaak,

It is possible that, as you suggest, the map instances are different.
The way to check this is to use C-u M-x show-expanded-sequent, which will
show all the instances of all the names.

If that doesn't suggest a way forward, could you send me the specs and
I'll see what I can do?

Thanks,
Sam

Sjaak Smetsers <s.smetsers@xxxxxxxxxxxxx> wrote:

> Especially when dealing with lists, I now end then get stuck in a situation like
> this:
> 
> [-1]  length[list[T]]
> 
>           (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
> 
>                inject(x!1)(cons2_var!1)))
> 
>        = 1 + length[T](cons2_var!1)
> 
>   |-------
> 
> [1]   1 +
> 
>        length[list[T]]
> 
>            (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
> 
>                 inject(x!1)(cons2_var!1)))
> 
>        = 2 + length[T](cons2_var!1)
> 
> I don’t understand why PVS is not able to derive 1 from -1. It seems as if it
> considers the applications of map as different, but I do not see why. But more
> annoyingly, there seems to way to continue. How should I proceed? E.g. if I type
> (name-replace STUPIDTHING “map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
> inject(x!1)(cons2_var!1))”) it will replace just one of the map expressions by
>  STUPIDTHING.
> 
> Sjaak
>