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

Re: How to prove this



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