[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Moving existential quantifiers out over universal quantifiers




Bruno,

I've made progress.  Thank you for your help.

I can't make FORWARD-CHAIN work, except as part of the proof of
the general equality theorem:

FORALL (P: [a -> [b -> boolean]]):
      (FORALL (x:a): EXISTS (y:b): P (x) (y)) IFF
      (EXISTS (z:[a -> b]): FORALL (x:a): P (x) (z (x)))

I can't make rewriting work with this theorem and installing as
auto-rewrite (I tried unconditional as well as conditional) I get:

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

The progress I've made is in writing the beginning of a strategy:


(let ((x (let* (
(n -3)
(f (args1 (formula (car (select-seq (s-forms *goal*) (list n))))))
(b (bindings f))
(e (expression f))
) (make-lambda-expr b (make-lambda-expr (bindings e) (expression e))))))
(use "CHOICE2[nat, [external, external]]" :subst ("P" x))
(prop)
)

(CHOICE2 is the IMPLIES version of the general equality theorem above).
(the antecedent number is currently hard-coded as -3).

This strategy has the desired effect, but I would like to automate its
finding of a suitable antecedent.  This either involves passing in the
relevant types to the strategy, or having the strategy pass the types
to the (USE "CHOICE2...") rule.

The former approach requires the parsing of string arguments to types;
I can't find any documentation on how to do this.  The latter (less
robust) approach requires the conversion of types to a string, for
which I can't find any documentation either.

Without giving any proprietary information, I can show you the
relevant proof dialogue:

Double_Buffer_Composition.2 :  

