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

*To*: Jerry James <loganjerry@xxxxxxxxx>*Subject*: Re: [PVS-Help] Non empty finite set induction*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Tue, 3 Jun 2008 07:51:24 -0700*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <870180fe0805291956i3a66c021hd6fbfba8ea77fb6b@mail.gmail.com>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20080515041856.GA2208@cs.caltech.edu> <20080522214701.GA16902@cs.caltech.edu> <20080530010928.GA28555@cs.caltech.edu> <870180fe0805291956i3a66c021hd6fbfba8ea77fb6b@mail.gmail.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

On Thu, May 29, 2008 at 08:56:18PM -0600, Jerry James wrote: >What do you think of the version I'm attaching here? I like >"doubleton". It makes more sense than "dualton". :-) I like the doubleton theory; doubleton_singleton is especially helpful. A little bit more is required, however, and I've been trying to figure out just what. Here are my thoughts: Before the doubleton theory, one of the open subgoals was as follows: curry_x.2.3 : {-1} singleton?(remove(choose(U!1), U!1)) [-2] U!1(k!1) |------- [1] empty?[index](U!1) [2] singleton?(U!1) {3} s!1(choose(U!1)) o curry(s!1, remove(choose(U!1), U!1)) = s!1(k!1) o curry(s!1, remove(k!1, U!1)) There are two plausible cases here: k!1 = choose(U!1) and k!1 /= choose(U!1). In the case of former, the proof is trivial; in the latter, doubleton_singleton can be used, but produces two subgoals: curry_x.2.3.2.1 : {-1} remove(k!1, U!1) = singleton(choose(U!1)) {-2} remove(choose(U!1), U!1) = singleton(k!1) [-3] singleton?(remove(choose(U!1), U!1)) [-4] U!1(k!1) |------- [1] choose(U!1) = k!1 [2] empty?[index](U!1) [3] singleton?(U!1) [4] s!1(choose(U!1)) o curry(s!1, remove(choose(U!1), U!1)) = s!1(k!1) o curry(s!1, remove(k!1, U!1)) curry_x.2.3.2.2 : [-1] singleton?(remove(choose(U!1), U!1)) [-2] U!1(k!1) |------- {1} U!1 = doubleton(k!1, choose(U!1)) [2] choose(U!1) = k!1 [3] empty?[index](U!1) [4] singleton?(U!1) [5] s!1(choose(U!1)) o curry(s!1, remove(choose(U!1), U!1)) = s!1(k!1) o curry(s!1, remove(k!1, U!1)) 2.3.2.1 goes easily with some help from commutivity and associativity; 2.3.2.2 on the other hand is more difficult. I don't think the other lemmas in your doubleton theory can handle this case, so I've added the following: singleton_doubleton: LEMMA FORALL S: doubleton?(S) IMPLIES FORALL t, u: member(t, S) AND member(u, S) AND t /= u IMPLIES S = doubleton(t, u) Do you agree that this is what we need? Unfortunately, I can't quite prove it. jerome

**References**:**[PVS-Help] Non empty finite set induction***From:*Jerome

**Re: [PVS-Help] Non empty finite set induction***From:*Jerome

**Re: [PVS-Help] Non empty finite set induction***From:*Jerome

**Re: [PVS-Help] Non empty finite set induction***From:*Jerry James

- Prev by Date:
**Re: [PVS-Help] Non empty finite set induction** - Next by Date:
**Re: [PVS-Help] Non empty finite set induction** - Previous by thread:
**Re: [PVS-Help] Non empty finite set induction** - Next by thread:
**[PVS-Help] Ask for help on a proof** - Index(es):