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

Re: Moving existential quantifiers out over universal quantifiers



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