mersenne

(in-package "DM")

(local (include-book "arithmetic-5/top" :dir :system))

(include-book "gauss")

(comp t)

(defmacro maybe-skip
  (x)
  (declare (ignore x))
  '(value-triple nil))

(defun m (p) (1- (expt 2 p)))

(defthm mersenne-19 (primep (m 19)))

(maybe-skip (defthm mersenne-31 (primep (m 31))))

(defthm mersenne-23 (not (primep (m 23))))

(maybe-skip (defthm mersenne-67 (not (primep (m 67)))))

(maybe-skip (defthm mersenne-999671
    (not (primep (m 999671)))))

(defun least-divisor-2
  (k n)
  (declare (xargs :measure (nfix (- n k))))
  (if (and (integerp n)
      (integerp k)
      (< 1 k)
      (<= k n))
    (if (> (* k k) n)
      n
      (if (divides k n)
        k
        (least-divisor-2 (1+ k) n)))
    nil))

(comp t)

(local-defthm hack-1
  (implies (and (not (zp a))
      (not (zp b))
      (not (zp c))
      (not (zp d))
      (<= a c)
      (<= b d))
    (<= (* a b) (* c b)))
  :rule-classes nil)

(local-defthm hack-2
  (implies (and (not (zp a))
      (not (zp b))
      (not (zp c))
      (not (zp d))
      (<= a c)
      (<= b d))
    (<= (* c b) (* c d)))
  :rule-classes nil)

(local-defthm hack-3
  (implies (and (not (zp a))
      (not (zp b))
      (not (zp c))
      (not (zp d))
      (<= a c)
      (<= b d))
    (<= (* a b) (* c d)))
  :hints (("Goal" :use (hack-1 hack-2)
     :in-theory (theory 'minimal-theory))))

(local-defthm hack-4
  (implies (and (not (zp k))
      (not (zp ld))
      (<= k ld))
    (<= (* k k) (* ld ld)))
  :hints (("Goal" :use ((:instance hack-3
        (a k)
        (b k)
        (c ld)
        (d ld)))))
  :rule-classes nil)

(defthm least-divisor-rewrite-lemma-1
  (implies (and (integerp n)
      (integerp k)
      (< 1 k)
      (<= k n)
      (<= (* (least-divisor k n)
          (least-divisor k n))
        n))
    (equal (least-divisor k n)
      (least-divisor-2 k n)))
  :rule-classes nil
  :hints (("Subgoal *1/7" :use (least-divisor-divides (:instance hack-4
         (ld (least-divisor (1+ k) n))))) ("Subgoal *1/1" :use (least-divisor-divides (:instance hack-4
          (ld (least-divisor (1+ k) n)))))))

(local-defthm hack-5
  (implies (and (not (zp a))
      (not (zp n))
      (<= 1 (/ n a)))
    (<= a n))
  :rule-classes nil)

(defthm least-divisor-rewrite-lemma-2
  (implies (and (integerp n)
      (> n 1)
      (not (= n (least-divisor 2 n))))
    (<= (* (least-divisor 2 n) (least-divisor 2 n))
      n))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable divides)
     :use ((:instance least-divisor-divides (k 2)) (:instance least-divisor-is-least
         (k 2)
         (d (/ n (least-divisor 2 n))))
       (:instance hack-5
         (a (* (least-divisor 2 n) (least-divisor 2 n))))))))

(defthm least-divisor-rewrite-lemma-3
  (implies (and (integerp n)
      (integerp k)
      (< 1 k)
      (<= k n)
      (= n (least-divisor k n)))
    (= n (least-divisor-2 k n)))
  :rule-classes nil
  :hints (("Goal" :use (least-divisor-divides (:instance least-divisor-is-least
         (d (least-divisor-2 2 n)))))))

(defthm least-divisor-rewrite
  (equal (least-divisor 2 n)
    (least-divisor-2 2 n))
  :hints (("Goal" :use (least-divisor-rewrite-lemma-2 (:instance least-divisor-rewrite-lemma-3 (k 2))
       (:instance least-divisor-rewrite-lemma-1 (k 2))))))

(in-theory (enable primep))

(in-theory (disable (primep) (least-divisor)))

(defthm mersenne-31-revisited
  (primep (m 31)))

(maybe-skip (defthm mersenne-61 (primep (m 61))))

(defthm theorem-103
  (implies (and (primep p)
      (= (mod p 4) 3)
      (primep (1+ (* 2 p))))
    (divides (1+ (* 2 p)) (m p)))
  :rule-classes nil
  :hints (("Goal" :use ((:instance second-supplement (p (1+ (* 2 p)))) (:instance euler-criterion
         (m 2)
         (p (1+ (* 2 p))))
       (:instance mod-sum
         (a 1)
         (b (* 2 p))
         (n 8))
       (:instance mod-prod (k 2) (m p) (n 4))
       (:instance divides-leq
         (x (1+ (* 2 p)))
         (y 2))
       (:instance divides-mod-equal
         (a (expt 2 p))
         (b 1)
         (n (1+ (* 2 p))))))))

(local-defthm hack-6
  (implies (and (not (zp a))
      (>= a (* 4 (1- p)))
      (integerp p)
      (> p 3))
    (>= (* 2 a) (* 4 p)))
  :rule-classes nil)

(local-defthm hack-7
  (implies (and (>= (expt 2 (1- p)) (* 4 (1- p)))
      (integerp p)
      (> p 3))
    (>= (expt 2 p) (* 4 p)))
  :rule-classes nil
  :hints (("Goal" :use ((:instance hack-6 (a (expt 2 (1- p))))))))

(local-defthm hack-8
  (implies (and (integerp p) (> p 3))
    (>= (expt 2 p) (* 4 p)))
  :rule-classes nil
  :hints (("Goal" :induct (fact p)) ("Subgoal *1/2" :use hack-7)))

(local-defthm hack-9
  (implies (and (integerp p) (> p 3))
    (> (* 4 p) (* 2 (1+ p))))
  :rule-classes nil)

(defthm expt-2-p-bnd
  (implies (and (integerp p) (> p 3))
    (> (expt 2 p) (* 2 (1+ p))))
  :rule-classes nil
  :hints (("Goal" :use (hack-8 hack-9)
     :in-theory (theory 'minimal-theory))))

(defthm theorem-103-corollary
  (implies (and (primep p)
      (= (mod p 4) 3)
      (> p 3)
      (primep (1+ (* 2 p))))
    (not (primep (m p))))
  :hints (("Goal" :use (theorem-103 expt-2-p-bnd
       (:instance primep-no-divisor
         (p (1- (expt 2 p)))
         (d (1+ (* 2 p))))))))

(local-in-theory (disable primep m (m)))

(local-in-theory (enable (primep)))

(defthm mersenne-23-revisited
  (not (primep (m 23))))

(defthm mersenne-999671-revisited
  (not (primep (m 999671))))

(maybe-skip (defthm mersenne-19876271
    (not (primep (m 19876271)))))