[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