# Re: Instantiation hints

> 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

(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))))