;; 2026-06-12.  dy.scm

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

;; Dyadic rationals have a power of 2 as denominator.  They are closed
;; under plus, times, minus and division by 2.  (1#3) can be
;; represented as a limit.

;; Dyadic rationals suffice for approximations to real numbers.  They
;; fit well with (binary) positive numbers and their constructors SZero
;; and SOne.  One only needs to cancel factors 2, and they are easily
;; visible since every positive number other than 1 has the unique
;; form SZero^n SOne p with n>=0.

;; Every dyadic rational has a unique normal form where no factor 2
;; can be cancelled.  This simplifies matters, since RatEqv and
;; compatibility lemmas are not needed for dyadic normal forms (DyNf).
;; Properties of RatMax and RatLe become cleaner on DyNf.  Recall that
;; RatMax has an asymmetric definition: in case k*q=j*p the lhs k*q is
;; returned, but the rhs j*p would be possible as well.  This leads to
;; RatMaxEq1: b<=a -> a max b=a but RatMaxEq2: a<=b -> a max b==b
;; with == instead of =.  On DyNf this does not happen.

;; Note that DyNf is not closed under addition (for example,
;; (1#2)+(1#2):=(4#4)).  We therefore use DyPlus (infix +=) defined by
;; a+=b := DyToNf(a+b).

(add-program-constant "RatNum" (py "rat=>int"))
(add-computation-rules
 "RatNum(k#p)" "k")

(set-totality-goal "RatNum")
(fold-alltotal)
(cases)
(assume "k" "p")
(use "TotalVar")
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant "RatDen" (py "rat=>pos"))
(add-computation-rules
 "RatDen(k#p)" "p")

(set-totality-goal "RatDen")
...
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant "IsTwoExp" (py "pos=>boole"))
(add-computation-rules
 "IsTwoExp 1" "True"
 "IsTwoExp(SZero p)" "IsTwoExp p"
 "IsTwoExp(SOne p)" "False")

(set-totality-goal "IsTwoExp")
...
;; Proof finished.
;; (cp)
(save-totality)

;; IsTwoExpTimes
(set-goal "all p,q(IsTwoExp p -> IsTwoExp q -> IsTwoExp(p*q))")
(ind)
;; 2-4
(assume "q" "Useless" "Iq")
(use "Iq")
;; 3
(assume "p" "IH" "q")
(ng)
(use "IH")
;; 4
(ng)
(search 1 '("EfAtom" 1)) ;bounds height of search tree.  Uses EfAtom
;; Proof finished.
;; (cp)
(save "IsTwoExpTimes")

(add-program-constant "Dy" (py "rat=>boole"))
(add-computation-rules
 "Dy a" "IsTwoExp(RatDen a)")

;; DyTotal
(set-totality-goal "Dy")
...
;; Proof finished.
;; (cp)
(save-totality)

;; (display-alg "pos" "int")

;; pos
;; 	One:	pos           
;; 	SZero:	pos=>pos
;; 	SOne:	pos=>pos
;; int
;; 	IntPos:	pos=>int
;; 	IntZero:	int
;; 	IntNeg:	pos=>int

;; Abbreviations: 
;; 1       for   One
;; IntP    for   IntPos
;; 0       for   IntZero
;; IntN    for   IntNeg

;; (display-default-varnames)

;; as: 	nat=>rat
;; a: 	rat
;; kj: 	int yprod int
;; k: 	int
;; ps: 	nat=>pos
;; wf: 	pos=>boole
;; p: 	pos
;; ns: 	nat=>nat
;; ws: 	nat=>boole
;; w: 	boole
;; n: 	nat

;; (pp (var-to-type (pv "q")))
;; pos

;; Dyadic rationals have a power of 2 as denominator:

;; DyToExpPosLog
(set-goal "all k,p(Dy(k#p) -> p=2**PosLog p)")
(assume "k")
(ng)
;; ?^3:all p(IsTwoExp p -> p=2**PosLog p)
(ind)
...
;; Proof finished.
;; (cp)
(save "DyToExpPosLog")

(add-program-constant "RatCancelTwo" (py "rat=>rat"))

(add-computation-rules
 "RatCancelTwo k" "k#1"
 "RatCancelTwo(0#q)" "0#1"
 "RatCancelTwo(1#SZero q)" "1#SZero q"
 "RatCancelTwo(SZero p#SZero q)" "RatCancelTwo(p#q)"
 "RatCancelTwo(SOne p#SZero q)" "SOne p#SZero q"
 "RatCancelTwo(IntN 1#SZero q)" "IntN 1#SZero q"
 "RatCancelTwo(IntN(SZero p)#SZero q)" "RatCancelTwo(IntN p#q)"
 "RatCancelTwo(IntN(SOne p)#SZero q)" "IntN(SOne p)#SZero q"
 "RatCancelTwo(IntP p#SOne q)" "IntP p#SOne q"
 "RatCancelTwo(IntN p#SOne q)" "IntN p#SOne q")

#|
(pp (nt (pt "RatCancelTwo(0#8)")))
(pp (nt (pt "RatCancelTwo(1#8)")))
(pp (nt (pt "RatCancelTwo(2#8)")))
(pp (nt (pt "RatCancelTwo(3#8)")))
(pp (nt (pt "RatCancelTwo(4#8)")))
(pp (nt (pt "RatCancelTwo(5#8)")))
(pp (nt (pt "RatCancelTwo(6#8)")))
(pp (nt (pt "RatCancelTwo(7#8)")))
(pp (nt (pt "RatCancelTwo(8#8)")))
(pp (nt (pt "RatCancelTwo(9#8)")))
(pp (nt (pt "RatCancelTwo(10#8)")))

(term-to-string (nt (pt "3*2**5"))) ;"96"
(term-to-string (nt (pt "5*2**5"))) ;"160"
(pp (nt (pt "RatCancelTwo(96#160)"))) ;3#5
(pp (nt (pt "RatCancelTwo(128#160)"))) ;4#5
|#

;; RatCancelTwoTotal
(set-totality-goal "RatCancelTwo")
(fold-alltotal)
(cases)
(ind)
...
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant "DyNf" (py "rat=>boole"))
(add-computation-rules
 "DyNf k" "True"
 "DyNf(k#SOne q)" "False"
 "DyNf(1#SZero q)" "DyNf(1#q)"
 "DyNf(SZero p#SZero q)" "False"
 "DyNf(SOne p#SZero q)" "DyNf(SOne p#q)"
 "DyNf(0#SZero q)" "False"
 "DyNf(IntN 1#SZero q)" "DyNf(1#q)"
 "DyNf(IntN(SZero p)#SZero q)" "False"
 "DyNf(IntN(SOne p)#SZero q)" "DyNf(SOne p#q)")

(set-totality-goal "DyNf")
(fold-alltotal)
(cases)
(cut "all q,k TotalBoole(DyNf(k#q))")
...
;; Proof finished.
;; (cp)
(save-totality)

;; DyNfToDy
(set-goal "all a(DyNf a -> Dy a)")
(cases)
(ng)
(cut "all p,k(DyNf(k#p) -> IsTwoExp p)")
...
;; Proof finished.
;; (cp)
(save "DyNfToDy")