#|
Here is an implementation of the Fitch-style proof language that we talked about on Feb 13.  
Your homework covered the proof language for atomic propositions, conjunction, and implication.
This implementation covers all of the cases including disjunction, negation, true, and false.
The case for negation is the most interesting one that you haven't yet seen.  Study it.
|#
(include-book "data-structures/structures" :dir :system)
(defstructure true)
(defstructure false)
(defstructure imp hyp concl)
(defstructure conj left right)
(defstructure disj left right)
(defstructure neg prop)

;; Data definition for Propositions P:
;; P ::= (true) | (false) | (imp P P) | (conj P P) | (disj P P) | (neg P) | A
;; A ::= Symbol (except for t and nil)

;; prop? : Any -> Booleanp
;; Decide if the given value is a proposition.
(defun prop? (x)
  (cond ((true-p x) t)
        ((false-p x) t)
        ((imp-p x) (and (prop? (imp-hyp x)) (prop? (imp-concl x))))
        ((conj-p x) (and (prop? (conj-left x)) (prop? (conj-right x))))
        ((disj-p x) (and (prop? (disj-left x)) (prop? (disj-right x))))
        ((neg-p x) (prop? (neg-prop x)))
        ((symbolp x) (not (booleanp x))))) ;; t and nil are ineligible
"prop? test"
(not (prop? t))
(not (prop? nil))
(prop? 'A)
(prop? (imp (false) (conj (true) (disj (neg 'X) 'Y))))


;; Here is a little language for representing proofs
;; (similar to the Fitch system).
(defstructure true-I) ;; a proof of (true)
(defstructure contradict prop neg-prop) ;; proof of (false)
(defstructure assume hyp body) ;; proof of implication
(defstructure mp implication antecedent) ;; modus ponens
(defstructure conj-I left right) ;; introduce conjunction
(defstructure conj-E/left conjunction) ;; take left conjunct
(defstructure conj-E/right conjunction) ;; take right conjunct
(defstructure disj-I left right) ;; introduce disjunction
(defstructure disj-E disj use-left use-right) ;; eliminate disjunction (proof by cases)
(defstructure suppose-for-contradiction prop deduction-of-false) ;; prove (neg prop) by contradiction.

;; Data definition for Deductions D:
;; D ::= (true-I) | (contradict P D) 
;;     | (assume P D) | (mp D D) 
;;     | (conj-I D D) | (conj-E/left D) | (conj-E/right D)
;;     | (disj-I D D) | (disj-E D D D)
;;     | (suppose-for-contradiction P D)
;;     | P

;; deduction? : Any -> Boolean
;; Decide if a given value is a deduction according to the data defn above.
;; Does *not* check that a deduction represents a well-formed proof.
(defun deduction? (x)
  (cond ((true-I-p x) t)
        ((contradict-p x) (and (deduction? (contradict-prop x))
                               (deduction? (contradict-neg-prop x))))
        ((assume-p x) (and (prop? (assume-hyp x))
                           (deduction? (assume-body x))))
        ((mp-p x) (and (deduction? (mp-implication x))
                       (deduction? (mp-antecedent x))))
        ((conj-I-p x) (and (deduction? (conj-I-left x))
                           (deduction? (conj-I-right x))))
        ((conj-E/left-p x) (deduction? (conj-E/left-conjunction x)))
        ((conj-E/right-p x) (deduction? (conj-E/right-conjunction x)))
        ((disj-I-p x) (and (deduction? (disj-I-left x))
                           (deduction? (disj-I-right x))))
        ((disj-E-p x) (and (deduction? (disj-E-disj x))
                           (deduction? (disj-E-use-left x))
                           (deduction? (disj-E-use-right x))))
        ((suppose-for-contradiction-p x) 
         (and (prop? (suppose-for-contradiction-prop x))
              (deduction? (suppose-for-contradiction-deduction-of-false x))))
        ((prop? x) t)))
"deduction? test"
(deduction? 'A)
(deduction? (assume 'A 'B))
(not (deduction? t))
(not (deduction? nil))
(deduction? (assume 'A (conj-I (disj-E (disj 'B 'C) 
                                       (assume 'B 'D)
                                       (assume 'C 'D))
                               (conj-E/right (conj 'X 'Y)))))

;; d->p : Deduction -> Proposition
;; Convert a deduction to a proposition *without* checking 
;; that the deduction actually represents a well-formed proof
;; of that proposition.
(defun d->p (d)
  (cond 
    ((true-I-p d) (true))
    ((contradict-p d) (false))
    ((assume-p d)
     (imp (d->p (assume-hyp d)) (d->p (assume-body d))))
    ((mp-p d) (imp-concl (d->p (mp-implication d)))) ;; just assume it's there
    ((conj-I-p d) 
     (conj (d->p (conj-I-left d))
           (d->p (conj-I-right d))))
    ((conj-E/left-p d) 
     (conj-left (d->p (conj-E/left-conjunction d))))
    ((conj-E/right-p d) 
     (conj-right (d->p (conj-E/right-conjunction d))))
    ((disj-I-p d) (disj (d->p (disj-I-left d))
                        (d->p (disj-I-right d))))
    ((disj-E-p d) 
     ;; chose left arbitrarily.. use-right would be okay.
     (d->p (disj-E-use-left d)))
    ((suppose-for-contradiction-p d)
     (neg (suppose-for-contradiction-prop d)))
    ((prop? d) d)))
"d->p test"
(equal (d->p 'A) 'A)
(equal (d->p (assume 'A 'B)) (imp 'A 'B))
(equal (d->p (assume 'A (conj-I (disj-I 'B 'C) 'D)))
       (imp 'A (conj (disj 'B 'C) 'D)))

