;; 20230621.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)))

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

;; End of initial parts of lib/nat.scm

;; Initial parts of lib/list.scm

(add-algs "list" 'prefix-typeop
	  '("list" "Nil")
	  '("alpha=>list=>list" "Cons"))

(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(add-token
 "::" 'pair-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (constr-name-to-constr "Cons"))
	    (uninst-type (const-to-uninst-type const))
	    (patterns (arrow-form-to-arg-types uninst-type 2)) ;al, list al
	    (instances (map term-to-type (list x y))) ;e.g.  nat, list int
	    (type1 (car instances)) ;nat
	    (type2 (car (alg-form-to-types (cadr instances)))) ;int
	    (tsubst (cond ((type-le? type1 type2)
			   (make-subst (car patterns) type2))
			  ((type-le? type2 type1)
			   (make-subst (car patterns) type1))
			  (else (myerror "comparable types expected"
					 type1 type2)))))
       (const-substitute const tsubst #f)))
    x y)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? 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=? "Cons"
			 (const-to-name (term-in-const-form-to-const op)))
	       (= 2 (length args)))
	  (list 'pair-op  "::"
		(term-to-token-tree (car args))
		(term-to-token-tree (cadr args)))
	  #f))
       #f)))

;; The postfix-op ":" with "x:" for "x::(Nil rho)" needs a special
;; treatment with explicit uses of add-token and add-display.

