;;;PROOF-CHECK.SCM (REVISED October 21, 1998, from October 4, 1998 version)
;We assume, for convenience, that proofs are represented as a list of
;aeq's, STARTING with the aeq-theorem being proved.
(define (proof? p) ;P is assumed to be a Tree, i.e., it contains no nonlist pairs
(or (null? p) ;the empty proof which proves nothing.
(and (pair? p)
(let ((theorem (car p))
(rest-of-proof (cdr p)))
(and (proof? rest-of-proof)
(or (axiom? theorem)
(for-some?
(inference-rules)
(lambda (rule)
(inference-from? rule theorem rest-of-proof)))))))))
(define (axiom? aeq)
(for-some?
(axiom-patterns)
(lambda (axiom-pattern)
(match? axiom-pattern aeq))))
(define (inference-from? rule theorem aeqs)
(let ((n (number-of-antecedents rule)))
(cond
((= n 1)
(for-some? ;check one-antecedent inference rules
aeqs
(lambda (antecedent)
(match? rule `(,antecedent ,theorem)))))
((= n 2)
(for-some? ;check two-antecedent inference rules
aeqs
(lambda (antecedent1)
(for-some?
aeqs
(lambda (antecedent2)
(match? rule `(,antecedent1 ,antecedent2 ,theorem)))))))
(else (error "INFERENCE-FROM?: unknown rule" rule)))))
;NOTE: some obvious optimizations omitted above include checking
;(MATCH? (CONSEQUENT RULE) THEOREM)
;before the COND. Similarly, in the two antecedent
;case, check
;(MATCH? ANTECEDENT1 (CAR (ANTECEDENTS RULE)))
;before the inner FOR-SOME?
(define (number-of-antecedents rule)
(- (length rule) 1))
(define (axiom-patterns)
'((?e = ?e) ;reflexivity
(((?e + ?f) + ?g) = (?e + (?f + ?g))) ;+associativity
(((?e * ?f) * ?g) = (?e * (?f * ?g))) ;*associativity
((?e + ?f) = (?f + ?e)) ;+commutativity
((?e * ?f) = (?f * ?e)) ;*commutativity
((0 + ?e) = ?e) ;+identity
((?e + (- ?e)) = 0) ;+inverse
((1 * ?e) = ?e) ;*identity
((?e * (?f + ?g)) = ((?e * ?f) + (?e+ ?g))))) ;distributivity
(define (inference-rules)
; ;ONE-ANTECEDENT-RULES:
'(((?e = ?f) (? f = ?e)) ;symmetry
((?e = ?f) ((- ?e) = (- ?f))) ;-congruence
; ;TWO-ANTECEDENT-RULES:
((?e = ?f) (?f = ?g) (?e = ?g)) ;transitivity
((?e0 = ?e1) (?f0 = ?f1) ((?e0 + ?f0) = (?e1 + ?f1))) ;+congruence
((?e0 = ?e1) (?f0 = ?f1) ((?e0 * ?f0) = (?e1 * ?f1))))) ;*congruence
(define (for-some? ls pred)
(and (pair? ls)
(or (pred (car ls))
(for-some? (cdr ls) pred))))
;;TESTS
(load "match.scm")
(define sample-prf
'( (((f + g) + (- g)) = f)
(((f + g) + (- g)) = (0 + f))
(((f + g) + (- g)) = (f + (g + (- g))))
((f + (g + (- g))) = (0 + f))
((f + 0) = (0 + f))
((f + (g + (- g))) = (f + 0))
(f = f)
((g + (- g)) = 0)
((0 + f) = f) ))
;(proof? sample-prf)
;;Value: #t
;EXERCISE 1: Modify the above procedures to define a procedure ANNOTATE such
;that, like PROOF?, (ANNOTATE PRF) returns #f when PRF is not an equational
;proof. However, if PRF is a proof then (ANNOTATE PRF) returns an
;annotated version of PRF. Here's an example:
;(ANNOTATE SAMPLE-PRF)
;;Value:((1 (((f + g) + (- g)) = f) (transitivity 2 9))
; (2 (((f + g) + (- g)) = (0 + f)) (transitivity 3 4))
; (3 (((f + g) + (- g)) = (f + (g + (- g)))) (+associativity))
; (4 ((f + (g + (- g))) = (0 + f)) (transitivity 6 5))
; (5 ((f + 0) = (0 + f)) (+commutativity))
; (6 ((f + (g + (- g))) = (f + 0)) (+congruence 7 8))
; (7 (f = f) (reflexivity))
; (8 ((g + (- g)) = 0) (+inverse))
; (9 ((0 + f) = f) (+identity)))
;Namely, in an annotated version of a proof each of the aeq's is
;consecutively numbered and is followed by a list consisting of the name of
;the rule by which the aeq is inferred and the numbers of the antecedents of
;used for the rule.
;EXERCISE 2: Suppose we allow an additional SUBSTITUTION inference rule
; f = g
; ---------------- (substitution)
; e[x:=f] = e[x:=g]
;Modify the code above so the PROOF? procedure will properly detect
;this larger class of proofs. HINT: This is straightforward using context
;patterns, providing there is only ONE occurrence of X in E, WHICH YOU MAY
;ASSUME. Handling the general case when E has many X's is not hard, but
;seems to require a recursive procedure which goes beyond a simple match.
;EXERCISE 3: Suppose we extend proofs with the INSTANTIATION rule
; f = g
; ---------------- (instantiation)
; f[x:=h] = g[x:=h]
;Modify the code above so the PROOF? procedure so will properly detect this
;larger class of proofs. Hint: One approach is to transform F and G into
;patterns in which the variable X is replaced by a qmark-variable.