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

[Jerome <jerome@xxxxxxxxxxxxxx>]

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