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

Re: forall clause within a set-comprehension



Gernot Lepuschitz wrote:
> 
> Is it possible to prove this lemma:
> 
>   empty_dict: LEMMA {w: Word |
>                FORALL (l: Letter
>                        | member(l, ),
>                (w1: Word | member(w1, retrDictd(empty))):
>                  w = cons(l, w1)}
>            =emptyset[Word]
> 
> I tried to do a (expand "emptyset"),(apply-extensionality) which leads
> me to this state:
> 
> {-1}    FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter): empty))),
>       (w1: Word | member(w1, retrDictd(empty))):
>         x!1 = cons(l, w1)
>   |-------
> [1]    (({w: Word |
>           FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter):
> empty))),
>           (w1: Word | member(w1, retrDictd(empty))):
>             w = cons(l, w1)})
>            = ({x: Word | FALSE}))
> How can I deal with the FORALL clause within the set comprehension ??
> 

(apply-extensionality) already delt with it by introducing antecedent
{-1}.
Now you have to prove that formula -1 is false.

Formula [1] is simply kept  from the previous goal but it's probably not
useful 
anymore. It's usually better to use (apply-extensionality :hide? t)
rather than
(apply-extensionality). In your case, this would get rid of [1].

Without knowing the definition of retrDictd(empty) and dom(...) it's
hard to be
sure but it is not clear whether {-1} is false. You have to find a
letter l and 
a Word w1 such that 

	x!1 /= cons(l, w1) 
	member(l, dom(LAMBDA (l: Letter): empty))
	member(w1, retrDictd(empty)).

If one of retrDictd(empty) or dom(LAMBDA (l: letter): empty) is empty,
then you can't find such l and w1. In this case, formula -1 is true and 
lemma empty_dict is false.

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