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

[PVS-Help] Re: using modulo_arithmetic



"R. Colvin" <robert@itee.uq.edu.au> wrote:
> Hi, I'm having trouble proving the following theorem using the
> modulo_arithmetic theory.  
>
> 	modding: THEOREM (forall (b: posnat), (x: nat):
> 		rem(b+1)(x + b) = 
> 			if rem(b+1)(x) = 0 then 
> 				b 
> 			else 
> 				rem(b+1)(x) - 1 endif)
>
> I've simplified it to some extent but seem to be overlooking the
> crucial property/technique for 'rem' that would allow me to complete
> the proof.  Does anyone have a tip on how to proceed?

This is more roundabout than I would like, but does the trick with PVS
3.1:

(""
 (grind)
 (("1"
   (lemma "commutative_add" ("x" "b!1" "y" "x!1"))
   (replace -1)
   (use "rem_sum_assoc")
   (assert))
  ("2"
   (lemma "same_remainder"
    ("b" "1 + b!1" "x" "b!1 + x!1" "y" "x!1 - 1"))
   (assert)
   (use "divides_reflexive")
   (assert)
   (replace -2)
   (lemma "rem_sum_assoc" ("b" "1 + b!1" "x" "x!1 - 1" "n" "1"))
   (assert)
   (lemma "rem_add_one" ("b" "1 + b!1" "x" "x!1 - 1"))
   (assert))))

Regards,
-- 
Jerry James
http://www.ittc.ku.edu/~james/