(add-token
 ":" 'postfix-op
 (lambda (x)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Cons"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f)))
    x
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Nil"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f))))))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? 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=? "Cons" (const-to-name
				    (term-in-const-form-to-const op)))
		  (= 2 (length args))
		  (term-in-const-form? (cadr args))
		  (string=? "Nil" (const-to-name
				   (term-in-const-form-to-const (cadr args)))))
	     (list 'postfix-op ":" (term-to-token-tree (car args)))
	     #f))
       #f)))

;; End of initial parts of lib/list.scm

;; Initial parts of lib/str.scm

(add-algs "str" 'prefix-typeop '("alpha=>str=>str" "SCons"))
(add-var-name "xstr" (py "str alpha"))
(add-infix-display-string "SCons" ":~:" 'pair-op) ;right associative

(pp (pt "x^1:~:x^2:~:x^3:~:xstr^"))

;; End of initial parts of lib/str.scm

;; Standard algebras

;; Be default we have the algebras unit boole yprod ysum uysum ysumu
;; We have added nat list str
;; We now add pos bin

(add-algs "pos" '("One" "pos") '("SZero" "pos=>pos") '("SOne" "pos=>pos"))
(add-var-name "p" "q" "r" (py "pos"))

(add-algs "bin" '("Lf" "bin") '("Br" "bin=>bin=>bin"))

(display-alg "unit" "boole" "nat" "pos" "bin")
(display-alg "list" "str")
(display-alg "yprod" "ysum" "uysum" "ysumu")

;; Program constants.

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

;; Computation rules for the program constants.

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

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

;; For NatLe
(add-computation-rules
 "0<=n" "True"
 "Succ n<=0" "False"
 "Succ n<=Succ m" "n<=m")

(display-pconst "NatPlus" "NatTimes" "NatLe")

;; The computation rules give rise to theorems, for instance

(pp "NatLe2CompRule")
;; all n^,m^ (Succ n^ <=Succ m^)eqd(n^ <=m^)

;; Here eqd denotes "Leibniz equality" between terms.  It will later
;; be defined as an "inductive predicate".

;; Types of recursion operators 

(pp (const-to-type (arrow-types-to-rec-const (py "boole=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "nat=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "pos=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "bin=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "list beta=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "beta ysum gamma=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "beta yprod gamma=>alpha"))))

(pp (make-term-in-const-form (arrow-types-to-rec-const (py "bin=>alpha"))))

;; Definition of addition for nat using recursion

(pp (pt "(Rec nat=>nat)2 3([n,l](Succ l))"))
(pp (nt (pt "(Rec nat=>nat)2 3([n,l](Succ l))")))

;; Types of destructors

(pp (const-to-type (alg-to-destr-const (py "nat"))))
(pp (const-to-type (alg-to-destr-const (py "pos"))))
(pp (const-to-type (alg-to-destr-const (py "bin"))))
(pp (const-to-type (alg-to-destr-const (py "list alpha"))))
(pp (const-to-type (alg-to-destr-const (py "str alpha"))))

(pp (make-term-in-const-form (alg-to-destr-const (py "bin"))))

;; 2023-06-12

(add-totality "nat")

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

(pp "TotalNatZero")
(pp "TotalNatSucc")

(add-eqpnc "nat")
(pp "EqPNatNcZero")

(display-pconst "NatPlus" "NatTimes" "NatLe")

(pp "NatPlus0CompRule")
(pp "NatPlus1CompRule")

(pp "AllTotalIntro")
(pp "AllTotalElim")

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

(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 (cadr aconsts))))
(pp (rename-variables (aconst-to-formula (caddr aconsts))))
(pp (rename-variables (aconst-to-formula (cadddr aconsts))))
(pp (rename-variables (aconst-to-formula (car (cddddr aconsts)))))

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

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

(display-pconst "NatPlus")
(pp "NatPlus0RewRule")

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

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

(display-pconst "NatPlus")

(set-goal "all n,m,l n+(m+l)=n+m+l")
(assume "n" "m")
(ind)
(ng #t)
(use "Truth")
(assume "l" "IH")
(ng #t)
(use "IH")
;; Proof finished.
;; (cp)
(add-rewrite-rule "n+(m+l)" "n+m+l")
(save "NatPlusAssoc")

(display-pconst "NatPlus")

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

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

(search-about "Nat" "Plus")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(add-ids (list (list "Even" (make-arity (py "nat")) "nat"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(Succ(Succ n^)))" "GenEven"))

(set-goal "allnc n^(Even n^ -> TotalNat n^)")
(assume "n^" "En")
(elim "En")
;; 3,4
(intro 0)
;; 4
(assume "m^" "Em" "Tm")
(intro 1)
(intro 1)
(use "Tm")
;; 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 (cadr aconsts))))
(pp (rename-variables (aconst-to-formula (caddr aconsts))))

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

;; Labelled natural numbers.

(add-algs "lnat"
	  '("alpha=>lnat" "LnatZero")
	  '("alpha=>lnat=>lnat" "LnatSucc"))
(add-rtotality "lnat")

(add-ids (list (list "TrCl" (make-arity (py "alpha") (py "alpha")) "lnat"))
	 '("allnc x^,y^(R x^ y^ -> TrCl x^ y^)" "InitTrCl")
	 '("allnc x^,y^,z^(R x^ y^ -> TrCl y^ z^ -> TrCl x^ z^)" "GenTrCl"))

;; Here ends 20230614.scm

(pp "InitTrCl")
;; allnc x^,y^(R x^ y^ -> (TrCl (cterm (x^0,x^1) R x^0 x^1))x^ y^)

(pp "GenTrCl")
;; allnc x^,y^,z^(
;;  R x^ y^ -> 
;;  (TrCl (cterm (x^0,x^1) R x^0 x^1))y^ z^ -> 
;;  (TrCl (cterm (x^0,x^1) R x^0 x^1))x^ z^)

(set-goal "allnc x^,y^((TrCl (cterm (x^0,x^1) R x^0 x^1))x^ y^ -> 
 allnc z^((TrCl (cterm (x^0,x^1) R x^0 x^1))y^ z^ ->
 (TrCl (cterm (x^0,x^1) R x^0 x^1))x^ z^))")
(assume "x^" "y^" "TCxy")
(elim "TCxy")
;; 3,4
(assume "x^0" "y^0" "Rx0y0" "z^" "TCy0z")
(use "GenTrCl" (pt "y^0"))
(use "Rx0y0")
(use "TCy0z")
;; 4
(assume "x^0" "x^1" "y^1" "Rx0x1" "TCx1y1" "IH" "z^" "TCy1z")
(use "GenTrCl" (pt "x^1"))
(use "Rx0x1")
(use "IH" (pt "y^1"))
(use "TCy1z")
;; 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 (cadr aconsts))))

;; In ets.scm we have

;; (add-ids (list (list "OrD" (make-arity) "ysum"))
;; 	 '("Pvar1 -> OrD" "InlOrD")
;; 	 '("Pvar2 -> OrD" "InrOrD"))

;; (add-ids (list (list "OrR" (make-arity) "uysum"))
;; 	 '("Pvar^1 -> OrR" "InlOrR")
;; 	 '("Pvar2 -> OrR" "InrOrR"))

;; (add-ids (list (list "OrL" (make-arity) "ysumu"))
;; 	 '("Pvar1 -> OrL" "InlOrL")
;; 	 '("Pvar^2 -> OrL" "InrOrL"))

;; ;; OrU has computational content, because we know on which side we are.

;; (add-ids (list (list "OrU" (make-arity) "boole"))
;; 	 '("Pvar^1 -> OrU" "InlOrU")
;; 	 '("Pvar^2 -> OrU" "InrOrU"))

;; (add-ids (list (list "OrNc" (make-arity)))
;; 	 '("Pvar^1 -> OrNc" "InlOrNc")
;; 	 '("Pvar^2 -> OrNc" "InrOrNc"))

(add-pvar-name "A" "B" "C" (make-arity))

(pp (pf "(OrD (cterm () A) (cterm () B))"))
;; A ord B

(set-goal "A ord B -> (A -> C) -> (B -> C) -> C")
(assume "Disj")
(elim "Disj")
;; 3,4
(assume "AHyp" "AImp" "Useless")
(use "AImp")
(use "AHyp")
;; 4
(assume "BHyp" "Useless" "BImp")
(use "BImp")
(use "BHyp")
;; Proof finished.
(cp)

;; Alternatively we can use auto for the final logical inferences:

(set-goal "A ord B -> (A -> C) -> (B -> C) -> C")
(assume "Disj")
(elim "Disj")
;; 3,4
(auto)
;; 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))))

(set-goal "A orl B^ -> (A -> C) -> (B^ -> C) -> C")
(assume "Disj")
(elim "Disj")
;; 3,4
(auto)
;; 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 (pf "A ori B^")) ;i for interactive
;; A orl B^

;; In ets.scm we have

;; (add-ids (list (list "ExR" (make-arity) "identity"))
;; 	 '("allnc alpha^((Pvar alpha)alpha^ -> ExR)" "InitExR"))

(pp "InitExR")
;; allnc alpha^((Pvar alpha)alpha^ -> exr alpha^0 (Pvar alpha)alpha^0)

(add-pvar-name "Q" (make-arity (py "alpha")))

(pp (pf "exr x^ Q x^"))

(set-goal "exr x^ Q x^ -> allnc x^(Q x^ -> A) -> A")
(assume "ExHyp")
(elim "ExHyp")
(auto)
;; 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))))

