[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*: Mon, 10 May 2004 10:21:57 -0700*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <200405082258.i48Mwqu02273@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*: <200405082258.i48Mwqu02273@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

list_cons_eta: AXIOM FORALL (cons?_var: (cons?)): cons(car(cons?_var), cdr(cons?_var)) = cons?_var; R. Colvin wrote: > 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")) > ++++++++++++++++ > Hi, This fails because theory map_properties has two parameters T1 and T2. Even though T2 does not occur in list_cons2, both parameters must be instantiated when the lemma is used. Variable l of list_cons and list_cons2 is of type list[T1], so PVS can infer the actual type T1 from the term "c0`list", but that's not enough. The prover cannot determine T2. When you use lemma "list_cons" and give a substitution for "f" then the prover has enough information to determine both T1 and T2. The simplest solution to avoid this f is to specify explicitly the types you want. For example, if T1 and T2 are nat, you can write (lemma "list_cons2[nat, nat]" ...). > 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? > Yes, the following axiom is generated from the definition of list: list_cons_eta: AXIOM FORALL (cons?_var: (cons?)): cons(car(cons?_var), cdr(cons?_var)) = cons?_var; It's in theory "list_adt" that axiomatizes the list datatype. The theory can be viewed using M-x view-prelude-theory. In a proof, you rarely need to invoke these lemmas explictly. The commands (eta ..) or (apply-eta ..) will do it for you. Also, (apply-extensionality ...) is often more useful than the eta axioms. Bruno

**References**:**Re: [PVS-Help] singleton lists***From:*"R. Colvin" <robert@itee.uq.edu.au>

- Prev by Date:
**[PVS-Help] CIL->PVS connector** - Next by Date:
**[PVS-Help] function domains** - Prev by thread:
**Re: [PVS-Help] singleton lists** - Next by thread:
**[PVS-Help] Problem in installation in Linux machine** - Index(es):