; The content of this file is in the public domain.
; example usage with Chicken Scheme: csi -q -b a-small-logic.scm

; A proof system based on the section 4 ("A Small Logic") in
; "Logic as Algebra" by Paul Halmos and Steven Givant, 1998
; ( https://archive.org/details/logicasalgebra0000halm ).
; It preserves the additive properties of parity.

(load "define-opaque-0.2.scm")

(define get-at (lambda (pos sentence)
  (if (equal? pos 0)
    (car sentence)
    (get-at (- pos 1) (cdr sentence)))))

(define sub-at (lambda (pos phrase sentence)
  (if (equal? pos 0)
    (append phrase (cdr sentence))
    (cons (car sentence) (sub-at (- pos 1) phrase (cdr sentence))))))

(define-opaque theorem make-theorem (sentence) ('nil)
  (
    (refl (lambda (what)
      (if (or (equal? what 'even) (equal? what 'odd))
        (make-theorem (list what '= what))
        (error "Argument must be 'even or 'odd: " what))))
    (replace (lambda (pos lhs-what rhs-what)
      (let* ((that (get-at pos sentence)))
        (cond
          ((and (equal? that 'even)
                (or (and (equal? lhs-what 'odd) (equal? rhs-what 'odd))
                    (and (equal? lhs-what 'even) (equal? rhs-what 'even))))
            (make-theorem (sub-at pos (list lhs-what '+ rhs-what) sentence)))
          ((and (equal? that 'odd)
                (or (and (equal? lhs-what 'odd) (equal? rhs-what 'even))
                    (and (equal? lhs-what 'even) (equal? rhs-what 'odd))))
            (make-theorem (sub-at pos (list lhs-what '+ rhs-what) sentence)))
          (else
            (error "Cannot replace: " that 'with lhs-what '+ rhs-what))))))
    (repr (lambda ()
      sentence))
  )
)

(define demo (lambda ()
  (let* (
    (thm0 (theorem 'refl 'odd))
    (thm1 (thm0 'replace 0 'odd 'even))
    ;(thm2 (thm1 'replace 2 'odd 'even))  ; this will error!
    (thm2 (thm1 'replace 2 'odd 'odd))
  )
    (display (thm0 'repr)) (newline)
    (display (thm1 'repr)) (newline)
    (display (thm2 'repr)) (newline)
  )))

(demo)