;; 2023-06-19.  Done up to this point.

(add-co "Even")

(pp "CoEvenClause")
;; allnc n^(
;;  CoEven n^ -> n^ eqd 0 orr exr n^0(CoEven n^0 andl n^ eqd Succ(Succ n^0)))

;; By the greatest-fixed-point (or coinduction) axiom CoEven is a
;; fixed point.  Hence the inverse implication holds as well.

;; CoEvenClauseInv
(set-goal
 "allnc n^(n^ eqd 0 orr exr n^0(CoEven n^0 andl n^ eqd Succ(Succ n^0)) ->
 CoEven n^)")
(assume "n^" "Disj")
(coind "Disj")
;; 2,3
(drop "Disj")
(assume "n^1" "n1Prop")
(elim "n1Prop")
;; 6,7
(drop "n1Prop")
(assume "n1=0")
(intro 0)
(use "n1=0")
;; 7
(drop "n1Prop")
(assume "ExHyp")
(by-assume "ExHyp" "n^2" "n2Prop")
(intro 1)
(intro 0 (pt "n^2"))
(split)
(intro 0)
(use "n2Prop")
(use "n2Prop")
;; Proof finished.
;; (cp)
(save "CoEvenClauseInv")

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

;; We can split this proposition into two, i.e., show that CoEven
;; satisfies the clauses of Even.

(pp "InitEven")
;; Even 0
(pp "GenEven")
;; allnc n^(Even n^ -> Even(Succ(Succ n^)))

;; InitCoEven
(set-goal "CoEven 0")
(use "CoEvenClauseInv")
(intro 0)
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "InitCoEven")

;; GenCoEven
(set-goal "allnc n^(CoEven n^ -> CoEven(Succ(Succ n^)))")
(assume "n^" "CoEn")
(use "CoEvenClauseInv")
(intro 1)
(intro 0 (pt "n^"))
(split)
(use "CoEn")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "GenCoEven")

;; Since Even is the least predicate satifying its clauses Even is a
;; subset of CoEven.

;; EvenToCoEven
(set-goal "allnc n^(Even n^ -> CoEven n^)")
(assume "n^" "En")
(elim "En")
;; 3,4
(use "InitCoEven")
;; 4
(assume "n^1" "Useless")
(use "GenCoEven")
;; Proof finished.
;; (cp)
(save "EvenToCoEven")

;; Leibniz equality.

;; In ets.scm

;; (add-ids (list (list "EqD" (make-arity (py "alpha") (py "alpha"))))
;; 	 '("allnc alpha^ EqD alpha^ alpha^" "InitEqD"))

(pp "EqDCompat")
(pp "EfEqD")
(pp "EfAtom")

;; EfTotalNat
(set-goal "allnc n^(F -> TotalNat n^)")
(assume "n^" "Absurd")
(simp (pf "n^ eqd 0"))
(intro 0)
;;(pp "TotalNatZero")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfTotalNat")

;; EfEven
(set-goal "allnc n^(F -> Even n^)")
(assume "n^" "Absurd")
(simp (pf "n^ eqd 0"))
(intro 0)
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfEven")

;; EfCoEven
(set-goal "allnc n^(F -> CoEven n^)")
(assume "n^" "Absurd")
(assert "Even n^")
(use "EfEven")
(use "Absurd")
(use "EvenToCoEven")
;; Proof finished.
;; (cp)
(save "EfCoEven")

(define proof (current-proof))
(define aconsts (proof-to-aconsts proof))
(map aconst-to-name aconsts)