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

[Jerome <jerome@xxxxxxxxxxxxxx>]

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