## Methods for dealing with equality: setup, reduce, expand, combine
## Also a method called conclude for setting up proof goals and aiding
## in tracing proof executions, and two methods spec and spec-right
## for specialization of universally quantified theorems

############################################################################
## 

### DRM: my attempt to define this (needed by pos-substitute-equals)
(define (prop-pos-replace P pos v)
  (letrec ((prop-pos-replace-args 
	    (function (n rest args v)
		      (match args
			((list-of x rest-args) 
			 (check 
			  ((equal? n 1) (add (prop-pos-replace x rest v) rest-args))
			  (else (add x (prop-pos-replace-args (minus n 1) rest rest-args v)))))
			([] [])))))
    (match pos
      ([] v)
      ((list-of n rest)
       (match P
	 (((some-symbol f) (some-list args))
	  (make-term f (prop-pos-replace-args n rest args v))))))))

### DRM: There is a definition of cases in util.ath, but it uses 
### a call to an external prover.  This version avoids that heavy
### machinery (which might not be installed in all Athena distributions
### anyway).
(primitive-method (cases P1 P2)
  (match [P1 P2]
    ([(if _P _Q) (if (not _P) _Q)] (check ((& (holds? P1) (holds? P2)) _Q)))))

#Similarly with cd 
(primitive-method (cd P1 P2 P3)
  (match [P1 P2 P3]
    ([(or _P _Q) (if _P _R) (if _Q _R)] (check ((& (holds? P1) (holds? P2) (holds? P3)) _R)))))

#datatype-axioms is still under the old name, fix it here

(define datatype-axioms structure-axioms)

#############################################################
(define (three-cases case1 case2 case3)
  (dmatch [case1 case2 case3]
    ([(if P1 Q) (if P2 Q) (if (and (not P1) (not P2)) Q)]
     (dseq
      (!cases (if P1 Q) 
	      ((if (not P1) Q)
	       BY (assume (not P1)
		    (!cases (if P2 Q)
			    ((if (not P2) Q)
			     BY (assume (not P2)
				  (!mp (if (and (not P1) (not P2)) Q)
				       (!both (not P1) (not P2)))))))))))))
(define (~ t)
  (match t 
    (true false)
    (false true)))

# If a proposition of the form (and Q R), (or Q R), or (iff Q R) is in
# the assumption base, prove the same proposition with the arguments
# exchanged.  E.g.,
#   (assume (and A B) (!reorder (and A B)))
# proves (if (and A B) (and B A))

(define (reorder P)
  (dmatch P
    ((and Q R) 
     (!both (!right-and (and Q R))
	    (!left-and (and Q R))))
    ((or Q R)
     (!cd (or Q R)
	  (assume Q
	    (!either R Q))
	  (assume R
	    (!either R Q))))
    ((iff Q R)
     (!equiv 
      (assume R
	(!mp (!right-iff (iff Q R)) R))
      (assume Q
	(!mp (!left-iff (iff Q R)) Q))))))

## The following method takes two terms t1 and t2 where
## the equality (= t1 t2) is in the assumption base, and
## derives the theorem (= t2 t1).

## This method takes three terms t1, t2, and t3 such that
## t1 = t2 and t2 = t3 hold, and derives the equality t1 = t3.

## The method below takes a term t1, a theorem P, and a term t2,
## where the equality (= t1 t2) holds, and returns the proposition
## obtained from P by replacing every occurrence of t1 by t2.

(define (replace-term-in-term t1 t t2)
  (match t 
     ((val-of t1) t2)
     (((some-symbol f) (some-list args)) 
         (make-term f (map (function (t) (replace-term-in-term t1 t t2)) args)))
     (s s)))

