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

*To*: pvs-help@csl.sri.com*Subject*: Re: Moving existential quantifiers out over universal quantifiers*From*: Paul Loewenstein <pnl@heavengate.eng.sun.com>*Date*: Fri, 1 Oct 1999 16:35:03 -0700 (PDT)*CC*: pvs-help@csl.sri.com*In-reply-to*: <37F4EFB6.9A6B7BC3@sdl.sri.com> (message from Bruno Dutertre onFri, 01 Oct 1999 10:30:30 -0700)*References*: <199909302207.PAA02125@heavengate.eng.sun.com> <37F4EFB6.9A6B7BC3@sdl.sri.com>

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

**References**:**Moving existential quantifiers out over universal quantifiers***From:*Paul Loewenstein <pnl@heavengate.eng.sun.com>

**Re: Moving existential quantifiers out over universal quantifiers***From:*Bruno Dutertre <bruno@sdl.sri.com>

- Prev by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Prev by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Index(es):