Re: Instantiation hints

[Sam Owre <owre@csl.sri.com>]

> Date: Thu, 1 Feb 2001 08:33:10 +0200 (EET)
> From: Kellom{ki Pertti <pk@cs.tut.fi>
> To: pvs@csl.sri.com
> Subject: Instantiation hints
> 
> I have to prove a number of theorems of the form
> 
>   (exists(a,b,c,...) : P(a,b,c,...))  => (exists(a,b,c,...) : Q(a,b,c,...))
> 
> where P=>Q is trivial once I get rid of the quantifications. The order
> of the quantified variables may not be the same in the two
> quantifications, but they have the same variables.
> 
> Is there a way to tell PVS that it should instantiate "a" with "a!1",
> "b" with "b!1" etc.? 
> -- 
> Pertti

Hi Pertti,

I decided to start writing a strategy that does this, mostly to
illustrate how this could be done in PVS.

It isn't robust, in that it will choose randomly if there are a number
of skolem constants with the same prefix, e.g., a!1, a!2, ...  This is
because collect-skolem-constants gets the constants from a hash table.
A better heuristic would probably use the larger suffixes, as they are
the more recently introduced skolem constants.  In addition, this
strategy becomes a (SKIP) if any of the bound variable fail to match;
you might want to use "_" as the value instead, so that it will do a
partial instantiation instead - you could even put this on a flag.

There are undoubtedly other ways that this could be improved.  I'll let
you make these adjustments since you know what you actually need.

Regards,
Sam Owre

---------Add to ~/pvs-strategies----------

(defstep inst-by-skolem-names (fnum)
  (let ((sformnum (find-sform (s-forms (current-goal *ps*)) fnum
			      #'(lambda (sform)
				  (if (negation? (formula sform))
				      (check-inst-quant (args1 (formula sform))
							nil nil)
				      (check-inst-quant (formula sform)
							nil T)))))
	(newterms (get-corresponding-skolem-constants sformnum))
	(inst-cmd `(inst ,sformnum ,@newterms)))
    (if newterms
	inst-cmd
	(skip)))
  "Instantiates from available skolem constants with the 'same' name."
  "Instantiating from skolem constants")

;; Get the skolem constants corresponding to the bound variables in
;; formula sformnum
(defun get-corresponding-skolem-constants (sformnum)
  (let* ((sforms (select-seq (s-forms (current-goal *ps*)) (list sformnum)))
	 (sform (when sforms (car sforms)))
	 (fmla (when sforms (formula sform)))
	 (boundvars (when sforms 
		      (if (forall-expr? fmla)
			  (bindings (args1 fmla))
			  (bindings fmla)))))
    (find-matching-skolem-names boundvars)))

;; Find a set of skolem constants with names matching the boundvars
;; If any boundvar fails to be matched, return nil.
(defun find-matching-skolem-names (boundvars)
  (find-matching-skolem-names* boundvars (collect-skolem-constants) nil))

(defun find-matching-skolem-names* (boundvars skoconsts skolem-names)
  (if (null boundvars)
      (nreverse skolem-names)
      (let ((skoconst (find (id (car boundvars)) skoconsts
			    :test #'matching-skolem-id :key #'id)))
	(when skoconst
	  (find-matching-skolem-names*
	   (cdr boundvars) skoconsts
	   (cons (mk-name-expr (id skoconst)
		   nil nil (mk-resolution skoconst (current-theory-name)
					  (type skoconst)))
		 skolem-names))))))

(defun matching-skolem-id (bound-id skolem-id)
  (or (eq bound-id skolem-id)
      (eq bound-id (sko-symbol-prefix skolem-id))))