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

Re: [PVS-Help] singleton lists

R. Colvin wrote:
> Hi, I'm having I'm having trouble working with an antecedent:
> {-10} cons(c0`next(car(c0`list)), null) = (: empty :)
> I'd like to simplify this to
> c0`next(car(c0`list)) = empty
> ('empty' is a data constructor constant)
> I can't get PVS to recognise that the LHS of -10 can be simplified
> down.  Is there some property I can use?  (I can't figure out
> exactly what list_rep does in the prelude.) If so, would PVS then
> work out that equality on singleton lists is equivalent to equality
> on their elements?


There's a proof command that does just what you want:
(decompose-equality -10)

To make proofs more automatic, a good trick is to have
the following lemma as an auto-rewrite:

    equal_cons: LEMMA cons(a, x) = cons(b, y) IFF a=b AND x=y

You can install this as a rewrite rule by writing

    AUTO_REWRITE+ equal_const

in your pvs file, or by using (auto-rewrite "equal_cons")
in a proof. After that, commands like (assert) will
automatically simplify any equality similar to -10 into
what you need.

> Now a couple of related questions:
> In trying to solve the above problem I proved the lemma:
> 	cons_null: THEOREM
> 			(forall f, x: (: x :) = cons(x, null))
> When I tried introducing this using 'lemma', PVS seemed to automatically
> simplify it to true, ie, I didn't get any addition to the antecedents
> by using the lemma rule (with appropriate substitutions).

(: x :) is the same as cons(x, null) so this theorem is not very useful.
It states something that the prover knows already. That's also why
it simplifies to true whenever you try to introduce it. It's almost
the same as trying to use (forall x: x=x) as a lemma.

> You'll note the inclusion of the unused
> variable 'f' in the definition of 'cons_null'.  Theorems apparently
> need two variables for the 'lemma' command to work.  Is this
> correct, and if so is there a neater work around?

The lemma command works for any lemma. When it fails, it should give
you an error message with some indication of the reason. That's usually
for a lemma that comes from a parameterized theory and the prover
cannot determine how to instantiate the parameters. The presence or
absence of f should not matter.

> Thanks,
> Rob