#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
; Matt Wilding

Event: Start with the library "extras" using the compiled version.

;; Proof of Matijasevich's lemma constructed by MW week of 5-10-91.  Inspired by
;; proof in Concrete Mathematics by Graham, Knuth, and Patashnik and notes from
;; Dijkstra's Capita Selecta Spring '90 course.
;;;; Some additional facts needed in the proof that appear useful
;;;; enough to add to libraries (and a few facts to prove them)

Theorem: irem-igcd-arg1 (irem (igcd (a, b), c) = 0) = ((irem (a, c) = 0) ∧ (irem (b, c) = 0))

Theorem: irem-x-x irem (x, x) = 0

;; The nonsensical induction hint is a silly trick to get the prover
;; to throw an equality away after using it

Theorem: gcd-times-easy-proof-helper-helper ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N)) → (((c ∗ gcd (a, b)) mod gcd (a, b ∗ c)) = 0)

Theorem: gcd-times-easy-proof-helper ((c ∗ gcd (a, b)) mod gcd (a, b ∗ c)) = 0

Theorem: gcd-times-easy-proof (gcd (a, b) = 1) → (gcd (a, b ∗ c) = gcd (a, c))

;; Would the more general case of rewriting gcd-times regardless
;; of the value of gcd with one of the times arguments be superior?

Theorem: gcd-times-easy (gcd (a, b) = 1) → ((gcd (a, b ∗ c) = gcd (a, c)) ∧ (gcd (a, c ∗ b) = gcd (a, c)))

Theorem: lessp-gcd3 ((gcd (a, b) < a) = (((b mod a) ≠ 0) ∧ (a ≄ 0) ∧ (b ≄ 0))) ∧ ((gcd (b, a) < a) = (((b mod a) ≠ 0) ∧ (a ≄ 0) ∧ (b ≄ 0)))

Theorem: equal-remainder-gcd-0-proof ((gcd (a, b) mod a) = 0) = ((b mod a) = 0)

;; not used in proof (though equal-remainder-gcd-0-proof is)

Theorem: equal-remainder-gcd-0 (((gcd (a, b) mod a) = 0) = ((b mod a) = 0)) ∧ (((gcd (b, a) mod a) = 0) = ((b mod a) = 0))

Theorem: equal-remainder-x-y-x ((x mod y) = x) = (((x ∈ N) ∧ (x < y))

∨ (x = 0)

∨ ((fix (y) = 0) ∧ (x ∈ N)))

Theorem: gcd-a-gcd-exp-a gcd (a, exp (a, b)) = if b ≃ 0 then 1

else fix (a) endif

Theorem: equal-gcd-times-1-help1 ((gcd (a, b) = 1) ∧ (gcd (a, c) = 1)) → (gcd (a, b ∗ c) = 1)

Theorem: remainder-gcd-gcd-0-hack (gcd (a, b ∗ c) mod gcd (a, c)) = 0 Theorem: lessp-gcd-times ((a ≄ 0) ∨ ((b ∗ c) ≄ 0)) → (gcd (a, b ∗ c) ≮ gcd (a, c))

Theorem: lessp-1-hack (1 < x) = ((x ≄ 0) ∧ (x ≠ 1))

Theorem: equal-gcd-times-1-help2 (gcd (a, b ∗ c) = 1) → (gcd (a, c) = 1)

Theorem: equal-gcd-times-1 (gcd (a, b ∗ c) = 1) = ((gcd (a, b) = 1) ∧ (gcd (a, c) = 1))

Theorem: gcd-exp-1 ((gcd (a, exp (b, c)) = 1) = ((gcd (a, b) = 1) ∨ (c ≃ 0))) ∧ ((gcd (exp (b, c), a) = 1) = ((gcd (a, b) = 1) ∨ (c ≃ 0)))

;; mistake in other version of this lemma limits applicability and
;; makes this version needed