(define (replace-term-in-prop t1 P t2)
  (match P
    ((some-atom t) (replace-term-in-term t1 t t2))
    ((not _Q) (not (replace-term-in-prop t1 _Q t2)))
    (((some-prop-con pc) P1 P2) (pc (replace-term-in-prop t1 P1 t2)
                                    (replace-term-in-prop t1 P2 t2)))
    (((some-quant quant) v B) (quant v (replace-term-in-prop t1 B t2)))))


(define (substitute-equals t1 P t2)
  (dlet ((fv (fresh-var))
         (newP (replace-term-in-prop t1 (rename P) fv))
         (biconditional (!leibniz t1 t2 newP fv)))
    (!mp (!left-iff biconditional) P)))

## The following is a more selective, positional version of
## substitute-equals. It takes a term t1, a theorem P, a position
## pos (represented as a list of numeric terms, say [2 1 4]) and
## a term t2, where the equality (= t1 t2) must hold. It returns
## the proposition obtained from P by replacing the occurrence of 
## t1 in P at position pos by t2. 

(define (pos-substitute-equals t1 P pos t2)
  (dlet ((t1=t2 $(= t1 t2))
         (v  (fresh-var [t1 t2 P]))
         (newP (prop-pos-replace P pos v))
         (biconditional (!leibniz t1 t2 newP v)))
    (!mp (!left-iff biconditional) P)))


## The method eq-congruence takes two terms t1 and t2, where
## the equality (= t1 t2) must hold, a term t, and a variable v
## and returns the equality (= t1' t2'), where t1' is obtained from
## t by replacing every occurrence of v by t1, and t2' is obtained
## from t by replacing every occurrence of v by t2.

