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

*To*: Bruno Dutertre <bruno@sdl.sri.com>*Subject*: Re: [PVS-Help] singleton lists*From*: "R. Colvin" <robert@itee.uq.edu.au>*Date*: Sun, 09 May 2004 08:58:52 +1000*Cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Fri, 07 May 2004 10:10:28 MST."<409BC304.40103@sdl.sri.com>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Hi Bruno, On Fri, 7 May, Bruno Dutertre wrote: : R. Colvin wrote: : > Hi, I'm having I'm having trouble working with an antecedent: : > [snip] : : There's a proof command that does just what you want: : (decompose-equality -10) Thanks, that fixed it : 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 Will do, thanks : > 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. Ok. I tried using a single-parameter lemma in a different context and the 'lemma' rule worked fine. But I still can't seem to make it work using the single-parameter version in the proofs I'm interested in. I have a theory: ---------------------------------- map_properties[T1, T2: TYPE]: Theory begin l: VAR list[T1] f: VAR [T1 -> T2] list_cons: THEOREM (forall f, l: cons?(l) implies l = cons(car(l), cdr(l))) list_cons2: THEOREM (forall l: cons?(l) implies l = cons(car(l), cdr(l))) [snip some other theorems] end map_properties ---------------------------------- In my proof I can execute: ++++++++++++++++ Rule? (lemma list_cons ("l" "c0`list" "f" "next(c0)")) Applying list_cons where l gets c0`list, f gets next(c0), this simplifies to: inv_np_not_ssq.1 : {-1} cons?(c0`list) IMPLIES c0`list = cons(car(c0`list), cdr(c0`list)) [snip] ++++++++++++++++ At the very next 'Rule?' prompt: ++++++++++++++++ Rule? (lemma list_cons2 ("l" "c0`list")) Found 0 resolutions for list_cons2 relative to the substitution. Please check substitution, provide actual parameters for lemma name, or supply more substitutions. No change on: (lemma list_cons2 ("l" "c0`list")) ++++++++++++++++ The object c0`list is the same in each case. As I said, I could get 'list_cons2' to work in a different context. The theorem list_cons is a fairly obvious property I need in my proofs - is there something in the prelude (or elsewhere) that I could use in place of list_cons? Thanks, Rob

- Prev by Date:
**Re: [PVS-Help] singleton lists** - Next by Date:
**[PVS-Help] Problem installing in RED HAT 9** - Prev by thread:
**Re: [PVS-Help] singleton lists** - Next by thread:
**Re: [PVS-Help] singleton lists** - Index(es):