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

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

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

(add-pvar-name "G" "H" (make-arity (py "alpha") (py "beta")))
(add-var-name "z" (py "beta"))

;; forall-introduction is similar to implication-introduction with
;; '(assume "varnameindex")'
(set-goal "all x C x")
;; ?_1:all x C x
(assume "x")
;;   x
;; --------
;; ?_2:C x

;; forall-elimination works automatically most of the time
(set-goal "all x C x -> all x C x")
(assume "AllHyp" "x0")
;; AllHyp:all x C x
;;   x0
;; ---------
;; ?_2:C x0
(use "AllHyp")
;; > ok, ?_2 is proved.  Proof finished.

;; All-formulas in assumption-variables can also be instantiated directly
(set-goal "all x C x -> B")
(assume "u")
(inst-with-to "u" (pt "y1") "y1Hyp")
;; u:all x C x
;;   y1Hyp:C y1
;; -------------
;; ?_4:B

;; existence introduction with '(intro 0 (pt "term"))'
(set-goal "exd x C x")
;; ?_1:exd x C x
(intro 0 (pt "x2"))
;;   x2
;; --------
;; ?_2:C x2

;; existence elimination either by using '(elim)' on a goal-formula 'exd x P x -> A',
(set-goal "exd x C x -> A")
(elim)
(assume "x0" "x0Hyp")
;; 1:exd x P x
;;   x0  x0Hyp:C x0
;; -----------------
;; ?_3:A

;; or '(elim "u")' , where 'u: exd x P x' is an existance-formula in the context
(undo 2)
(assume "u")
(elim "u")
(assume "y23" "Cy23")
;; u:exd x C x
;;   y23  Cy23:P x0
;; -----------------
;; ?_4:A


;; or with '(by-assume "avar-name" "var-name" "new-avar-name")'
(undo 3)
(assume "ExHyp")
(by-assume "ExHyp" "y" "yHyp")
;;  y  yHyp:C y
;; -------------
;; ?_5:A

;; forward reasoning is also possible with the commands '(assert "formula")' and '(cut "formula")'. If the goal was e.g., "A", then '(assert "B")' generates two new goals: "B" and "B -> A"
(set-goal "A")
(assert "B")
;; > ok, goal 1 can be obtained from
;; ?_2:B -> A
;; ?_3:B

;; '(cut ..)' is the same up to the order of goals
(undo)
(cut "B")
;; > ok, goal 1 can be obtained from
;; ?_3:B
;; ?_2:B -> A

;; Note that the formulae 'G' and 'H' expect different types of variables as their two arguments. Namely, names '"x","x1",...,"y","y0",...' are eligible for the first argument and '"z","z0","z1",...' for the second
(pp (pf "H y1 z0"))
;; > H y1 z0
;; otherwise
;; (pp (pf "G y0 y1"))
;; ...
;; Exception in Minlog: sorry

;; -----------------------;;
;; Exercice 9 derivations ;;
;; -----------------------;;

;; We add the induction-hypotheses as axioms (=global assumption)
(add-global-assumption "IhC" "all x(bot -> C x)")
(add-global-assumption "IhB" "bot -> B")
(add-global-assumption "IhA" "bot -> A")

;; the may be used via their name
(set-goal "B")
(use "IhB")
;; > ok, goal 1 can be obtained from
;; ?_2:bot

;; i)
(set-goal "bot -> exd x C x")
(assume "Hyp")
;; ...

;; ii)
(set-goal "bot ->  all x C x")
;; ...

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

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

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

;; ------------------------;;
;; Exercice 10 derivations ;;
;; ------------------------;;

;; i)
(set-goal "exd x all z (G0 x z -> H x z) -> all x,z(G1 x z -> G0 x z) -> all z exd x (G1 x z -> H x z)")
;; ...

;; ii)
(set-goal "(((B -> bot) -> bot) -> B) -> (((A -> bot) -> bot) -> A) -> (((A andd B) -> bot) -> bot) -> A andd B")
(assume "StabB" "StabA" "DNConj")
;; ...