;; 2022-06-12.  ueb07.scm

;; Exercise 25:  Formalization of Exercise 24 (on Dy, DyNf).

(load "~/git/minlog/init.scm")

;; loading some library files:
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.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 hat 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.

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

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

(add-program-constant "IsTwoExp" (py "pos=>boole"))
(add-computation-rules
 ;; ...
 )

(add-program-constant "Dy" (py "rat=>boole"))
(add-computation-rules
 ;; ...
 )

(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)"
 ;; ...
 )

(add-program-constant "DyNf" (py "rat=>boole"))
(add-computation-rules
 ;; ...
 )

;; (b)

(pp "EfAtom")
;; F -> allnc boole^ boole^

;; DyNfToDy
(set-goal "all a(DyNf a -> Dy a)")
(cases)
(ng)
(cut "all p,k(DyNf(k#p) -> IsTwoExp p)")
;; 3,4
(auto)
;; 4
(ind)
;; ...