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

;; (display-idpc "Eq")

;; The rules (minus induction) are avaliable as Axioms:
(pp "Refl")
(pp "Sym")
(pp "Trans")
(pp "Suc")

;; 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 x x")
;; using the induction axiom should automatically substitute the correct formula for 'P'
(use "Induction")
;; ?^3:all x(Eq x x -> Eq(S x)(S x))
;; ?^2:Eq(Z alpha)(Z alpha)
(use "Refl")
(assume "x" "x=x")
(use "Suc")
(use "x=x")
;; finished proofs can be saved under a "thm-name"
(save "TheoremName")
;; can later be 'used' under that name

;;;;;;;;;;;;;;;;;
;; Exercise 13 ;;
;;;;;;;;;;;;;;;;;


(set-goal "Eq (Z alpha) (S (Z alpha)) -> all x,y(Eq x y)")
(assume "0=1")
(cut "all x Eq (Z alpha) x")
(assume "CutHyp")
;; ...

;;;;;;;;;;;;;;;;;
;; Exercise 14 ;;
;;;;;;;;;;;;;;;;;

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

(set-goal "(((A -> bot) -> bot) -> A) -> (bot -> B) -> ((A -> B) -> A) -> A")
;; ...

(set-goal "(((C -> bot) -> bot) -> C) -> (((A -> C) -> bot) -> ((B -> C) -> bot) -> bot) -> A -> B -> C")
;; ...