{-1}  Buffer_Q(s!1(0)`1)
{-2}  Buffer_Q(s!1(0)`2)
{-3}  FORALL (t: nat):
        EXISTS (ei, eo: external):
          (i!1(t) = Input(ei)) AND
           (oh!1(t) = Output(eo)) AND (Input(eo) = Output(ei)) AND Buffer_N(s!1(t)`1)(ei)(s!1(1 + t)`1) AND Buffer_N(s!1(t)`2)(eo)(s!1(1 + t)`2)
  |-------
{1}   EXISTS (x: [nat -> bound[T]]):
        (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := i!1(t), Output := x(t) #))(s(1 + t)))) AND
         (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := x(t), Output := oh!1(t) #))(s(1 + t))))

Rule? (let ((x (let* (
(n -3)
(f (args1 (formula (car (select-seq (s-forms *goal*) (list n))))))
(b (bindings f))
(e (expression f))
) (make-lambda-expr b (make-lambda-expr (bindings e) (expression e))))))
(use "CHOICE2[nat, [external, external]]" :subst ("P" x)))
Using lemma CHOICE2[nat, [external, external]],
this simplifies to: 
Double_Buffer_Composition.2 :  

{-1}  (FORALL (x: nat):
         EXISTS (y: [external, external]):
           (i!1(x) = Input(y`1)) AND
            (oh!1(x) = Output(y`2)) AND (Input(y`2) = Output(y`1)) AND Buffer_N(s!1(x)`1)(y`1)(s!1(1 + x)`1) AND Buffer_N(s!1(x)`2)(y`2)(s!1(1 + x)`2))
       IMPLIES
       (EXISTS (z: [nat -> [external, external]]):
          FORALL (x: nat):
            (i!1(x) = Input(z(x)`1)) AND
             (oh!1(x) = Output(z(x)`2)) AND
              (Input(z(x)`2) = Output(z(x)`1)) AND Buffer_N(s!1(x)`1)(z(x)`1)(s!1(1 + x)`1) AND Buffer_N(s!1(x)`2)(z(x)`2)(s!1(1 + x)`2))
[-2]  Buffer_Q(s!1(0)`1)
[-3]  Buffer_Q(s!1(0)`2)
[-4]  FORALL (t: nat):
        EXISTS (ei, eo: external):
          (i!1(t) = Input(ei)) AND
           (oh!1(t) = Output(eo)) AND (Input(eo) = Output(ei)) AND Buffer_N(s!1(t)`1)(ei)(s!1(1 + t)`1) AND Buffer_N(s!1(t)`2)(eo)(s!1(1 + t)`2)
  |-------
[1]   EXISTS (x: [nat -> bound[T]]):
        (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := i!1(t), Output := x(t) #))(s(1 + t)))) AND
         (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := x(t), Output := oh!1(t) #))(s(1 + t))))


At this point FORWARD_CHAIN -1 doesn't work, but PROP does!  This
might at something to do with the multiple existentially quantified
variables: ei and eo.

Rule? (forward-chain -1)
Could not find a matching forward-chaining antecedent
formula.

No change on: (FORWARD-CHAIN -1)


...


Rule? (prop)
Applying propositional simplification,
this simplifies to: 
Double_Buffer_Composition.2 :  

{-1}  EXISTS (z: [nat -> [external, external]]):
        FORALL (x: nat):
          (i!1(x) = Input(z(x)`1)) AND
           (oh!1(x) = Output(z(x)`2)) AND
            (Input(z(x)`2) = Output(z(x)`1)) AND Buffer_N(s!1(x)`1)(z(x)`1)(s!1(1 + x)`1) AND Buffer_N(s!1(x)`2)(z(x)`2)(s!1(1 + x)`2)
[-2]  Buffer_Q(s!1(0)`1)
[-3]  Buffer_Q(s!1(0)`2)
[-4]  FORALL (t: nat):
        EXISTS (ei, eo: external):
          (i!1(t) = Input(ei)) AND
           (oh!1(t) = Output(eo)) AND (Input(eo) = Output(ei)) AND Buffer_N(s!1(t)`1)(ei)(s!1(1 + t)`1) AND Buffer_N(s!1(t)`2)(eo)(s!1(1 + t)`2)
  |-------
[1]   EXISTS (x: [nat -> bound[T]]):
        (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := i!1(t), Output := x(t) #))(s(1 + t)))) AND
         (EXISTS (s: [nat -> internal]): Buffer_Q(s(0)) AND (FORALL (t: nat): Buffer_N(s(t))((# Input := x(t), Output := oh!1(t) #))(s(1 + t))))

So, to summarize I've automated the instantiation, but I still need to
eliminate antecedent numbers from the proof to make the proofs easily
maintainable.

It would be nice not to have to import multiple instantiations of the
choice theory, because every time a new type instantiation is
required, I need to quit the proof and edit the .pvs file.

It would be nice to construct the strategy to perform a case split on
type-instantiated version of CHOICE2, and then prove it.  However, I
can't see from the documentation how to construct the term for a case
split.

I'm waiting on your suggestion for using lemma forall_and until I
attack more complex examples.

    Paul.

   Sender: bruno@csl.sri.com
   Date: Fri, 01 Oct 1999 10:30:30 -0700
   From: Bruno Dutertre <bruno@sdl.sri.com>
   X-Accept-Language: en
   CC: pvs-help@csl.sri.com
   Content-Type: text/plain; charset=us-ascii
   Content-Length: 1550

   Paul Loewenstein wrote:
   > 
   > I have proofs that have antecedent formulas of the form:
   > 
   > FORALL (x: a): EXISTS (y: b): Formula (x, y)
   > 
   > which I need to convert to the form:
   > 
   > EXISTS (z: [a -> b]): FORALL (x: a): Formula (x, z (x))
   > 
   > so I can skolemize z without instantiating x.
   > 
   > I currently do this rather tediously by hand specialization of the lemma:
   > 
   >  FORALL (P: [a -> [b -> boolean]]):
   >       (FORALL (x:a): EXISTS (y:b): P (x) (y)) IMPLIES
   >       (EXISTS (z:[a -> b]): FORALL (x:a): P (x) (z (x)))
   > 
   > which, somewhat to my surprise, turned out to be provable without
   > restricting a or b to be non-empty.
   > 

   (FORWARD-CHAIN ...) with this lemma is capable of instantiating P 
   automatically, at least in simple cases.

   You could use a stronger lemma as a rewrite rule:

     FORALL P: (FORALL x: EXISTS y P(x, y)) IFF (EXISTS z: FORALL x: P(x,
   z(x))).

   Rewriting with this lemma works better than forward-chaining with
   the other one.

   > I also need to apply eagerly the much simpler operation corresponding
   > to the theorem:
   > 
   > FORALL (P, Q: [a -> boolean]):
   >     (FORALL (x:a): P (a) AND Q (a)) IMPLIES
   >     (FORALL (x:a): P (a)) AND (FORALL (x:a): Q (a))
   > 
   > which would be my zeroth strategy to write.
   > 

   Rewriting also works here. The rewrite rule is already in the 
   prelude: lemma forall_and in theory quantifier_props.

   -- 
   Bruno Dutertre                             | bruno@sdl.sri.com
   SDL, SRI International                     | fax: 650 859-2844
   333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717