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

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

(add-var-name "l" (py "nat"))
(add-var-name "p" (py "nat yprod nat"))

;; The graph of the Fibonacci function:

(add-ids
 (list (list "G" (make-arity (py "nat") (py "nat"))))
 '("G 0 0" "InitGZero")
 '("G 1 1" "InitGOne")
 '("all n,k,l(G n k -> G(n+1)l -> G(n+2)(k+l))" "GenG"))

;; Fibonacci
(set-goal "all n exl k G n k")
(assert "all n exd k exl l(G n k andu G(n+1)l)")
 (ind)
 (intro 0 ...)
 (intro 0 ...)
 (split)
 (use ...)
 (use ...)
 (assume "n" "IH")
 (by-assume "IH" "k" "IHk")
 (by-assume "IHk" "l" "IHl")
 (intro 0 ...)
 (intro 0 ...)
 (split)
 (use ...)
 (use ...)
 (use ...)
 (use ...)
(assume "Assertion" "n")
(inst-with-to "Assertion" (pt "n") "Exkl")
(drop "Assertion")
(by-assume "Exkl" "k" "Exl")
(by-assume "Exl" "l" "klProp")
(intro 0 (pt "k"))
(use "klProp")
;; Proof finished.
(save "Fibonacci")

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

(pp (term-to-type (pt "(Rec nat=>nat yprod nat)")))

(ppc neterm)

(pp (nt (make-term-in-app-form neterm (pt "0")))) ;"0"
(pp (nt (make-term-in-app-form neterm (pt "1")))) ;"1"
(pp (nt (make-term-in-app-form neterm (pt "2")))) ;"1"
(pp (nt (make-term-in-app-form neterm (pt "3")))) ;"2"
(pp (nt (make-term-in-app-form neterm (pt "4")))) ;"3"
(pp (nt (make-term-in-app-form neterm (pt "8")))) ;"21"
(pp (nt (make-term-in-app-form neterm (pt "10")))) ;"55"
(pp (nt (make-term-in-app-form neterm (pt "12")))) ;"144"