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

*To*: pvs-help@xxxxxxxxxxx*Subject*: Re: [PVS-Help] Non empty finite set induction*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Fri, 16 May 2008 02:23:09 -0700*In-reply-to*: <870180fe0805152029p18dedf1es273a4a1d93658490@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> <870180fe0805151403y563a54b8k43b8d5db25fbfda@mail.gmail.com> <20080515232134.GA29387@cs.caltech.edu> <870180fe0805152029p18dedf1es273a4a1d93658490@mail.gmail.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

On Thu, May 15, 2008 at 09:29:03PM -0600, Jerry James wrote: >On Thu, May 15, 2008 at 5:21 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote: >> Another set-based subgoal I have is the following: >> >> [-1] member(choose(add(k!1, singleton(e!1))), singleton(e!1)) >> |------- >> [1] member(k!1, singleton(e!1)) >> [2] singleton?(add(k!1, singleton(e!1))) >> >> Again, seems straightforward, but figuring out which set_lemma's to >> use, and in what order, isn't so easy. Any ideas? Thanks > >That isn't straightforward, I'm afraid. Both [1] and [2] amount to >"k!1 = e!1", but it could be that k!1 /= e!1 and choose(add(k!1, >singleton(e!1)) just happens to be e!1. >-- Agreed. I initially hid one of the consequents (involving curry) as I thought the proof was about set membership. Bringing that consequent back in, however, allowed the proof to go through. My final challenge involves the inductive step: [-1] curry(s!1, add(e!1, U!1)) = s!1(e!1) o curry(s!1, U!1) |------- [1] U!1(e!1) [2] member(k!1, add(e!1, U!1)) [3] singleton?(add(k!1, add(e!1, U!1))) {4} s!1(choose(add(k!1, add(e!1, U!1)))) o curry(s!1, rest(add(k!1, add(e!1, U!1)))) = s!1(k!1) o (s!1(e!1) o curry(s!1, U!1)) Using "choose_add," I get two subgoals; it's the second one that I can't quite get my head around: {-1} member(choose(add(k!1, add(e!1, U!1))), add(e!1, U!1)) [-2] curry(s!1, add(e!1, U!1)) = s!1(e!1) o curry(s!1, U!1) |------- [1] U!1(e!1) [2] member(k!1, add(e!1, U!1)) [3] singleton?(add(k!1, add(e!1, U!1))) [4] s!1(choose(add(k!1, add(e!1, U!1)))) o curry(s!1, rest(add(k!1, add(e!1, U!1)))) = s!1(k!1) o (s!1(e!1) o curry(s!1, U!1)) In the first subgoal, I was able to get [4] to reduce to TRUE. I have the feeling that somewhere in this subgoal I need to get: ... [4] s!1(e!1) o (s!1(k!1) o curry(s!1, U!1)) = s!1(k!1) o (s!1(e!1) o curry(s!1, U!1)) and use associativity/commutivity to finish it off... or at least that's what my intuition says. Whether or not that's true, and how to actually do it, is where I could use some advice. Thanks. jerome

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

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

**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:
**[PVS-Help] Ask for help on a proof** - Previous by thread:
**Re: [PVS-Help] Non empty finite set induction** - Next by thread:
**Re: [PVS-Help] Non empty finite set induction** - Index(es):