;;; Copyright 2022 Intel Corporation All Rights Reserved.
;; Simple proofs of Sam Coward rules
;; Anna Slobodova 02/08/2022
(in-package "ACL2")
(include-book "centaur/bitops/ihsext-basics" :dir :System)
(local (include-book "arithmetic/top" :dir :system))
(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))
;; (local (include-book "std/strings/hexify" :dir :system))
(local (in-theory (disable unsigned-byte-p (tau-system))))
;;------- Commutativity
;; For any r: follows from commutativity of integers
(defthm bounded-commutativity-of-*
(implies
(and
(integerp a)
(integerp b))
(equal
(loghead r (* a b))
(loghead r (* b a)))))
;; SOme lemmas that help us with further proofs
(local
(defthm unsigned-byte-p-of-mul
(implies
(and
(unsigned-byte-p p a)
(unsigned-byte-p r b))
(unsigned-byte-p (+ p r) (* a b)))
:hints (("goal" :in-theory (enable unsigned-byte-p)
:nonlinearp t))
))
;; uses BITOPS::UNSIGNED-BYTE-P-INCR
(local
(defthm loghead-inc
(implies
(and
(unsigned-byte-p n x)
(natp m)
(<= n m))
(equal
(loghead m x)
x))))
(local
(defthm loghead-inc-of-mul
(implies
(and
(force (unsigned-byte-p p a))
(force (unsigned-byte-p r b))
(natp p)
(natp r)
(natp u)
(<= (+ p r) u))
(equal
(loghead u (* a b))
(* a b)
))
:hints (("goal" :in-theory (disable loghead-inc)
:use ((:instance loghead-inc (m u) (n (+ p r)) (x (* a b))))
))
))
;;------------------ MULT ASSOCIATIVITY --------------
;; Our goal is to prove (under some conditions)
;; (equal
;; (loghead v (* (loghead u (* a b)) c))
;; (loghead v (* a (loghead q (* b c )))))
;; First let's simplify LHS:
;; consider two cases:
;;= (loghead v (* (loghead v (loghead u (* a b))) (loghead v c))) if (<= v u)
;;= (loghead v (* (* a b) c)) if (and (< u v)(<= (+ p r) u))
(local
(encapsulate
()
(local
(defthm bounded-mult-associativity-LHS1
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(<= v u))
(equal
(loghead v (* (loghead u (* a b)) c))
(loghead v (* (loghead v (* a b)) (loghead v c)))))
:hints (("goal"
:in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
BITOPS::LOGHEAD-OF-LOGHEAD-1)
:use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n v) (x (loghead u (* a b))) (y c))
(:instance BITOPS::LOGHEAD-OF-LOGHEAD-1 (m v) (n u) (x (* a b))))))
))
(local
(defthm bounded-mult-associativity-LHS2
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(<= v u))
(equal
(loghead v (* (loghead v (* a b)) (loghead v c)))
(loghead v (* a b c))))))
(local (in-theory (disable COMMUTATIVITY-OF-*)))
(local
(defthm bounded-mult-associativity-LHS3
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(<= v u))
(equal
(loghead v (* (loghead u (* a b)) c))
(loghead v (* a b c))))
:hints (("goal" :cases ((<= v u)) ))
))
(defthm bounded-mult-associativity-LHS4
(implies
(and
(unsigned-byte-p p a)
(unsigned-byte-p r b)
(integerp c)
(natp u) (natp v) (natp p) (natp r)
(or
(<= v u)
(<= (+ p r) u)))
(equal
(loghead v (* (loghead u (* a b)) c))
(loghead v (* a b c)))))
))
;; Now let's simplify RHS (again consider two cases)
;;(loghead v (* a (loghead q (* b c))))
;;= (loghead v (* (loghead v a) (loghead v (* b c)))) if (<= v q)
;;= (loghead v (* a (loghead (+ r s) (* b c)))) if (< q v) (<= (+ r s) q)
;; =(loghead v (* a (loghead v (* b c))))
;; =(loghead v (* a (* b c)))
(local
(encapsulate
()
(local
(defthm bounded-mult-associativity-RHS1
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp v)
(natp q)
(<= v q))
(equal
(loghead v (* a (loghead q (* b c))))
(loghead v (* (loghead v a ) (loghead v (* b c))))))
:hints (("goal"
:in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
BITOPS::LOGHEAD-OF-LOGHEAD-1)
:use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n v) (x a) (y (loghead q (* b c))))
(:instance BITOPS::LOGHEAD-OF-LOGHEAD-1 (m v) (n q) (x (* b c))))))
))
(local
(defthm bounded-mult-associativity-RHS2
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp v)
(natp q)
(<= v q))
(equal
(loghead v (* (loghead v a ) (loghead v (* b c))))
(loghead v (* a b c))))))
(local
(defthm bounded-mult-associativity-RHS3
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp v)
(natp q)
(<= v q))
(equal
(loghead v (* a (loghead q (* b c))))
(loghead v (* a b c))))))
(defthm bounded-associativity-RHS4
(implies
(and
(unsigned-byte-p r b)
(unsigned-byte-p s c)
(integerp a)
(natp q) (natp v) (natp r) (natp s)
(or
(<= v q)
(<= (+ r s) q)))
(equal
(loghead v (* a (loghead q (* b c))))
(loghead v (* a b c)))))
))
(defthm bounded-mult-associativity
(implies
(and
(unsigned-byte-p p a)
(unsigned-byte-p r b)
(unsigned-byte-p s c)
(natp p)(natp r) (natp s)(natp u)
(natp v)(natp q)
(and
(or
(<= v q)
(<= (+ r s) q))
(or
(<= v u)
(<= (+ p r) u))))
(equal
(loghead v (* (loghead u (* a b)) c))
(loghead v (* a (loghead q (* b c )))))
))
;;---------- ADD ASSOCIATIVITY LEFT OUT
#||
(defthm bounded-add-associativity
(implies
(and
(unsigned-byte-p p a)
(unsigned-byte-p r b)
(unsigned-byte-p s c)
(and
(or (<= v q) (< (max r s) q))
(or (<= v u) (< (max p r) u))))
(equal
(loghead v (+ (loghead u (+ a b)) c))
(loghead v (+ a (loghead q (+ b c)))))))
||#
;;------------- DISTRIBUTE
;; We want to prove (under some conditions)
(local
(encapsulate
()
;; (loghead r (* a (loghead q (+ b c))))
;; (loghead r (* (loghead r a) (loghead r (loghead q (+ b c)))))
;; (loghead r (* (loghead r a) (loghead r (+ b c))))
;; (loghead r (* (loghead r a) (loghead r (+ (loghead r b) (loghead r c)))))
(local
(defthm distribute-mult-over-add-LHS1
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp q)
(<= r q))
(equal
(loghead r (* a (loghead q (+ b c))))
(loghead r (* (loghead r a) (loghead r (+ b c))))
))
:hints (("goal"
:in-theory (disable BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME
BITOPS::LOGHEAD-OF-LOGHEAD-1
)
:use ((:instance BITOPS::LOGHEAD-OF-*-OF-LOGHEAD-SAME (n r) (x a) (y (loghead q (+ b c))))
(:instance BITOPS::LOGHEAD-OF-LOGHEAD-1 (m r) (n q) (x (+ b c)))
)
))))
(local
(defthm distribute-mult-over-add-LHS2
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp q)
(<= r q))
(equal
(loghead r (* (loghead r a) (loghead r (+ b c))))
(loghead r (* a (+ b c)))
))))
(defthm distribute-mult-over-add-LHS3
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp q)
(<= r q))
(equal
(loghead r (* a (loghead q (+ b c))))
(loghead r (* a (+ b c)))
)))
))
(local
(encapsulate
()
(local
(defthm distribute-mult-over-add-RHS1
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(natp v)
(<= r u)
(<= r v))
(equal
(loghead r (+ (loghead u (* a b)) (loghead v (* a c))))
(loghead r (+ (loghead r (* a b)) (loghead r (* a c))))
))
:hints (("goal"
:in-theory (disable BITOPS::LOGHEAD-OF-+-OF-LOGHEAD-SAME
BITOPS::LOGHEAD-OF-LOGHEAD-1
)
:use ((:instance BITOPS::LOGHEAD-OF-+-OF-LOGHEAD-SAME (n r) (x (loghead u (* a b))) (y (loghead v (* a c))))
(:instance BITOPS::LOGHEAD-OF-LOGHEAD-1 (m r) (n u) (x (* a b)))
(:instance BITOPS::LOGHEAD-OF-LOGHEAD-1 (m r) (n v) (x (* a c)))
)
)))
)
(local
(defthm distribute-mult-over-add-RHS2
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(natp v)
(<= r u)
(<= r v))
(equal
(loghead r (+ (loghead r (* a b)) (loghead r (* a c))))
(loghead r (+ (* a b) (* a c)))
))))
(defthm distribute-mult-over-add-RHS3
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp u)
(natp v)
(<= r u)
(<= r v))
(equal
(loghead r (+ (loghead u (* a b)) (loghead v (* a c))))
(loghead r (+ (* a b) (* a c)))
)))
))
(defthm distribute-mult-over-add
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(natp q) (natp u) (natp v)
(<= r q) (<= r u) (<= r v))
(equal
(loghead r (* a (loghead q (+ b c))))
(loghead r (+ (loghead u (* a b)) (loghead v (* a c))))))
:hints (("goal"
:in-theory (disable distribute-mult-over-add-LHS3 )
:use ( distribute-mult-over-add-LHS3)
))
)
;;------------- Sum Same
(encapsulate
()
(local
(defthm lemma1
(implies
(integerp a)
(equal (+ a a) (* 2 a)))))
(defthm bounded-sum-same
(implies
(integerp a)
(equal
(loghead q (+ a a))
(loghead q (* 2 a)))))
)
;;--------------- Add Zero
(defthm bounded-add-zero
(implies
(and
(integerp a)
(integerp b)
(natp p)
(equal (mod b (expt 2 p)) 0))
(equal
(loghead p (+ a b))
(loghead p a)))
:hints (("goal" :in-theory (enable loghead)))
)
;;------------- Sub to Neg
;; no rules are created from this theorem
(defthm sub-to-neg
(implies
(and
(integerp a)
(integerp b))
(equal
(loghead r (- a b))
(loghead r (+ a (- b)))))
:rule-classes nil
)
;;----------- Mult by One
(defthm mult-by-one
(implies
(and
(integerp a)
(integerp b)
(natp p)
(equal (mod b (expt 2 p)) 1))
(equal
(loghead p (* a b))
(loghead p a)))
:hints (("goal" :in-theory (enable loghead)))
)
;;------------ Mult by Two
(defthm bounded-mult-by-two
(implies
(integerp a)
(equal
(loghead r (* a 2))
(loghead r (ash a 1))))
:hints(("goal" :in-theory (Enable ash)))
)
;;------------ Merge Left Shift
;; -- more general
(defthm merge-left-shift
(implies
(and
(integerp a)
(natp b)
(natp c))
(equal
(ash (ash a b) c)
(ash a (+ b c))))
:hints (("goal" :in-theory (enable ash)))
)
;;----------- Merg Right Shift
;; -- mode general
(defthm merge-right-shift
(implies
(and
(integerp a)
(natp b)
(natp c))
(equal
(ash (ash a (- b)) (- c))
(ash a (- (+ b c))))))
;;---------- Redundant Sel
(defthm redundant-sel
(equal
(if b a a)
a)
:rule-classes nil)
;; not true: (r=10, p=2, a=3=b011,~a=b110, -a=-3=b101, r=3)
;; (defthm bounded-not-neg
;; (implies
;; (and
;; (unsigned-byte-p p a)
;; (natp p))
;; (equal
;; (loghead r (+ 1 (loghead p (lognot a))))
;; (loghead r (- a))))
;; :hints (("goal" :in-theory (Enable lognot)))
;; )
;; (defthm bounded-neg-not
;; (implies
;; (and
;; (natp p)
;; (natp r)
;; (<= r p)
;; (unsigned-byte-p p a)
;; )
;; (equal
;; (loghead r (+ 1 (loghead p (lognot a))))
;; (loghead r (- a))))
;; :hints (("goal" :in-theory (Enable lognot)))
;; )
;;---------- Not over Con
;;-- more general --
;; (logapp s b a) will concatenate a and low s bits of b
(defthm not-over-con
(implies
(and
(unsigned-byte-p q a)
(unsigned-byte-p s b)
)
(equal
(loghead (+ s q) (lognot (logapp s b a)))
(loghead (+ s q) (logapp s (lognot b) (lognot a)))))
:hints (("goal" :in-theory (enable logapp lognot loghead expt mod unsigned-byte-p)
:nonlinearp t))
)
;;-------------- Mult Constant
(defthm mult-constant
(implies
(and (integerp x) (integerp c))
(equal
(+ (* 2 (* (logtail 1 c) x)) (* (loghead 1 c) x))
(* c x)))
:hints (("goal" :nonlinearp t
:in-theory (Enable loghead logtail)
))
)
;;------------- One to Two Mult
(defthm mult-to-two
(implies
(integerp x)
(equal
(- (* 2 x) x)
x)))
;;------------ Left Shift Add
(defthm left-shift-add
(implies
(and
(natp c)
(integerp a)
(integerp b))
(equal
(ash (+ a b) c)
(+ (ash a c) (ash b c))))
:hints (("goal" :in-theory (Enable ash)))
)
;;------------- Right Shift Add
(defthm add-right-shift
(implies
(and
(integerp a)
(integerp b)
(natp c))
(equal
(ash (+ (ash a c) b) (- c))
(+ a (ash b (- c)))))
:hints (("goal" :in-theory (Enable ash)))
)
;;-------------- Left Shift Mul
(defthm left-shift-mult
(implies
(and
(integerp a)
(integerp b)
(natp c))
(equal
(ash (* a b) c)
(* (ash a c) b)))
:hints (("goal" :in-theory (Enable ash)))
)
;;-------------- Sel Add
;; (defthm bounded-sel-add
;; (implies
;; (and
;; (unsigned-byte-p p a)
;; (unsigned-byte-p q b)
;; (unsigned-byte-p p c)
;; (unsigned-byte-p q d)
;; )
;; (equal
;; (loghead r (if e (+ a b) (+ c d)))
;; (loghead r (+ (if e a c) (if e b d))))))
;;
;;-- more general ---
;; In acl2, (if e x y) will evaluate to y only if e=NIL, otherwise it evaluates to x
(defthm sel-add
(implies
(and
(integerp a)
(integerp b)
(integerp c)
(integerp d)
)
(equal
(if e (+ a b) (+ c d))
(+ (if e a c) (if e b d)))))
;;-------- Sel Add Zero
;; this is jsut a case of the previous one.
(defthm sel-add-zero
(implies
(and
(integerp a)
(integerp b)
(integerp c))
(equal
(if e (+ a b) c)
(+ (if e a c) (if e b 0)))))
;;------- Mov Sel Zero
;; (defthm mov-sel-zero
;; (implies
;; (and
;; (integerp a)
;; (integerp c))
;; (equal
;; (loghead r (* (if b 0 a) c))
;; (loghead r (* a (if b 0 c))))))
;;
;;--- More general--
(defthm mov-sel-zero
(implies
(and
(integerp a)
(integerp c))
(equal
(* (if b 0 a) c)
(* a (if b 0 c)))))
;;------------- Concat to Add
;; (str::hexify (logapp 16 #uxCDEF #uxAB))
;;more general
(defthm bounded-concat-to-add
(implies
(and
(integerp a)
(unsigned-byte-p q b)
(natp q))
(equal
(logapp q b a)
(+ (ash a q) b)))
:hints (("goal" :in-theory (enable ash logapp unsigned-byte-p)))
)
