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

*To*: "R. Colvin" <robert@itee.uq.edu.au>*Subject*: Re: [PVS-Help] singleton lists*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Fri, 07 May 2004 10:10:28 -0700*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <200405060609.i46693v11425@localhost.localdomain>*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*: <200405060609.i46693v11425@localhost.localdomain>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040113

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? > Hi, 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 > Bruno

- Prev by Date:
**Re: [PVS-Help] symbol manipulation** - Next by Date:
**Re: [PVS-Help] singleton lists** - Prev by thread:
**[PVS-Help] singleton lists** - Next by thread:
**Re: [PVS-Help] singleton lists** - Index(es):