;; 2022-06-19.  ueb10.scm

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

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

;; Add 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")

;; Exercise 38

;; Adding predicate Odd

(add-ids (list (list "Odd" (make-arity (py "nat")) "nat"))
	 '("Odd 1" "InitOdd")
	 '("allnc n^(Odd n^ -> Odd ((Succ(Succ n^))))" "GenOdd"))

(display-idpc "Odd")

(add-pvar-name "X" (make-arity (py "nat")))

;; Display the elim aconst
(pp (rename-variables
     (aconst-to-formula (imp-formulas-to-elim-aconst (pf "Odd n^ -> X n^")))))

(display-pconst "NatDouble")

;; We can ouput the type of the formula to be proven
(pp (formula-to-et-type (pf "allnc n^(Odd n^ -> Even(NatDouble n^))")))

(set-goal "allnc n^(Odd n^ -> Even(NatDouble n^))")
;; ...

(define proof (current-proof))
(proof-to-expr-with-formulas proof)

(define eterm (proof-to-extracted-term proof))

(pp (rename-variables (nt eterm)))

(pp (nt (make-term-in-app-form eterm (pt "0"))))
(pp (nt (make-term-in-app-form eterm (pt "1"))))
(pp (nt (make-term-in-app-form eterm (pt "2"))))
(pp (nt (make-term-in-app-form eterm (pt "3"))))
(pp (nt (make-term-in-app-form eterm (pt "4"))))

;; Exercise 40.  Inversion property of CoEven

;; Adding the co-variant of Even
(add-co "Even")

(pp "CoEvenClause")

;; allnc n^(CoEven n^ -> n^ eqd 0 orr exr n^0(CoEven n^0 andl n^ eqd n^0+2))

;; CoEvenInvAux
(set-goal "allnc n^(exr m^(n^ eqd m^ +2 andr CoEven m^) -> CoEven n^)")
(assume "m^" "Exm")
(coind "Exm")
;; ...
(save "CoEvenInvAux")

;; Now we can derive the original goal.

;; CoEvenInv
(set-goal "allnc n^(CoEven n^ -> CoEven(n^ +2))")
;; ...

(define eterm (proof-to-extracted-term))
(animate "CoEvenInvAux")
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; ...