;; 2023-07-03
(load "~/git/minlog/init.scm")

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

(set-goal "all n^,m^(CoTotalNatMR n^ m^ -> CoEqPNatNc n^ m^)")
(assume "n^" "m^" "MRnm")
(coind "MRnm")
(assume "n^0" "m^0" "MRn0m0")
(inst-with-to
 (make-proof-in-aconst-form
  (coidpredconst-to-closure-aconst
   (predicate-form-to-predicate (pf "CoTotalNatMR n^ m^"))))
 (pt "n^0") (pt "m^0") "MRn0m0" "Inst")
(elim "Inst")
;; 7,8
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 8
(drop "Inst")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^1" "n1Prop")
(by-assume "n1Prop" "m^1" "n1m1Prop")
(intro 0 (pt "n^1"))
(intro 0 (pt "m^1"))
(split)
(intro 1)
(use "n1m1Prop")
(split)
(use "n1m1Prop")
(use "n1m1Prop")
;; Proof finished.
;; (cp)

(define proof (current-proof))
(define aconsts (proof-to-aconsts proof))
(map aconst-to-name aconsts)
(pp (rename-variables (aconst-to-formula (car aconsts))))
(pp (rename-variables (aconst-to-formula (car (reverse aconsts)))))

(set-goal "all n^,m^(CoEqPNatNc n^ m^ -> CoTotalNatMR n^ m^)")
(assume "n^" "m^" "EqPnm")
(coind "EqPnm")
(assume "n^0" "m^0" "EqPn0m0")
(inst-with-to
 (make-proof-in-aconst-form
  (coidpredconst-to-closure-aconst
   (predicate-form-to-predicate (pf "CoEqPNatNc n^ m^"))))
 (pt "n^0") (pt "m^0") "EqPn0m0" "Inst")
(elim "Inst")
;; 7,8
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 8
(drop "Inst")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^1" "n1Prop")
(by-assume "n1Prop" "m^1" "n1m1Prop")
(intro 0 (pt "n^1"))
(intro 0 (pt "m^1"))
(split)
(intro 1)
(use "n1m1Prop")
(split)
(use "n1m1Prop")
(use "n1m1Prop")
;; Proof finished.
;; (cp)

;; To demonstrate program extraction and verification of what is
;; extracted we use examples/analysis/sdavaux.scm