;; Define:
;; Context = List[Proposition]
;; Maybe[X] = (union X {nil})

;; check-proof&get-theorem : Context Deduction -> Maybe[Proposition]
;; Check that the deduction is a well-formed proof; if so, produce the
;; proposition it proves.  Produce nil otherwise.
;; (ctx accumulates the assumptions made during the course of the proof).
(defun check-proof&get-theorem (ctx d)
  (cond 
    ((true-I-p d) 
     ;; true always provable.
     (true))
    ((contradict-p d) 
     ;; prove (false) from p and (neg p)
     (let ((p (check-proof&get-theorem ctx (contradict-prop d)))
           (neg-p (check-proof&get-theorem ctx (contradict-neg-prop d))))
       (and (equal (neg p) neg-p) 
            (false))))
    ((assume-p d)
     ;; prove implication by assuming antecedent and deriving consequent.
     (let ((assumption (assume-hyp d))
           (body (assume-body d)))
       (let ((body-thm (check-proof&get-theorem (cons assumption ctx) body)))
         (and body-thm
              (imp assumption body-thm)))))
    ((mp-p d)
     ;; modus ponens
     (let ((imp-thm (check-proof&get-theorem ctx (mp-implication d)))
           (antecedent-thm (check-proof&get-theorem ctx (mp-antecedent d))))
       (and imp-thm antecedent-thm
            (imp-p imp-thm)
            (equal (imp-hyp imp-thm) antecedent-thm)
            (imp-concl imp-thm))))
    ((conj-I-p d)
     ;; prove (conj P Q) from proof of P and proof of Q
     (let ((left-thm (check-proof&get-theorem ctx (conj-I-left d)))
           (right-thm (check-proof&get-theorem ctx (conj-I-right d))))
       (and left-thm right-thm
            (conj left-thm right-thm))))
    ((conj-E/left-p d)
     ;; prove P from a proof of (conj P Q)
     (let ((conj-thm (check-proof&get-theorem ctx (conj-E/left-conjunction d))))
       (and (conj-p conj-thm)
            (conj-left conj-thm))))
    ((conj-E/right-p d)
     ;; prove Q from a proof of (conj P Q)
     (let ((conj-thm (check-proof&get-theorem ctx (conj-E/right-conjunction d))))
       (and (conj-p conj-thm)
            (conj-right conj-thm))))
    ((disj-I-p d)
     ;; prove (disj P Q) from either a proof of P or a proof of Q.
     ;;
     ;; This case is slightly ugly due to the use of d->p.  Remember that to
     ;; introduce a disjunction, only one of the constituent formulae need
     ;; to be proved.  So we try to prove both, and take the first one that
     ;; works out.  d->p is used to convert the other one.
     (let ((left (disj-I-left d))
           (right (disj-I-right d)))
       (let ((maybe-left-thm (check-proof&get-theorem ctx left))
             (maybe-right-thm (check-proof&get-theorem ctx right)))
         (or (and maybe-left-thm (disj maybe-left-thm (d->p right)))
             (and maybe-right-thm (disj (d->p left) maybe-right-thm))))))
    ((disj-E-p d)
     ;; Prove R from proofs of (disj P Q). (imp P R), and (imp Q R).
     ;; ("proof by cases")
     (let ((disj-thm (check-proof&get-theorem ctx (disj-E-disj d)))
           (left->ans-thm (check-proof&get-theorem ctx (disj-E-use-left d)))
           (right->ans-thm (check-proof&get-theorem ctx (disj-E-use-right d))))
       (and (disj-p disj-thm)
            (imp-p left->ans-thm)
            (imp-p right->ans-thm)
            (equal (disj-left disj-thm) (imp-hyp left->ans-thm))
            (equal (disj-right disj-thm) (imp-hyp right->ans-thm))
            (equal (imp-concl left->ans-thm) (imp-concl right->ans-thm))
            (imp-concl left->ans-thm))))
    ((suppose-for-contradiction-p d)
     ;; Prove (neg P) by contradiction.
     (let ((prop (suppose-for-contradiction-prop d)))
       (let ((false-thm (check-proof&get-theorem (cons prop ctx) (suppose-for-contradiction-deduction-of-false d))))
         (and (equal false-thm (false))
              (neg prop)))))
    ((prop? d) 
     ;; "Prove" d by checking that it's among the assumptions.
     (car (member-equal d ctx)))))

