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

[Jerome <jerome@xxxxxxxxxxxxxx>]

On Wed, May 14, 2008 at 09:18:56PM -0700, Jerome wrote:
>I've defined a generic binary operator over sets that I'm trying to
>prove things about. It's very similar to what's done in finite_sets
>sum and prod(uct), however, the actual operator is variable:
>
>example[R: TYPE, o: FUNCTION[R, R -> R]]: THEORY
>BEGIN
>  ASSUMING
>    comm:  ASSUMPTION commutative?(o)
>    assoc: ASSUMPTION associative?(o)
>  ENDASSUMING
>
>  IMPORTING finite_sets@finite_sets_inductions[posnat]
>
>  myset:   TYPE = ARRAY[posnat -> R]
>  indices: TYPE = non_empty_finite_set[posnat]
>
>  curry(s: myset, K: indices): RECURSIVE R =
>    IF singleton?(K) THEN s(the(K))
>    ELSE s(choose(K)) o curry(s, rest(K))
>    ENDIF
>  MEASURE card(K)
>
>  curry_add: LEMMA
>    FORALL (s: myset, K: indices, k: posnat):
>      NOT member(k, K) IMPLIES curry(s, add(k, K)) = s(k) o curry(s, K)
>END example
>

Does this subgoal look feasible to anyone?

  {-1}  curry(s!1, add(k!1, U!1)) = s!1(k!1) o curry(s!1, U!1)
  [-2]  member(choose(add(e!1, add(k!1, U!1))), add(k!1, U!1))
  [-3]  member(choose(add(e!1, add(k!1, U!1))), add(e!1, U!1))
  [-4]  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(e!1, add(k!1, U!1)))
  [4]   s!1(choose(add(e!1, add(k!1, U!1)))) o
	 curry(s!1, rest(add(e!1, add(k!1, U!1))))
	 = s!1(k!1) o (s!1(e!1) o curry(s!1, U!1))

I can't quite figure out if there's something I can do with this, or
whether or not I've made a mistake earlier in the proof. Thanks

jerome