;; ueb04.scm  ueb04.scm

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

(add-algs "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-var-name "n" "m" "l" (py "nat")) ;l instead of k, which will be an int

(define (make-numeric-term-wrt-nat n)
  (if (= n 0)
      (pt "Zero")
      (make-term-in-app-form
       (pt "Succ")
       (make-numeric-term-wrt-nat (- n 1)))))

(define NAT-NUMBERS #t)

(define (make-numeric-term x)
  (if NAT-NUMBERS
      (make-numeric-term-wrt-nat x)
      (make-numeric-term-wrt-pos x)))

(define (is-numeric-term? x)
  (if NAT-NUMBERS
      (is-numeric-term-wrt-nat? x)
      (is-numeric-term-wrt-pos? x)))

(define (numeric-term-to-number x)
  (if NAT-NUMBERS
      (numeric-term-wrt-nat-to-number x)
      (numeric-term-wrt-pos-to-number x)))

(add-totality "nat")

;; This adds the c.r. predicate TotalNat with clauses
;; TotalNatZero:	TotalNat Zero
;; TotalNatSucc:	allnc nat^(TotalNat nat^ -> TotalNat(Succ nat^))

;; NatTotalVar
(set-goal "all n TotalNat n")
(use "AllTotalIntro")
(assume "n^" "Tn")
(use "Tn")
;; Proof finished
;; (cdp)
(save "NatTotalVar")

(add-program-constant "NatPlus" (py "nat=>nat=>nat"))

;; Tokens used by the parser.

(define (add-nat-tokens)
  (let* ((make-type-string
	  (lambda (type op-string type-strings)
	    (let* ((string (type-to-string type))
		   (l (string->list string)))
	      (if (member string type-strings)
		  (list->string (cons (char-upcase (car l)) (cdr l)))
		  (myerror op-string "unexpected type" type)))))
	 (tc ;term-creator
	  (lambda (op-string . type-strings)
	    (lambda (x y)
	      (let* ((type (term-to-type x))
		     (type-string
		      (make-type-string type op-string type-strings))
		     (internal-name (string-append type-string op-string)))
		(mk-term-in-app-form
		 (make-term-in-const-form
		  (pconst-name-to-pconst internal-name))
		 x y))))))
    (add-token "+" 'add-op (tc "Plus" "nat"))
    (add-token "*" 'mul-op (tc "Times" "nat"))
    (add-token "<" 'rel-op (tc "Lt" "nat"))
    (add-token "<=" 'rel-op (tc "Le" "nat"))
    (add-token "--" 'add-op (tc "Minus" "nat"))
    (add-token "max" 'mul-op (tc "Max" "nat"))
    (add-token "min" 'mul-op (tc "Min" "nat"))))

(add-nat-tokens)

;; (add-nat-display) updates DISPLAY-FUNCTIONS, so that it uses the
;; tokens introduced by (add-nat-tokens).

(define (add-nat-display)
  (let ((dc ;display-creator
	 (lambda (name display-string token-type)
	   (lambda (x)
	     (let ((op (term-in-app-form-to-final-op x))
		   (args (term-in-app-form-to-args x)))
	       (if (and (term-in-const-form? op)
			(string=? name (const-to-name
					(term-in-const-form-to-const op)))
			(= 2 (length args)))
		   (list token-type display-string
			 (term-to-token-tree (term-to-original (car args)))
			 (term-to-token-tree (term-to-original (cadr args))))
		   #f))))))
    (add-display (py "nat") (dc "NatPlus" "+" 'add-op))
    (add-display (py "nat") (dc "NatTimes" "*" 'mul-op))
    (add-display (py "boole") (dc "NatLt" "<" 'rel-op))
    (add-display (py "boole") (dc "NatLe" "<=" 'rel-op))
    (add-display (py "nat") (dc "NatMinus" "--" 'add-op))
    (add-display (py "nat") (dc "NatMax" "max" 'mul-op))
    (add-display (py "nat") (dc "NatMin" "min" 'mul-op))))

(add-nat-display)

;; Computation rules for the program constants.

;; For NatPlus
(add-computation-rules
 "n+0" "n"
 "n+Succ m" "Succ(n+m)")

(set-totality-goal "NatPlus")
(fold-alltotal)
(assume "n")
(fold-alltotal)
(ind)
;; 5,6
(use "TotalVar")
;; 6
(assume "m" "IH")
(ng #t)
(use "TotalNatSucc")
(use "IH")
;; Proof finished.
;; (cdp)
(save-totality)

(display-pconst "NatPlus")

;; NatPlus
;;   comprules
;; 0	n+0	n
;; 1	n+Succ m	Succ(n+m)

;; Here the work starts.

(set-goal "all n 0+n=n")
(ind)
;; 2,3
;; Base
(use "Truth") ;by NatPlus0CompRule
;; Step
(assume "n" "IH")
(use "IH") ;by NatPlus1CompRule and injectivity of Succ
;; Proof finished.
;; (cdp)
(add-rewrite-rule "0+n" "n")

(display-pconst "NatPlus")

;; NatPlus
;;   comprules
;; 0	n+0	n
;; 1	n+Succ m	Succ(n+m)
;;   rewrules
;; 0	0+n	n

(set-goal "all n,m Succ n+m=Succ(n+m)")
(assume "n")
(ind)
...

(add-rewrite-rule "Succ n+m" "Succ(n+m)")

(display-pconst "NatPlus")

;; NatPlus
;;   comprules
;; 0	n+0	n
;; 1	n+Succ m	Succ(n+m)
;;   rewrules
;; 0	0+n	n
;; 1	Succ n+m	Succ(n+m)

(set-goal "all n,m,l n+(m+l)=n+m+l")
(assume "n" "m")
(ind)
...

(add-rewrite-rule "n+(m+l)" "n+m+l")
(save "NatPlusAssoc")

(display-pconst "NatPlus")

;; NatPlus
;;   comprules
;; 0	n+0	n
;; 1	n+Succ m	Succ(n+m)
;;   rewrules
;; 0	0+n	n
;; 1	Succ n+m	Succ(n+m)
;; 2	n+(m+l)	n+m+l

;; NatPlusComm
(set-goal "all n,m n+m=m+n")
...