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

*To*: pvs-help@csl.sri.com*Subject*: Re: How to prove this*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Mon, 20 Mar 2000 10:46:19 -0800*CC*: pvs-help@csl.sri.com*Delivery-Date*: Mon Mar 20 09:44:27 2000*References*: <38D410CB.57FCB8FC@cs.uidaho.edu>*Sender*: bruno@csl.sri.com

Jie Dai wrote: > > Hi pvs users, > > I am a new user of PVS. Is there anyone know why the last > GRIND can not simplify (y!1 - rem(n)(y!1))/n) to 0/n too?? > What should I do to complete the proof. > > Thanks for your help. > Rerunning step: (LEMMA "rem_mod2") > Applying rem_mod2 > this simplifies to: > test : > > {-1} FORALL (b: posnat, x: int): 0 <= x AND x < b IMPLIES rem(b)(x) = x > > [-2] (expt(2, r - 1) = n) > [-3] x!1 < n > [-4] y!1 < n > |------- > [1] (x!1 - rem(n)(x!1)) / n = (y!1 - rem(n)(y!1)) / n > > Rerunning step: (GRIND) > Trying repeated skolemization, instantiation, and if-lifting, > this simplifies to: > test : > > {-1} rem(n)(x!1) = x!1 > [-2] (expt(2, r - 1) = n) > [-3] x!1 < n > [-4] y!1 < n > |------- > {1} 0 / n = (y!1 - rem(n)(y!1)) / n > > Rule? > > Why the GRIND here can not simplify (y!1 - rem(n)(y!1))/n) to 0/n too? That's because the heuristic (GRIND) uses for instantiating quantifiers tries to find one instantiation only. In your case, (GRIND) instantiates formula -1 with b=n and x=x!1, and does not look for another match. To get (GRIND) to look for all possible matches, you can use (GRIND :IF-MATCH ALL), but even that does not always work. It is better to use "rem_mod2" as a rewrite rule: instead of doing (LEMMA "rem_mod2"), you can try something like (AUTO-REWRITE "rem_mod2")(ASSERT). Bruno -- Bruno Dutertre | bruno@sdl.sri.com SDL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

**References**:**How to prove this***From:*Jie Dai <jiedai@cs.uidaho.edu>

- Prev by Date:
**How to prove this** - Next by Date:
**help** - Prev by thread:
**How to prove this** - Next by thread:
**Typecheck question** - Index(es):