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

(add-var-name "x" "y" "z" (py "alpha"))

;; Adding constants
(add-program-constant "Suc" (py "alpha=>alpha") t-deg-one 'const 1)
(add-prefix-display-string "Suc" "S")

(add-program-constant "Plus" (py "alpha=>alpha=>alpha") t-deg-one 'add-op 1)
(add-infix-display-string "Plus" "+" 'add-op)

(add-program-constant "Z" (py "alpha") t-deg-one 'const)
;; is written as '(null alpha)' for reasons
(pp (pt "(Z alpha)"))

(add-ids (list (list "Eq" (make-arity (py "alpha") (py "alpha"))))
	 '("all x Eq x x" "Refl")
	 '("all x,y(Eq x y -> Eq y x)" "Sym")
	 '("all x,y,z(Eq x y -> Eq y z -> Eq x z)" "Trans")
	 '("all x,y(Eq x y -> Eq (S x)(S y))" "Suc")
	 '("all x(Eq (x+(Z alpha)) x)" "PlusZero")
	 '("all x,y(Eq (x + S y) (S(x+y)))" "PlusSuc"))

;; (display-idpc "Eq")

;; We add the ind-rule as global assumption
(add-pvar-name "P" (make-arity (py "alpha")))
(add-global-assumption "Induction" (pf "P (Z alpha) -> all x(P x -> P(S x)) -> all x P x"))

(set-goal "all x Eq ((Z alpha)+x) x")
;; ...
(save "ZeroPlus")

(set-goal "all y,x(Eq (S x+ y) (S(x+y)))")
;; ...
(save "SucPlus")

(set-goal "all x,y(Eq (x+y) (y+x))")