Theorem: gcd-remainder-times-fact1-proof2 (gcd (a, b) = 1) → ((((c ∗ b) mod a) = 0) = ((c mod a) = 0))

Theorem: times-quotient-better ((x mod y) = 0) → ((((x ÷ y) ∗ y)

= if y ≃ 0 then 0

else fix (x) endif) ∧ ((y ∗ (x ÷ y))

= if y ≃ 0 then 0 else fix (x) endif))

Theorem: equal-remainder-exp-0 (((a mod c) = 0) ∧ (b ≄ 0)) → ((exp (a, b) mod c) = 0)

Theorem: remainder-2-hack (2 mod x) = if (x = 1) ∨ (x = 2) then 0

else 2 endif

Theorem: remainder-times-hack2 ((a mod b) ≠ 0) → (((a mod (b ∗ c)) ≠ 0) ∧ ((a mod (c ∗ b)) ≠ 0))

Theorem: gcd-a-add1-a gcd (a, 1 + a) = 1

;; These facts should perhaps be generalized into a meta lemma that
;; factors first

Theorem: remainder-times-times-hack ((b ∗ (a ∗ c)) mod (a ∗ x)) = (a ∗ ((b ∗ c) mod x))

Theorem: remainder-plus-times-hack (((a ∗ x) + (b ∗ (c ∗ (a ∗ y)))) mod (a ∗ z)) = (a ∗ ((x + (b ∗ (c ∗ y))) mod z))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Now, on to the proof
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: fib (x) = if x ≃ 0 then 0

elseif x = 1 then 1

else fib ((x − 1) − 1) + fib (x − 1) endif

Theorem: fib-plus fib (j + k) = if j ≃ 0 then fib (k)

else (fib (1 + k) ∗ fib (j )) + (fib (j − 1) ∗ fib (k)) endif

Theorem: gcd-fib-next-fib gcd (fib (n), fib (1 + n)) = 1

Theorem: gcd-fib gcd (fib (a), fib (b)) = fib (gcd (a, b))

Theorem: equal-fib-constant ((fib (a) = 0) = (a ≃ 0)) ∧ ((fib (a) = 1) = ((a = 1) ∨ (a = 2)))

Theorem: fib-small (a < 3) → (fib (a)

= if a ≃ 0 then 0 else 1 endif)

Definition: double-fib-induction (a, b) = if (a < 3) ∨ (b < 3) then t

else double-fib-induction (a − 1, b − 1) ∧ double-fib-induction ((a − 1) − 1, (b − 1) − 1) endif Theorem: lessp-fib-fib (fib (a) < fib (b)) = ((a < b) ∧ (¬ ((a = 1) ∧ (b = 2))))

Theorem: remainder-fib-fib-0 ((fib (a) mod fib (b)) = 0) = (((a mod b) = 0) ∨ (b = 2))

;; fib-times-open and fib-add1-times-open apply fib-plus to
;; particular terms in a way that will be useful in the proof
;; of fib-times-special

Theorem: fib-times-open (0 < k) → (fib (k ∗ n)

= ((fib (n) ∗ fib (1 + ((k − 1) ∗ n))) + (fib (n − 1) ∗ fib ((k − 1) ∗ n))))

Event: Disable fib-times-open.

Theorem: fib-add1-times-open (0 < k) → (fib (1 + (k ∗ n))

= ((fib (1 + ((k − 1) ∗ n)) ∗ fib (1 + n)) + (fib ((k − 1) ∗ n) ∗ fib (n))))

Event: Disable fib-add1-times-open.

Theorem: fib-times-special-step (1 < k) → (((k ∗ (fib (n) ∗ exp (fib (1 + n), k − 1))) mod (fib (n) ∗ fib (n)))

= (((fib (n) ∗ exp (fib (1 + n), k − 1))

+ (fib (n − 1)

∗ ((k − 1)
∗ (fib (n)

∗ exp (fib (1 + n), (k − 1) − 1)))))

mod (fib (n) ∗ fib (n))))

