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

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