;; 2025-05-31.  solleafstotal.scm

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

(add-algs "bin" '("L" "bin") '("B" "bin=>bin=>bin"))
(add-var-name "x" "y" "z" (py "bin"))

(add-totality "bin")
(display-idpc "TotalBin")
;; ok, inductively defined predicate constant TotalBin added.

;; This adds the c.r. predicate TotalBin with clauses
;; TotalBinL:	TotalBin L
;; TotalBinB:
;;  allnc x^(TotalBin x^ -> allnc x^0(TotalBin x^0 -> TotalBin(B x^ x^0)))

(add-program-constant "Leafs" (py "bin=>nat"))
(add-computation-rules
 "Leafs L" "Succ Zero"
 "Leafs(B x y)" "Leafs x+Leafs y")

;;;; Command help
;; (use …), in particular. (use "Truth")
; →/∀-Introduction
;; (assume …)
; →/∀-Elimation
;; (simp …), (simp "<-" …)
; Simp accepts the name of a theorem or a variable(*),
; which expresses an equality (i.e., the corresponding formula should
; be of the form "… eqd …" or "… = …") and applies
; this equality to the goal.
; The theorem or variable can also express a formula of the Form A → B → … → x=y.
; In that case x=y is used on the goal and A,B,… are added as additional goals.
; Sometimes
; If the string "<-" is passed as the first argument, the replacement
; is done from right to left instead of left to right.
; Regarding (*): Simp also accepts formulas directly, i.e., one can write
; (simp (pf "n+m=m+n"));
; "n+m=m+n" will be added as an additional goal.
; Furthermore, simp can replace computably true formulas with truth.
; For example, if a:l<n is in the context, then
; (simp a) performs the replacement.
;; (ind), (ind (pt "…"))
; If the goal has the form ∀ₓA(x), then (ind) initiates an induction proof over x.
; That is, (ind) uses the the axiom of the smallest fixpoint for the totality predicate
; of the type of x if applicable. Ofc this is only possible if x is total.
; (ind (pt "…"))
;; (assert B)
; Replaces Goal A by the two goals B -> A and B
;; (pp …)
; Display a theorem
;; (ng #t)
; This command tries to normalize all terms in the goal as
; much as possible [note that it will not always do what you want]
;; (fold-alltotal)
; Convert a goal of form ∀ n^(Total…1 n^ -> …2) to ∀ n (…2)
;; (elim …)
; Use the fitting elimination axiom on the given hypothesis

;;; Example
; Note especially the usage of: fold-alltotal, ng, elim

; We proof totality of
(display-pconst "NatPlus")
; This is already known as
(pp "NatPlusTotal")

(set-goal "allnc n^(TotalNat n^ -> allnc m^(TotalNat m^ -> TotalNat (NatPlus n^ m^)))")
(fold-alltotal)
(assume "n")
(fold-alltotal)
(ind)
(ng #t)
(use "TotalVar")
(assume "n0" "IH")
(ng #t)
(use "TotalNatSucc")
(use "IH")

;; When we use (elim "Total m^") in the following
;; proof, we use the elimination axiom of the following
;; ind. def. predicate:
(display-idpc "TotalNat")

(set-goal "allnc n^(TotalNat n^ -> allnc m^(TotalNat m^ -> TotalNat (NatPlus n^ m^)))")
(assume "n^" "Total n^" "m^" "Total m^")
(elim "Total m^")
(ng #t)
(use "Total n^")
(assume "n^0" "Total n^0" "IH")
(ng #t)
(use "TotalNatSucc")
(use "IH")

;;; Exercise

;; Useful theorems
(pp "TotalVar")     ; States that all total variables are actually total
(pp "NatPlusTotal")

;; Using the elimination axiom for TotalBin
(set-totality-goal "Leafs")
;; TODO

;; Proof finished.
(cp)
(proof-to-expr-with-formulas)

;; With fold-alltotal
(set-totality-goal "Leafs")
;; TODO

;; Proof finished.
(cp)
(proof-to-expr-with-formulas)