;; 2014-04-28.  quotrem.scm

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

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

(display-pconst "NatPlus")
(display-pconst "Pred")
(display-pconst "NatMinus")
(display-pconst "NatTimes")
(display-pconst "NatLt")
(display-pconst "NatLe")

;;   We add l as a variable name of type nat
(add-var-name "l" (py "nat"))

;; QR
(set-goal "all m,n ex k,l(n=(m+1)*k+l & l<m+1)")
(assume "m")
(ind)
;; Base
(ex-intro (pt "0"))
(ex-intro (pt "0"))
(split)
(use "Truth")
(use "Truth")
;; Step
(assume "n" "IH")
(by-assume "IH" "k" "kProp")
(by-assume "kProp" "l" "klProp")
(cases (pt "l<m"))

;; Case l<m
(assume "l<m")
(ex-intro (pt "k"))
(ex-intro (pt "l+1"))
(ng)
(split)
(use "klProp")
(use "l<m")

;; Case l<m -> F
(assume "l<m -> F")
(ex-intro (pt "k+1"))
(ex-intro (pt "0"))
(ng)
(split)
(assert "l=m")
 (use "NatLeAntiSym")
 (use "NatLtSuccToLe")
 (use "klProp")
 (use "NatNotLtToLe")
 (use "l<m -> F")
(assume "l=m")
(simphyp-with-to "klProp" "l=m" "klPropSimp")
(use "klPropSimp")
(use "Truth")
;; Proof finished.
(save "QR")

(define eterm (proof-to-extracted-term))
(add-var-name "p" (py "nat@@nat"))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "754"))))

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

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

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