(define eq-congruence
  (method (t1 t2 t v)
    (dlet ((t1=t2 $(= t1 t2))
           (v' (fresh-var))
           (newt (replace-var v v' t))
           (newt{t2/v'} (replace-var v' t2 newt))
           (prop (= newt newt{t2/v'}))
           (newt{t1/v'}=newt{t2/v'}<==>newt{t2/v'}=newt{t2/v'} (!leibniz t1 t2 prop v'))
           (newt{t2/v'}=newt{t2/v'}==>newt{t1/v'}=newt{t2/v'}
                (!right-iff newt{t1/v'}=newt{t2/v'}<==>newt{t2/v'}=newt{t2/v'}))
           (newt{t2/v'}=newt{t2/v'} (!eq-reflex newt{t2/v'})))
      (!mp newt{t2/v'}=newt{t2/v'}==>newt{t1/v'}=newt{t2/v'}
           newt{t2/v'}=newt{t2/v'}))))

## The following method, positional congruence, works with positions 
## instead of variables. It takes again two terms t1 and t2 such that
## (= t1 t2) is a theorem, a term t, and a position pos, and returns
## the equality (= t1' t2'), where t1' is obtained from t by replacing
## plugging t1 at position pos, and t2' is obtained from t by plugging
## t2 at position pos.

(define (pos-congruence t1 t2 t pos)
  (dlet ((v (fresh-var [t1 t2 t]))
         (newt (term-replace t pos v)))
    (!eq-congruence t1 t2 newt v)))

##==============================================================================
##                            FUNCTION CONGRUENCE 
##==============================================================================

## The method fun-cong below takes a function symbol f (of arbitrary arity), 
## and two lists of terms, s-terms = [s1 ... sn] and t-terms = [t1 ... tn],
## such that s_i = t_i is in the assumption base for every i = 1,...,n,
## and derives the equality f(s1,...sn) = f(t1,...,tn).  

(define (vars* terms)
  (match terms
    ([] [])
    ((list-of t rest) (join (vars t) (vars* rest)))))

(define (fun-cong f s-terms t-terms)
  (dletrec ((v (fresh-var (join (vars* s-terms) (vars* t-terms))))
            (do-args (method (first-s_i first-t_i rem-s_j rem-t_j eq)
                        (dmatch [rem-s_j rem-t_j]
                          ([[] []] (!claim eq))
                          ([(list-of s_j more-s_j) (list-of t_j more-t_j)]
                              (dlet ((F (= (make-term f s-terms)
                                           (make-term f (join first-t_i (join [v] more-s_j)))))
                                     (bi-cond (!leibniz s_j t_j F v))
                                     (new-eq (!mp (!left-iff bi-cond) eq)))
                                       (!do-args (join first-s_i [s_j]) 
                                                 (join first-t_i [t_j])
                                                 more-s_j more-t_j new-eq)))))))
     (!do-args [] [] s-terms t-terms (!eq-reflex (make-term f s-terms)))))
                                             

##==============================================================================
##                            RELATION CONGRUENCE 
##==============================================================================

## The method rel-cong below takes an atomic theorem P of the form (R s1 ... sn),
## the terms s-terms [s1...sn], and the terms t-terms [t1...tn], where si = ti 
## must be in the assumption base for all i, and returns the theorem (R t1 ... tn).

(define (rel-cong P s-terms t-terms)
  (dletrec ((do-args (method (s-terms t-terms theorem)
                       (dmatch [s-terms t-terms]
                         ([[] []] (!claim theorem))
                         ([(list-of s more-s) (list-of t more-t)]
                             (dlet ((new-theorem (!substitute-equals s theorem t)))
                               (!do-args more-s more-t new-theorem)))))))
     (!do-args s-terms t-terms P)))

## DRM: the above definition applies each substitution to the whole
## theorem P, which is incorrect (according to the comment preceding
## it).  The following is a modified version that uses
## pos-substitute-equals instead of substitute-equals, to restrict
## application of individual substitution to the corresponding
## argument position only.

(define (rel-cong P s-terms t-terms)
  (dletrec ((do-args (method (s-terms t-terms theorem n)
                       (dmatch [s-terms t-terms]
                         ([[] []] (!claim theorem))
                         ([(list-of s more-s) (list-of t more-t)]
			  (dlet ((new-theorem 
				  (!pos-substitute-equals s theorem [n] t)))
			    (!do-args more-s more-t new-theorem (plus n 1))))))))
    (!do-args s-terms t-terms P 1)))

## The argument list s-terms in the method rel-cong above is superfluous, since
## it can be extracted from the atomic theorem P. Hence rel-cong-2 below simply
## takes a theorem P, which again must be of the form (R s1 ... sn), and a list
## of terms t-terms [t1 ... tn], where si = ti must be in the asm. base, and 
## derives the theorem (R t1 ... tn)

(define (rel-cong-2 P t-terms)
  (dcheck ((atom? P) (!rel-cong P (children P) t-terms))))

##================================================================================
##                              RECURSIVE CONGRUENCE
##================================================================================

## This is a powerful recursive congruence method. If any
## subterms of t1 and t2 in corresponding positions are equal
## (with the equality in the assumption base), everything else 
## being the same, then the theorem (= t1 t2) is returned.

(define (rec-cong t1 t2)
    (dmatch (equal? t1 t2)
      (true (!equality (= t1 t1)))
      (_ (dmatch (fetch (function (P)  
                          (|| (equal? P (= t1 t2))
                              (equal? P (= t2 t1)))))
           (() (dlet ((root1 (root t1))
                      (root2 (root t2))
                      (args1 (children t1))
                      (args2 (children t2)))
                 (dmatch (equal? root1 root2)
                   (true (dletrec ((do-args 
                                     (method (s-terms t-terms) 
                                       (dmatch [s-terms t-terms]
                                         ([[] []] (!fun-cong root1 args1 args2))
                                         ([(list-of s1 more) (list-of t1 rest)] 
                                           (dseq 
                                             (!rec-cong s1 t1) 
                                             (!do-args more rest)))))))
                           (!do-args args1 args2))))))
           (P (dmatch P
                ((= (val-of t1) (val-of t2)) (!claim P))
                (_ (!sym (= t2 t1)))))))))
                      
## (assume (= ?x (+ 1 2)) (!rec-cong (* 7 ?x) (* 7 (+ 1 2))))

## This method takes two equational theorems eq1 and eq2, where eq1 is
## t=u and eq2 is v=u, and derives the equational theorem t=v.
## ****> Superceded by combine (which is used with reduce and expand)

(define combine-equations
  (method (eq1 eq2)
    (dmatch eq1
      ((= t11 t12)
       (dmatch eq2
	 ((= t21 t22)
	  (dcheck 
	   ((equal? t12 t22)
	    (dseq
	     (!sym (= t21 t22))
	     (!tran (= t11 t22) (= t22 t21)))))))))))

#################################################################################
##
## Rewriting methods: setup, reduce, expand, combine

(declare unary ((T) -> (T) T))

(declare --> (-> () Boolean))

(declare <-- (-> () Boolean))

(define (universal-quantifiers P)
  (match P
    ((forall _x _Q) (add _x (universal-quantifiers _Q)))
    (_ [])))

(define (universal-quantifierless P)
  (match P
    ((forall x _Q) (universal-quantifierless _Q))
    (_ P)))

(define (positions&subterms t k)
  (add [[] t] 
       (fold join (map 
		   (function (child)
			     (let ((n (cell 0))
				   (p&s (positions&subterms child n)))
			       (seq
				 (set! k (plus (ref k) 1))
				 (map 
				  (function (position&subterm)
					    (match position&subterm
					      ([position subterm]
					       [(add (ref k) position) subterm])))
				  p&s))))
		   (children t))
	     [])))

(define (attempt-rewrite current-equation new-term 
			 proposition position subterm direction)
    (dlet ((term0 
	    (match (universal-quantifierless proposition)
	      ((= lhs rhs) lhs)
	      ((if condition (= lhs rhs))
	       lhs)))
	   (subst (unify term0 subterm)))
      (dcheck 
       ((~ (equal? subst false))
	(dlet ((proposition1 
		(!uspec* proposition 
			 (subst (universal-quantifiers proposition))))
	       (result 
		(dmatch proposition1
		  ((= lhs rhs)
		   (dseq
		    (dmatch direction
		      (--> (!pos-substitute-equals 
			    lhs (ref current-equation) position rhs))
		      (<-- (dseq (!sym proposition1)
				   (!pos-substitute-equals 
				    rhs (ref current-equation) position lhs)))))
		   )
		  ((if condition (= lhs rhs))
		   (dseq
		    (dcheck ((holds? condition)
			     (!claim true))
			    (else (!claim false)))
		    (dmatch direction
		      (--> (dseq
			    (!mp proposition1 condition)
			    (!pos-substitute-equals 
			     lhs (ref current-equation) position rhs)))
		      (<-- (dseq 
			    (!sym (!mp proposition1 condition))
			    (!pos-substitute-equals 
			     rhs (ref current-equation) position lhs))))))))
	       (dummy (match result
			((= lhs rhs) 
			 (check ((equal? rhs new-term) 
				 true)))))
	       (dummy (set! current-equation result)))
	  (!claim result))))))

(define (try-all-terms current-equation new-term equation positions&subterms direction)
  (dmatch positions&subterms
    ((list-of [position subterm] more)
     (dtry (!attempt-rewrite current-equation new-term equation position subterm direction)
	   (!try-all-terms current-equation new-term equation more direction)))))

(define (rewrite current-equation new-term equation direction)
  (dlet ((old-term (match (ref current-equation)
			   ((= lhs rhs) rhs))))
    (dmatch direction
      (--> (!try-all-terms current-equation 
			   new-term 
			   (rename equation) 
			   (positions&subterms (unary old-term) (cell 1))
			   direction))
      (<-- (!try-all-terms current-equation
			   new-term
			   (rename equation)
			   (positions&subterms (unary new-term) (cell 1))
			   direction)))))

(define tracing-rewrites (cell false))

(define previous-equation (cell (cell true)))

(define level (cell 0))

(define (indent level)
  (check ((equal? level 0)
	  ())
	 (else (seq
		 (print "    ")
		 (indent (minus level 1))))))
	       
(define (rewrite current-equation new-term equation direction)
  (dlet ((old-term (match (ref current-equation)
		     ((= lhs rhs) rhs)))
	 (dummy (check ((ref tracing-rewrites)
			(check ((~ (equal? current-equation
					   (ref previous-equation)))
				(seq
				  (indent (plus (ref level) 1))
				  (print "Rewriting\n")
				  (indent (plus (ref level) 1))
				  (write-val old-term)
				  (print "\n")
				  ))
			       (else ())))
		       (else ())))
	 (result (dmatch direction
		   (--> (!try-all-terms current-equation 
					new-term 
					(rename equation) 
					(positions&subterms (unary old-term) (cell 1))
					direction))
		   (<-- (!try-all-terms current-equation
					new-term
					(rename equation)
					(positions&subterms (unary new-term) (cell 1))
					direction))))
	 (dummy 
	  (check ((ref tracing-rewrites)
		  (seq
		    (indent (plus (ref level) 1))
		    (check ((equal? current-equation
				    (ref previous-equation))
			    (print "-->\n"))
			   (else
			    (print "-->\n")))
		    (indent (plus (ref level) 1))
		    (write-val new-term)
		    (print "\n")
		    (set! previous-equation current-equation)))
		 (else ()))))
    (!claim result)))

(define (reduce current-equation new-term equation)
  (!rewrite current-equation new-term equation -->))

(define (expand current-equation new-term equation)
  (!rewrite current-equation new-term equation <--))

(define neither-left-nor-right (cell (cell true)))

(define (setup current-equation term)
  (dlet ((equation (!equality term term))
	 (dummy (seq
		  (set! current-equation equation)
		  (set! previous-equation neither-left-nor-right))))
    (!claim equation)))

(define left (cell true))

(define right (cell true))

(define (combine left right)
  (!combine-equations (ref left) (ref right)))

###########################################################################

(define (test-proof p)
  (dlet ((dummy (write p)))
    (!claim true)))

(define (test-proof p)
  (seq
    (write p)
    (print "Proved!")))

(define (spec proposition terms)
  (dlet ((spec-proposition (!uspec* proposition terms)))
    (dmatch spec-proposition
      ((if _P _Q)
       (!mp spec-proposition
	    _P))
      ((iff _P _Q)
       (!mp (!left-iff spec-proposition)
	    _P))
      (_ (!claim spec-proposition)))))

(define (spec-right proposition terms)
  (dlet ((spec-proposition (!uspec* proposition terms)))
    (dmatch spec-proposition
      ((iff _P _Q)
       (!mp (!right-iff spec-proposition)
	    _Q)))))

(define tracing (cell false))

(define (conclude prop)
  (seq
    (check ((ref tracing)
	    (seq
	      (set! level (plus (ref level) 1))
	      (indent (ref level))
	      (print "Proving at level ")
	      (write-val (ref level))
	      (print ":\n")
	      (indent (ref level))
	      (write-val prop)
	      (print "\n")))
	   (else ()))
    (method (proof)
      (dseq		
       (prop BY (!claim proof))
       (dlet ((dummy 
	       (check ((ref tracing)
		       (seq 
			 (indent (ref level))
			 (print "Done at level ")
			 (write-val (ref level))
			 (print "\n")
			 (set! level (minus (ref level) 1))))
		      (else ()))))
	 (!claim prop))))))

# To turn on tracing, enter
#   (set! tracing true)
# To turn it off, enter
#   (set! tracing false)

# To turn on tracing of rewrite rule applications
#   (set! tracing-rewrites true)
# To turn it off, enter
#   (set! tracing-rewrites false)

()