;; 2026-05-28.  fib.scm

#|
(load "~/git/minlog/init.scm")
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
|#

(add-program-constant "Fib" (py "nat=>nat"))
(add-computation-rules
 "Fib 0" "0"
 "Fib 1" "1"
 "Fib(Succ(Succ n))" "Fib(Succ n)+Fib n")

(pp (nt (pt "Fib 0")))
(pp (nt (pt "Fib 1")))
(pp (nt (pt "Fib 2")))
(pp (nt (pt "Fib 3")))
(pp (nt (pt "Fib 4")))
(pp (nt (pt "Fib 5")))
(pp (nt (pt "Fib 6")))
(pp (nt (pt "Fib 7")))

;; > 0
;; > 1
;; > 1
;; > 2
;; > 3
;; > 5
;; > 8
;; > 13

(display-pconst "Fib")

;; Fib
;;   comprules
;; 0	Fib 0	0
;; 1	Fib 1	1
;; 2	Fib(Succ(Succ n))	Fib(Succ n)+Fib n

(pp "Fib2CompRule")

;; all n^ Fib(Succ(Succ n^))eqd Fib(Succ n^)+Fib n^

(set-totality-goal "Fib")
(fold-alltotal)
(assert "all n(TotalNat(Fib n) andi TotalNat(Fib(Succ n)))")
;; ...
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant
 "Next" (py "nat yprod nat yprod nat=>nat yprod nat yprod nat"))
(add-computation-rules
 "Next(n1 pair n2 pair n3)" "n1+n2 pair n2+n3 pair n2")

(add-var-name "nml" (py "nat yprod nat yprod nat"))

(set-totality-goal "Next")
(fold-alltotal)
(cases)
(assume "n")
(cases)
(assume "m" "l")
(ng #t)
(use "TotalVar")
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant "L" (py "nat=>nat yprod nat yprod nat"))
(add-computation-rules
 "L 0" "1 pair 0 pair 1"
 "L(Succ n)" "Next(L n)")

(pp (nt (pt "L 0")))
(pp (nt (pt "L 1")))
(pp (nt (pt "L 2")))
(pp (nt (pt "L 3")))
(pp (nt (pt "L 4")))
(pp (nt (pt "L 5")))
(pp (nt (pt "L 6")))
(pp (nt (pt "L 7")))

;; > 1 pair 0 pair 1
;; > 1 pair 1 pair 0
;; > 2 pair 1 pair 1
;; > 3 pair 2 pair 1
;; > 5 pair 3 pair 2
;; > 8 pair 5 pair 3
;; > 13 pair 8 pair 5
;; > 21 pair 13 pair 8

(set-totality-goal "L")
(fold-alltotal)
(ind)
;; 3,4
(ng #t)
(use "TotalVar")
;; 4
(assume "n" "IH")
(ng #t)
(use "NextTotal")
(use "IH")
;; Proof finished.
;; (cp)
(save-totality)

;; LFib
(set-goal "all n L(n+1)eqd(Fib(n+2) pair Fib(n+1) pair Fib n)")
;; ...
;; Proof finished.
;; (cp)
(save "LFib")

(display-pconst "Next")
(display-pconst "L")

(time (pp (nt (pt "Fib 29"))))
(time (pp (nt (pt "L 28"))))