Theorem: fib-remainder-hack (fib (x ∗ y) mod fib (x)) = 0

;; We wish the rewriter to use a modulo arithmetic equality to rewrite
;; a term.  Fortunately, we can can construct REMAINDER-FIB-BACKCHAIN
;; to do it the way we wish since the terms are of a specialized form

Theorem: remainder-backchain-proof1 ((a mod c) = (b mod c)) → (((a ∗ d) mod c) = ((b ∗ d) mod c))

Theorem: remainder-backchain-proof2 (((a mod c) = (b mod c)) ∧ ((d mod c) = (e mod c))) → (((a + d) mod c) = ((b + e) mod c))

Theorem: remainder-fib-backchain (((fib (x) mod c) = (exp (p, q) mod c)) ∧ ((fib (y) mod c) = ((r ∗ s) mod c))) → ((((a ∗ fib (x)) + (b ∗ fib (y))) mod c)

= (((a ∗ exp (p, q)) + (b ∗ (r ∗ s))) mod c))

;; This is the guts of the proof

Theorem: fib-times-special (1 < k) → (((fib (k ∗ n) mod exp (fib (n), 2))

= ((k ∗ (fib (n) ∗ exp (fib (1 + n), k − 1)))

mod exp (fib (n), 2))) ∧ ((fib (1 + (k ∗ n)) mod exp (fib (n), 2))

= (exp (fib (1 + n), k) mod exp (fib (n), 2))))

Theorem: fib-remainder-times-special (fib (n ∗ k) mod (fib (n) ∗ fib (n))) = ((k ∗ (fib (n) ∗ exp (fib (1 + n), k − 1))) mod (fib (n) ∗ fib (n)))

Theorem: remainder-times-times-hack2 ((k ∗ n) mod (n ∗ p)) = (n ∗ (k mod p))

Theorem: matijasevich-lemma-helper ((2 < n) ∧ ((m mod n) = 0)) → (((fib (m) mod (fib (n) ∗ fib (n))) = 0)

= ((m mod (n ∗ fib (n))) = 0))

Theorem: matijasevich-lemma (2 < n) → (((fib (m) mod (fib (n) ∗ fib (n))) = 0)

= ((m mod (n ∗ fib (n))) = 0))

Index

double-fib-induction, 4

equal-fib-constant, 4 equal-gcd-times-1, 3 equal-gcd-times-1-help1, 2 equal-gcd-times-1-help2, 3 equal-remainder-exp-0, 3 equal-remainder-gcd-0, 2 equal-remainder-gcd-0-proof, 2 equal-remainder-x-y-x, 2 exp, 2, 3, 5, 6

fib, 4–6 fib-add1-times-open, 5 fib-plus, 4 fib-remainder-hack, 5 fib-remainder-times-special, 6 fib-small, 4 fib-times-open, 5 fib-times-special, 6 fib-times-special-step, 5

gcd, 2–4 gcd-a-add1-a, 3 gcd-a-gcd-exp-a, 2 gcd-exp-1, 3 gcd-fib, 4 gcd-fib-next-fib, 4 gcd-remainder-times-fact1-proof

2, 3 gcd-times-easy, 2 gcd-times-easy-proof, 2 gcd-times-easy-proof-helper, 2 gcd-times-easy-proof-helper-helpe

r, 2

igcd, 1 irem, 1 irem-igcd-arg1, 1 irem-x-x, 1

lessp-1-hack, 3 lessp-fib-fib, 5 lessp-gcd-times, 3 lessp-gcd3, 2

matijasevich-lemma, 6

matijasevich-lemma-helper, 6

remainder-2-hack, 3

remainder-backchain-proof1, 5 remainder-backchain-proof2, 6 remainder-fib-backchain, 6 remainder-fib-fib-0, 5 remainder-gcd-gcd-0-hack, 2 remainder-plus-times-hack, 4 remainder-times-hack2, 3 remainder-times-times-hack, 4 remainder-times-times-hack2, 6

times-quotient-better, 3