;; 2021-11-06.  intronum.scm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Example: commutativity of NatPlus
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

(add-algs "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-var-name "n" "m" "l" (py "nat"))

(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)))))

;; The functions make-numeric-term (used by the parser) and
;; is-numeric-term?, numeric-term-to-number (used by term-to-expr and
;; token-tree-to-string) take either pos or nat as default.

(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)))

;; Program constants.

(add-program-constant "NatPlus" (py "nat=>nat=>nat"))
(add-program-constant "NatTimes" (py "nat=>nat=>nat"))
(add-program-constant "NatLt" (py "nat=>nat=>boole"))
(add-program-constant "NatLe" (py "nat=>nat=>boole"))
(add-program-constant "Pred" (py "nat=>nat"))
(add-program-constant "NatMinus" (py "nat=>nat=>nat"))
(add-program-constant "NatMax" (py "nat=>nat=>nat"))
(add-program-constant "NatMin" (py "nat=>nat=>nat"))
(add-program-constant "AllBNat" (py "nat=>(nat=>boole)=>boole"))
(add-program-constant "ExBNat" (py "nat=>(nat=>boole)=>boole"))
(add-program-constant "NatLeast" (py "nat=>(nat=>boole)=>nat"))
(add-program-constant "NatLeastUp" (py "nat=>nat=>(nat=>boole)=>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)

(add-totality "nat")
;; ok, inductively defined predicate constant TotalNat added

(display-idpc "TotalNat")
;; TotalNat	with content of type nat
;; 	TotalNatZero:	TotalNat 0
;; 	TotalNatSucc:	allnc n^(TotalNat n^ -> TotalNat(Succ n^))

;; Computation rules for the program constants.

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

(term-to-t-deg (pt "NatPlus"))
;; 0

(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.
;; (cp)
(save-totality)

;; ok, computation rule n+0 -> n added
;; ok, computation rule n+Succ m -> Succ(n+m) added
;; ok, NatPlusTotal added as a new theorem.

(term-to-t-deg (pt "NatPlus"))
;; 1

(set-goal "all n 0+n=n")
(ind)
(use "Truth")
(assume "n" "IH")
(use "IH")
;; Proof finished.
;; (cp)
(add-rewrite-rule "0+n" "n")

(set-goal "all n,m Succ n+m=Succ(n+m)")
(assume "n")
(ind)
(use "Truth")
(assume "m" "IH")
(use "IH")
;; Proof finished.
;; (cp)
(add-rewrite-rule "Succ n+m" "Succ(n+m)")

;; NatPlusComm
(set-goal "all n,m n+m=m+n")
(assume "n")
(ind)
(use "Truth")
(assume "m" "IH")
(use "IH")
;; Proof finished.
;; (cp)
(save "NatPlusComm")

(display-pconst "NatPlus")
(search-about "Nat" "Plus")
(search-about 'all "Nat" "Plus")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; pos, int and rat
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
(set! COMMENT-FLAG #t)

;; We overload operators like +,*,/,<=,<, and automatically raise the
;; type of arguments when reading.  For instance, + should take its
;; arguments, compute the lub rho of their types, raise the type of
;; both arguments to type rho, apply RhoPlus to the results.
;; Moreover, a number should be displayed at the lowest possible
;; level.

(display-alg "nat" "pos" "int" "rat")

(display-default-varnames)

(pp (pt "n+p"))

;; ppn (pretty print with names) shows the internal conversions (coercions)

(ppn (pt "n+p"))
;; (n NatPlus (PosToNat p))

(ppn (pt "n+k"))
;; ((NatToInt n) IntPlus k)

(ppn (pt "n+a"))
;; (((NatToInt n) RatConstr 1) RatPlus a)

(ppn (pt "p+k"))
;; ((IntPos p) IntPlus k)

(ppn (pt "p+a"))
;; (((IntPos p) RatConstr 1) RatPlus a)

(ppn (pt "k+a"))

(display-pconst "PosToNat" "NatToPos" "NatToInt")

(ppn (pt "Succ Zero+2"))
;; ((Succ Zero) NatPlus (PosToNat 2))

(ppn (pt "Succ Zero+IntPos 2"))
;; ((NatToInt (Succ Zero)) IntPlus (IntPos 2))

(ppn (pt "Succ Zero+(2#3)"))

;; (((NatToInt (Succ Zero)) RatConstr 1)
;;   RatPlus
;;   ((IntPos 2) RatConstr 3))

(pp (pt "Succ Zero+(2#3)"))
;; Succ Zero+(2#3)

(pp (nt (pt "Succ Zero+(2#3)")))
;; 5#3

(ppn (nt (pt "Succ Zero+(2#3)")))
;; ((IntPos 5) RatConstr 3)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Example for program extraction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

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

(add-var-name "k" (py "nat"))

;; QR
(set-goal "all m,n exi k,l(n=(m+1)*k+l andi l<m+1)")
(assume "m")
(ind)
;; Base
(intro 0 (pt "0"))
(intro 0 (pt "0"))
(split)
(use "Truth")
(use "Truth")
;; Step
(assume "n" "IH")
(by-assume "IH" "k" "kProp")
(by-assume "kProp" "l" "klProp")
(cases (pt "l<m"))

;; Case l<m
(assume "l<m")
(intro 0 (pt "k"))
(intro 0 (pt "l+1"))
(ng)
(split)
(use "klProp")
(use "l<m")

;; Case l<m -> F
(assume "l<m -> F")
(intro 0 (pt "k+1"))
(intro 0 (pt "0"))
(ng)
(split)
(assert "l=m")
 (use "NatLeAntiSym")
 (use "NatLtSuccToLe")
 (use "klProp")
 (use "NatNotLtToLe")
 (use "l<m -> F")
;; Assertion proved.
(assume "l=m")
(simphyp-with-to "klProp" "l=m" "klPropSimp")
(use "klPropSimp")
(use "Truth")
;; Proof finished.
;; (cdp)
;; (cp)
(save "QR")

(define eterm (proof-to-extracted-term))
(add-var-name "p" (py "nat yprod nat"))
(define neterm (rename-variables (nt eterm)))

(ppc neterm)

;; [n,n0](Rec nat=>nat yprod nat)n0(0 pair 0)
;;  ([n1,p][case p
;;      (n2 pair n3 -> 
;;      [case (n3<n) (True -> n2 pair Succ n3) (False -> Succ n2 pair 0)])])

(pp (nt (mk-term-in-app-form neterm (pt "2") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "5") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "54"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "754"))))
;; 107 pair 5

(define expr (term-to-scheme-expr neterm))

;; expr

;; (lambda (n)
;;   (lambda (n0)
;;     (((natRec n0) (cons 0 0))
;;       (lambda (n1)
;;         (lambda (p)
;;           (((lambda (n2)
;;               (lambda (n3)
;;                 (if (< n3 n) (cons n2 (+ n3 1)) (cons (+ n2 1) 0))))
;;              (car p))
;;             (cdr p)))))))

(((ev expr) 6) 754)
;; (107 . 5)

(((ev expr) 682) 387688)
;; (567 . 427)

;; (+ (* 567 683) 427)
;; 387688

(add-sound "QR)