"simplify test"
(equal (check-proof&get-theorem '(A) 'A) 'A)
(equal (check-proof&get-theorem '() 'A) nil)
(equal (check-proof&get-theorem '() (assume (conj 'A (neg 'A))
                                            (contradict (conj-E/left (conj 'A (neg 'A)))
                                                        (conj-E/right (conj 'A (neg 'A))))))
       (imp (conj 'A (neg 'A)) (false)))
(equal (check-proof&get-theorem '() (suppose-for-contradiction (conj 'A (neg 'A))
                                                               (contradict (conj-E/left (conj 'A (neg 'A)))
                                                                           (conj-E/right (conj 'A (neg 'A))))))
       (neg (conj 'A (neg 'A))))

(equal (check-proof&get-theorem '() (assume 'A 'A)) (imp 'A 'A))
(equal (check-proof&get-theorem '() (assume 'A (assume 'B (conj-I 'A 'B))))
       (imp 'A (imp 'B (conj 'A 'B))))
(equal (check-proof&get-theorem '() (assume (conj 'A 'B)
                                            'A))
       nil) ;; not justified by a proof step!  must use conj-E/left.

(equal (check-proof&get-theorem '() (assume (conj 'A 'B)
                                            (conj-E/left (conj 'A 'B))))
       (imp (conj 'A 'B) 'A))

(equal (check-proof&get-theorem '() (assume 'A (disj-I 'A 'B)))
       (imp 'A (disj 'A 'B)))
(equal (check-proof&get-theorem '() (assume 'B (disj-I 'A 'B)))
       (imp 'B (disj 'A 'B)))

(equal (check-proof&get-theorem 
        '() 
        (assume (disj 'A 'B)
                (assume (imp 'A 'C)
                        (assume (imp 'B 'C)
                                (disj-E (disj 'A 'B)
                                        (imp 'A 'C)
                                        (imp 'B 'C))))))
       (imp (disj 'A 'B)
            (imp (imp 'A 'C)
                 (imp (imp 'B 'C)
                      'C))))

(equal (check-proof&get-theorem
        '()
        (assume (conj (disj 'A 'B)
                      (conj (imp 'A 'C)
                            (imp 'B 'C)))
                (disj-E (conj-E/left (conj (disj 'A 'B)
                                           (conj (imp 'A 'C)
                                                 (imp 'B 'C))))
                        (conj-E/left
                         (conj-E/right
                          (conj (disj 'A 'B)
                                (conj (imp 'A 'C)
                                      (imp 'B 'C)))))
                        (conj-E/right
                         (conj-E/right
                          (conj (disj 'A 'B)
                                (conj (imp 'A 'C)
                                      (imp 'B 'C))))))))
       (imp (conj (disj 'A 'B)
                  (conj (imp 'A 'C)
                        (imp 'B 'C)))
            'C))