;; 2022-06-19.  ueb09.scm

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

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

;; Ddding predicate 'Even'

(add-ids (list (list "Even" (make-arity (py "nat")) "nat"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))" "GenEven"))

(display-idpc "Even")
(display-idpc "TotalNat")
(display-idpc "CoTotalNat")

;; Exercise 31 (a)
(set-goal "allnc n^(Even n^ -> TotalNat n^)")
;; ...

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; Ex 31 (b)
(set-goal "allnc n^(TotalNat n^ -> CoTotalNat n^)")
(assume "n^" "Tn")
(coind "Tn")
;; ...

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(ppc neterm)

;; Exercise 32.  Inversion property of Even

;; We will need ex-falso-quodlibet for Even:

;; EfEven
(set-goal "allnc n^(F -> Even n^)")
(assume "n^" "Absurd")
(simp (pf "n^ eqd 0"))
(use "InitEven")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfEven")

;; We also need that Succ is injective

;; SuccInj
(set-goal "allnc n^,m^(Succ n^ eqd Succ m^ -> n^ eqd m^)")
(assume "n^" "m^"  "Sn=Sm")
;; Injectivity of constructors can be proven using
;; 'constructor-eqd-imp-args-eqd-proof'
(pp (rename-variables (proof-to-formula (constructor-eqd-imp-args-eqd-proof
					 (pf "Succ n^ eqd Succ m^")))))
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ n^ eqd Succ m^")))
(use "Sn=Sm")
;; Proof finished.
;; (cp)
(save "SuccInj")

;; Disjointness of constructors can be proven using
;; 'constructors-overlap-imp-falsity-proof', e.g.

(set-goal "all n^ (Succ n^ eqd 0 -> F)")
(assume "n^" "Sn=0")
(use "EqDTrueToAtom")
;; it takes a formula and in case of non-nullary constructos also some terms
(use (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0"))
     (pt "n^"))
(use "Sn=0")
;; Proof finished.
;; (cp)

 ;; EvenInversion
(set-goal "allnc n^(Even(Succ(Succ n^)) -> Even n^)")
(assume "n^" "ESSn")
(assert "allnc n^0(Even n^0 -> n^0 eqd Succ(Succ n^) -> Even n^)")
(assume "n^0" "En0")
(elim "En0")
;; Base
(assume "0=SSn")
(use "EfEven")
(use "EqDTrueToAtom")
(use (constructors-overlap-imp-falsity-proof (pf "0 eqd Succ(Succ n^)"))
     (pt "n^"))
;; ...

(define eterm (proof-to-extracted-term))
(animate "EfEven")
(define neterm (rename-variables (nt eterm)))
(ppc neterm)

;; Exercise 35 (b).  quotrem

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

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

(add-var-name "k" (py "nat"))

;; QR
(set-goal "all m,n exd k exl l(n=(m+1)*k+l andnc l<m+1)")
(assume "m")
(ind)
;; 3,4
;; Base
...
;; 4
;; Step
(assume "n" "IH")
(by-assume "IH" "k" "kProp")
(by-assume "kProp" "l" "klProp")
(cases (pt "l<m"))
;; ...

(define eterm (proof-to-extracted-term))
(add-var-name "nm" (py "nat yprod nat"))
(define neterm (rename-variables (nt eterm)))
(ppc neterm)

(pp (nt (mk-term-in-app-form neterm (pt "2") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "5") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "54"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "754")))) 
;; 107 pair 5

(define expr (term-to-scheme-expr neterm))

(((ev expr) 6) 754)
;; (107 . 5)

(((ev expr) 682) 387688)
;; (567 . 427)

;; (+ (* 567 683) 427)
;; 387688

;; Exercise 36 (b).  RatBound

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

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

(remove-theorem "RatLeBound")
(remove-theorem "RatLePosExpTwo")
(remove-theorem "RatLePosExpTwoMinus")

(display-pconst "PosLog")

;; PosLog
;;   comprules
;; 0	PosLog 1	Zero
;; 1	PosLog(SZero p)	Succ(PosLog p)
;; 2	PosLog(SOne p)	Succ(PosLog p)

(pp "PosLtExpTwoSuccLog")
;; all p p<2**Succ(PosLog p)

(pp "PosLeExpTwoLog")
;; all p 2**PosLog p<=p

(pp "PosLeMonTimes")
;; all p,q,r,r0(p<=q -> r<=r0 -> p*r<=q*r0)

;; RatLePosExpTwo
(set-goal "all p,q (p#q)<=(2**Succ(PosLog p)#2**PosLog q)")
(assume "p" "q")
(ng)
(assert "p<2*2**PosLog p")
 (use "PosLtExpTwoSuccLog")
(assume "Assertion")
(use "PosLeTrans" (pt "2*2**PosLog p*2**PosLog q"))
(use "PosLeMonTimes")
(use "PosLtToLe")
(use "Assertion")
(use "Truth")
(ng)
(use "PosLeExpTwoLog")
;; Proof finished.
;; (cp)
(save "RatLePosExpTwo")

;; RatLePosExpTwoMinus
(set-goal "all n,m (2**n#2**m)<=2**(n--m)")
(ind)
;; ...

;; RatLeBound
(set-goal "all p,q exl n (p#q)<=2**n")
;; ...

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)