;; 2024-10-23.  ueb02.scm

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

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

;; Disjunction and conjunction are written "ornc" and "andnc"
(pp (pf "A ornc B"))
(pp (pf "A andnc B"))

;; There are introduction axioms (2 for ornc and one for andnc),
;; and also an elimination axiom for each of these.

;; To prove a goal in disjunction form one uses (intro 0) or (intro 1)
;; depending on which side of the disjunction you want to prove.

;; To prove a goal in conjunction form one uses (intro 0).

;; To make use of a hypothesis in disjunction ar conjunction form
;; use (elim 'hypname').

;; Example

;; Note that andnc binds stronger than ornc, and both bind stronger
;; than implication ->

(set-goal "A andnc (B ornc C) -> A andnc B ornc A andnc C")
(assume "Conj")
(elim "Conj")
(assume "u" "Disj")
(elim "Disj")
;; 5,6
;; Case B
(assume "v")
(intro 0)
(intro 0)
(use "u")
(use "v")
;; 6
;; Case C
(assume "v")
(intro 1)
(intro 0)
(use "u")
(use "v")
;; Proof finished.

;; Instead of (intro 0) for a conjunctive goal it is better to use
;; split.  It generates the same proof, but is easier to understand.

(set-goal "A andnc (B ornc C) -> A andnc B ornc A andnc C")
(assume "Conj")
(elim "Conj")
(assume "u" "Disj")
(elim "Disj")
;; 5,6
;; Case B
(assume "v")
(intro 0)
(split)
(use "u")
(use "v")
;; 6
;; Case C
(assume "v")
(intro 1)
(split)
(use "u")
(use "v")
;; Proof finished.

;; Evaluationg (cdp) (for "check and display proof") returns a linear form
;; of the proof tree, with an indication which rule is used.

(cdp)