;; 2026-04-23.  np.scm

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "pos.scm")
(set! COMMENT-FLAG #t)

(add-program-constant "NP" (py "nat=>pos"))
(add-computation-rules
 "NP Zero" "1"
 "NP(Succ Zero)" "1"
 "NP(Succ(Succ n))"
 "[if (NatEven n) (SZero(NP(Succ(NatHalf n)))) (SOne(NP(Succ(NatHalf n))))]")

;; Exercise 15.  Goal: NP is total

;; Helpful commands: assume use ng cases

;; Helpful theorems
(pp "TotalPosSOne")
(pp "TotalPosSZero")
(pp "NatHalfLe")
;; all n NatHalf n<=n

;; NPStep
(set-goal "all n(Zero<n -> all m(m<=Succ n -> TotalPos(NP m)) -> 
 TotalPos(NP(Succ(Succ n))))")
;; ...
(save "NPStep")

;; Helpful theorems
(pp "CVIndPvar")
;; (F -> all n (Pvar nat)n) -> 
;; all n(all m(m<n -> (Pvar nat)m) -> (Pvar nat)n) -> all n (Pvar nat)n
(pp "EfTotalPos")
;; all p^(F -> TotalPos p^)
(pp "TotalVar")
;; all alpha Total alpha
(pp "NatLeToLtSucc")
;; all n,m(n<=m -> n<Succ m)

(set-totality-goal "NP")
(fold-alltotal)
(use "CVIndPvar")
;; ...
(save-totality)

;; Exercise 16.  Goal: NP and PosToNat are inverse to each other

(display-pconst "NP" "PosToNat")

;; NP
;;   comprules
;; 0	NP Zero	1
;; 1	NP(Succ Zero)	1
;; 2	NP(Succ(Succ n)) [if (NatEven n)
;;                           (SZero(NP(Succ(NatHalf n))))
;;                           (SOne(NP(Succ(NatHalf n))))]
;; PosToNat
;;   comprules
;; 0	PosToNat 1	Succ Zero
;; 1	PosToNat(SZero p)	NatDouble(PosToNat p)
;; 2	PosToNat(SOne p)	Succ(PosToNat(SZero p))

;; Helpful theorems
(pp "NatHalfDouble")
;; all n NatHalf(NatDouble n)=n
(pp "NatEvenDouble")
;; all n NatEven(NatDouble n)
(pp "NatHalfSuccDouble")
;; all n NatHalf(Succ(NatDouble n))=n
(pp "NatNotEvenSuccDouble")
;; all n(NatEven(Succ(NatDouble n)) -> F)
(pp "NatDoubleHalfOdd")
;; all n((NatEven n -> F) -> Succ(NatDouble(NatHalf n))=n)
(pp "EfAtom")
;; F -> all boole^ boole^

;; NatNPDoubleSucc
(set-goal "all n NP(NatDouble(Succ n))=SZero(NP(Succ n))")
;; ...
(save "NatNPDoubleSucc")

;; NatNPSuccDoubleSucc
(set-goal "all n NP(Succ(NatDouble(Succ n)))=SOne(NP(Succ n))")
;; ...
(save "NatNPSuccDoubleSucc")

;; NatNPDouble
(set-goal "all n(Zero<n ->  NP(NatDouble n)=SZero(NP n))")
;; ...
(save "NatNPDouble")

;; NatNPSuccDouble
(set-goal "all n(Zero<n ->  NP(Succ(NatDouble n))=SOne(NP n))")
;; ...
(save "NatNPSuccDouble")

;; Helpful commands for the next theorems:
;; assume use simp ng ind cases

;; Helpful theorem
(pp "NatLtZeroPosToNat")
;; all p Zero<p

;; NPCircPosToNatId
(set-goal "all p NP(PosToNat p)=p")
(ind)
;; ...
(save "NPCircPosToNatId")

( pp "NP2CompRule")

;; all n^ 
;;  NP(Succ(Succ n^))eqd
;;  [if (NatEven n^) (SZero(NP(Succ(NatHalf n^)))) (SOne(NP(Succ(NatHalf n^))))]

(display-pconst "PosToNat")
;; 1	PosToNat(SZero p)	NatDouble(PosToNat p)
;; 2	PosToNat(SOne p)	Succ(PosToNat(SZero p))

;; Helpful theorems
(pp "NatNPDouble")
;; all n(Zero<n -> NP(NatDouble n)=SZero(NP n))
(pp "NatNPSuccDouble")
;; all n(Zero<n -> NP(Succ(NatDouble n))=SOne(NP n))
(pp "NatDoubleSuccHalfEven")
;; all n(NatEven n -> NatDouble(Succ(NatHalf n))=Succ(Succ n))
(pp "NatDoubleHalfOdd")
;; all n((NatEven n -> F) -> Succ(NatDouble(NatHalf n))=n)
(pp "NatHalfLe")
;; all n NatHalf n<=n

;; PosToNatCircNPIdSucc
(set-goal "all n PosToNat(NP(Succ n))=Succ n")
(use "CVIndPvar")
;; ...
(save "PosToNatCircNPIdSucc")

;; PosToNatCircNPId
(set-goal "all n(Zero<n -> PosToNat(NP n)=n)")
;; ...
(save "PosToNatCircNPId")