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

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

;; The disjunction is written "ord"
(pp (pf "A ord B"))

;; A disjunction can be 'eliminated' to distinguish cases
(set-goal "A ord B -> (bot -> B) -> (A -> bot) -> B")
(assume "u" "EfQB" "v")
;; u:A ord B
;;   EfQB:bot -> B
;;   v:A -> bot
;; -----------------------------------------------------------------------------
;; ?_2:B
(elim "u")
;; We are presented with two new goals, namely
;; ?_4:B -> B
;; ?_3:A -> B
(assume "w")
(use "EfQB")
(use "v")
(use "w")
(use "Id")
;; (cdp)
;; (proof-to-expr-with-formulas)

;; A disjunction is introduced by providing proof of the left or right disjunct
(display-idpc "OrD")
;; OrD	with content of type ysum
;; 	InlOrD:	Pvar1 -> Pvar1 ord Pvar2
;; 	InrOrD:	Pvar2 -> Pvar1 ord Pvar2

;; The commands are "(intro 0)" and "(intro 1)"

(set-goal "A ord B")
;; ?_1:A ord B
(intro 0)
;; ok, goal 1 can be obtained from

;; -----------------------------------------------------------------------------
;; ?_2:A
(undo)
(intro 1)
;; ?_2:B

(set-goal "A ord B")
(intro 1)

;; The conjunction is written "andd"
(pp (pf "A andd B"))

;; A conjunction can be 'eliminated' to obtain the lft and rht
(set-goal "A andd B -> (A -> B -> C) -> C")
(assume "ConjHyp" "ImpHyp")
;; ConjHyp:A andd B
;;   ImpHyp:A -> B -> C
;; -----------------------------------------------------------------------------
;; ?_2:C
(elim "ConjHyp")
(use "ImpHyp")
;; (cdp)
;; (proof-to-expr-with-formulas)

;; A conjunction is introduced by providing proof of the left and right conjunct
(display-idpc "AndD")
;; AndD	with content of type yprod
;; 	InitAndD:	Pvar1 -> Pvar2 -> Pvar1 andd Pvar2

;; The commands is "(intro 0)"

(set-goal "A andd B")
;; ?_1:A andd B
(intro 0)
;; ok, goal 1 can be obtained from
;; ?_3:B