;; 2024-12-08,  ueb09.scm

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

;; Copy the file nat1.scm from the website of the lecture course and
;; load it by replacing ""~/wwwpublic/lectures/logic/ws24/" by the
;; directory containing nat1.scm.

(set! COMMENT-FLAG #f)
(load "~/wwwpublic/lectures/logic/ws24/nat1.scm")
(set! COMMENT-FLAG #t)

(add-pvar-name "P" (make-arity (py "nat")))

(add-global-assumption
 "Induction"
 (pf "P^ 0 -> all n(P^ n -> P^(Succ n)) -> all n P^ n"))

;; (a).  By loading nat1.scm, for equality on natural numbers some
;; rewrite rules are available:

(pp (nf (pf "Succ n=Succ m")))
;; n=m

(pp (nf (pf "Succ n=0")))
;; F

(pp (nf (pf "0=Succ m")))
;; F

(pp (nf (pf "0=0")))
;; T

;; EfNatEq
(set-goal "F -> all n,m n=m")
(assume "Absurd")
(use "Induction")
;; 3,4
(use "Induction")
;; 5,6
(use "Truth")
;; 6
(assume "n" "IHn")
(ng #t)
(use "Absurd")
;; ...

;; (cp)
(save "EfNatEq")

(pp "EfNatEq")
(proof-to-expr-with-formulas)

(display-pconst "NatPlus")

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

;; NatPlusZero
(set-goal "all n 0+n=n")
(use "Induction")
;; ...

;; (cp)
(save "NatPlusZero")

(c)

;; NatPlusSucc
(set-goal "all n,m Succ n+m=Succ(n+m)")
(assume "n")
(use "Induction")
;; ...

;; (cp)
(save "NatPlusSucc")

(proof-to-expr-with-formulas)

(d)

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

;; (cp)
(save "NatPlusComm")

(proof-to-expr-with-formulas)