minlog 4.0.99.20100221-5.2 / usr / share / minlog / lib / minpr_gen.scm

; $Id: minpr_gen.scm 2156 2008-01-25 13:25:12Z schimans $
; Proof of the minimum principle with measure function from induction

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

(set! COMMENT-FLAG #f)
(mload "../lib/nat.scm")
(set! COMMENT-FLAG #t)

; The minimum principle formula is generated through formula-to-min-pr-at
; parameters:
;  l-or-a-string, specifying if one wants to work within logic or arithmetic
;  n is the number of type variables
;  m is the number of predicates
; returns:
;  the minpr formula
; For m=n=1, the minimum principle, for some measure m, is:
;   ex i P(i) -> ex i. P(i) ! all j. m(j) < m(i) -> P(j) -> bot

; For the often appearing parameters, we define auxiliary functions
; k works as a counter

(define (fixed-vars-fun k n) 
; a function through which (alpha1)_((k-1)*n+1) ... (alphan)_((k-1)*n+n) 
; are generated, i.e. n fresh variables of types alpha1 to alphan
	  (do ((i (- n 1) (- i 1))
	       (res (list (make-var (make-tvar n DEFAULT-TVAR-NAME) 
				    (+ (* (- k 1) n) n) 1 ""))
		    (cons (make-var (make-tvar i DEFAULT-TVAR-NAME) 
				    (+ (* (- k 1) n) i) 1 "")
			  res)))
	      ((zero? i) res)))

(define (fixed-pvars-fun m n)
; a function through which m predicate vars are generated;
; each predicate takes n arguments of type alpha1 to alphan
  (let* (
	 (fixed-vars (fixed-vars-fun 1 n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (fixed-arity (apply make-arity fixed-tvars)))
    (do ((j (- m 1) (- j 1))
	 (res (list (make-pvar fixed-arity m h-deg-zero n-deg-zero ""))
	      (cons (make-pvar fixed-arity j h-deg-zero n-deg-zero "") res)))
	((zero? j) res))))
(define (measure-term-fun k n)
; a function returning the measure function m appearing in the min principle
; it has type alpha1=>...=>alphan=>nat and takes n parameters
; i.e. the k-th set of n fixed-vars
  (let* (
	 (fixed-vars (fixed-vars-fun k n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (measure-function-type
	  (apply mk-arrow (append fixed-tvars (list (make-alg "nat")))))
	 (measure-function-var (make-var measure-function-type -1 1 ""))
	 )
    (apply mk-term-in-app-form
	   (cons (make-term-in-var-form measure-function-var)
		 (map make-term-in-var-form fixed-vars)))))

(define (measure-function-var n)
; returns the type of the measure function, i.e. alpha1=>...=>alphan
  (let* (
	 (fixed-vars (fixed-vars-fun 1 n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (measure-function-type
	  (apply mk-arrow (append fixed-tvars (list (make-alg "nat"))))))
    (make-var measure-function-type -1 1 "")))


(define (formula-of-min-pr-at l-or-a-string n m)
; the function generating the min-pr formula
  (let* ((fixed-vars (fixed-vars-fun 1 n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (fixed-pvars (fixed-pvars-fun m n))
	 (fixed-varterms (map make-term-in-var-form fixed-vars))
	 (fixed-formulas (map (lambda (x)
				(apply make-predicate-formula
				       (cons x fixed-varterms)))
			      fixed-pvars))
	 (fixed-pvar (make-pvar (make-arity) -1 h-deg-zero n-deg-zero ""))
	 (fixed-formula (make-predicate-formula fixed-pvar))
	 (fixed-exc-kernel (apply mk-tensor fixed-formulas))
	 (fixed-exc-formula
	  (cond
	   ((string=? "l" l-or-a-string)
	    (apply mk-excl (append fixed-vars (list fixed-exc-kernel))))
	   ((string=? "a" l-or-a-string)
	    (apply mk-exca (append fixed-vars (list fixed-exc-kernel))))
	   (else (myerror "formula-of-min-pr-at: string l or a expected"
			  l-or-a-string))))
	 (measure-term (measure-term-fun 1 n))
	 (fixed-vars1 (fixed-vars-fun 2 n))
	 (fixed-varterms1 (map make-term-in-var-form fixed-vars1))
	 (measure-term1 (measure-term-fun 2 n))
	 (fixed-formulas1 (map (lambda (x)
				 (apply make-predicate-formula
					(cons x fixed-varterms1)))
			       fixed-pvars))
	 (fixed-all-formula
	  (apply mk-all
		 (append
		  fixed-vars1
		  (list (apply mk-imp
			       (cons (make-atomic-formula
				      (mk-term-in-app-form
				       (make-term-in-const-form
					(pconst-name-to-pconst "NatLt"))
				       measure-term1 measure-term))
				     (append
				      fixed-formulas1
				      (list (if (string=? "l" l-or-a-string)
						falsity-log falsity)))))))))
	 (fixed-extended-exc-kernel
	  (apply mk-tensor (cons fixed-all-formula fixed-formulas)))
	 (fixed-extended-exc-formula
	  (if (string=? "l" l-or-a-string)
	      (apply mk-excl
		     (append fixed-vars (list fixed-extended-exc-kernel)))
	      (apply mk-exca
		     (append fixed-vars (list fixed-extended-exc-kernel))))))
    (make-all (measure-function-var n)
	      (make-imp fixed-exc-formula fixed-extended-exc-formula))))
 

; In order to prove min-pr, we need the course-pf-values induction
; For the later, we need to construct the corresponding formula...

(define (formula-of-course-of-val-ind-at n m)
  (let* (
	 (fixed-vars (fixed-vars-fun 1 n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (fixed-pvars (fixed-pvars-fun m n))
	 (fixed-varterms (map make-term-in-var-form fixed-vars))
	 (fixed-formulas (map (lambda (x)
				(apply make-predicate-formula
				       (cons x fixed-varterms)))
			      fixed-pvars))
	 (fixed-pvar (make-pvar (make-arity) -1 h-deg-zero n-deg-zero ""))
	 (fixed-formula (make-predicate-formula fixed-pvar))
	 (fixed-all-kernel (apply mk-imp fixed-formulas))
	 (fixed-all-formula
	  (apply mk-all (append fixed-vars (list fixed-all-kernel))))
	 (measure-term (measure-term-fun 1 n))
	 (fixed-vars1 (fixed-vars-fun 2 n))
	 (fixed-varterms1 (map make-term-in-var-form fixed-vars1))
	 (measure-term1 (measure-term-fun 2 n))
	 (fixed-formulas1 
	  (map (lambda (x)
		 (apply make-predicate-formula
			(cons x fixed-varterms1)))
	       fixed-pvars))
	 (fixed-all-formula1
	  (apply mk-all
		 (append
		  fixed-vars1
		  (list (apply mk-imp
			       (cons (make-atomic-formula
				      (mk-term-in-app-form
				       (make-term-in-const-form
					(pconst-name-to-pconst "NatLt"))
				       measure-term1 measure-term))
				     fixed-formulas1
				     ))))))
	 (fixed-extended-all-kernel
	  (apply mk-imp (cons fixed-all-formula1 fixed-formulas)))
         (fixed-extended-all-formula
	  (apply mk-all
		 (append fixed-vars (list fixed-extended-all-kernel)))))
    (make-all (measure-function-var n)
	      (make-imp fixed-extended-all-formula fixed-all-formula ))))

; In the proof of course-of-values induction, we need to cut in
; an intermediate formula, which we construct bellow
(define (formula-cut n m)
  (let* (
	 (fixed-vars (fixed-vars-fun 1 n))
	 (fixed-tvars (map var-to-type fixed-vars))
	 (fixed-arity (apply make-arity fixed-tvars))
	 (fixed-varterms (map make-term-in-var-form fixed-vars))
	 (measure-term
	  (apply mk-term-in-app-form
		 (cons (make-term-in-var-form (measure-function-var n))
		       fixed-varterms)))
	 (fixed-pvars (fixed-pvars-fun m n))
	 (fixed-vars2 (fixed-vars-fun 2 n))
	 (fixed-varterms2 (map make-term-in-var-form fixed-vars2))
	 (measure-term2
	  (apply mk-term-in-app-form
		 (cons (make-term-in-var-form (measure-function-var n))
		       fixed-varterms2)))
	 (fixed-formulas2
	  (map (lambda (x)
		 (apply make-predicate-formula
			(cons x fixed-varterms2)))
	       fixed-pvars))
	 (natvar (make-var (make-alg "nat") -1 1 ""))
	 (tnatvar (make-term-in-var-form natvar))
	 (cut-formula-kernel
	  (apply mk-all
		 (append
		  fixed-vars2
		  (list (apply mk-imp
			       (cons (make-atomic-formula
				      (mk-term-in-app-form
				       (make-term-in-const-form
					(pconst-name-to-pconst "NatLt"))
				       measure-term2
				       tnatvar))
				     fixed-formulas2
				     ))))))
	  )
	  (apply mk-all
		 (append (list natvar) (list cut-formula-kernel)))
	  ))
	 


; We now prove the minimum principle, i.e. the result of formula-of-min-pr-at

; First, a function appending the elements from a list to a string
(define (str-app s l)
 (if (null? l) s (str-app (string-append s (car l)) (cdr l))))

(define (min-pr-to-thm-intern n m l-or-a-string) 
  (set! COMMENT-FLAG #f)
  (let* (
	 (fixed-vars (fixed-vars-fun 1 n))
	 (appvar (string-append (term-to-string (measure-term-fun 1 n)) "+1"))
	 (pred-form-to-args (str-app (pvar-to-string (car (reverse (fixed-pvars-fun m n)))) (map var-to-string fixed-vars)))
	 (pred-form-to-args-neg
	  (cond
	   ((string=? "l" l-or-a-string)
	    (string-append pred-form-to-args "->bot"))
	   ((string=? "a" l-or-a-string)
	    (string-append pred-form-to-args "->F")))) 
	 (CvInd
	  (string-append
	   "CvInd-" l-or-a-string "-" (number-to-string n) "-" (number-to-string m))))
          ; this is just to make sure we prove and save a new CvInd 
    ; proving
    (set-goal (formula-of-course-of-val-ind-at n m))
    (assume (var-to-string (measure-function-var n)) "H1")

    ; We need an auxiliary claim to get the induction through
    (cut (pf (formula-to-string (formula-cut n m))))
    
    (assume "H2") 
    (map assume (map var-to-string fixed-vars)) 
    ;(define appvar (string-append (term-to-string (measure-term-fun 1 n)) "+1"))
    (use "H2" (pt appvar))
    (use "Truth-Axiom")

    ; Now the proof of the generalized claim:
    (ind)

    ; Base
    (map assume (map var-to-string fixed-vars)) 
    (assume "Absurd")
    (use "Efq")
    (use "Absurd")

    ; Step
    (assume "nat" "H2")
    (map assume (map var-to-string (fixed-vars-fun 2 n))) 
    (assume "H3")
    (use "H1")
    (map assume (map var-to-string (fixed-vars-fun 3 n))) 
    (assume "H4")
    (use "H2")
    (use "NatLtLeTrans" (pt (term-to-string (measure-term-fun 2 n))))
    (use "H4")
    (use "NatLtSuccToLe")
    (use "H3")
    (save CvInd) 


    ; Now we can get back to our main goal:
    ; proving the minimum principle

    (set-goal (formula-of-min-pr-at l-or-a-string n m)) 
    (assume (var-to-string (measure-function-var n))) 
    (assume "H1" "H2")
    (use "H1")
    
    (use-with
     (proof-substitute
      (make-proof-in-aconst-form (theorem-name-to-aconst CvInd))
      (make-subst-wrt
       pvar-cterm-equal?
       (predicate-form-to-predicate 
	(pf pred-form-to-args))
;    statt make-cterm
       (list 'cterm (map pv (map var-to-string (fixed-vars-fun 1 n))) 
	     (pf pred-form-to-args-neg))))
     (pt (var-to-string (measure-function-var n))) "?")
    (use "H2"))
)

 
; by the bellow function, we avoid the computation in case the theorem already exists
(define (min-pr-to-thm n m l-or-a-string)
  (let* (
	 (name_thm
	  (string-append
	   "Min-Pr-" l-or-a-string "-" (number-to-string n) "-" (number-to-string m)))
	 (info (assoc name_thm THEOREMS)))
    (cond ((not info) ; that is, if the theorem does not exist
	(min-pr-to-thm-intern n m l-or-a-string)
	(save name_thm)))
    (set! COMMENT-FLAG #t)
    name_thm))