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

[PVS-Help] Non empty finite set induction



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

I've worked it out on paper, but unfortunately can't carry it over to
PVS. Most of my trouble comes from trying to reason about set
operations.

The idea is to induct on K: the base case being where K is singleton;
the inductive step where K has an additional (arbitrary) element. My
proof so far is as follows:

curry_add :  

  |-------
{1}   FORALL (s: myset, K: indices, k: posnat):
        NOT member(k, K) IMPLIES curry(s, add(k, K)) = s(k) o curry(s, K)

Rule? (INDUCT "K" :NAME "nonempty_finite_set_induct")
Using instance
  finite_sets@finite_sets_inductions[posnat].nonempty_finite_set_induct
Inducting on K on formula 1 using induction scheme nonempty_finite_set_induct,
this yields  2 subgoals: 
curry_add.1 :  

  |-------
{1}   FORALL (e: posnat):
        FORALL (s: myset, k: posnat):
          NOT member(k, singleton(e)) IMPLIES
           curry(s, add(k, singleton(e))) = s(k) o curry(s, singleton(e))

Rule? (SKOSIMP*)
Repeatedly Skolemizing and flattening,
this simplifies to: 
curry_add.1 :  

  |-------
{1}   member(k!1, singleton(e!1))
{2}   curry(s!1, add(k!1, singleton(e!1))) =
       s!1(k!1) o curry(s!1, singleton(e!1))

Rule? (EXPAND "curry" 2 1)
Expanding the definition of curry,
this simplifies to: 
curry_add.1 :  

  |-------
[1]   member(k!1, singleton(e!1))
{2}   IF singleton?(add(k!1, singleton(e!1)))
        THEN s!1(the(add(k!1, singleton(e!1))))
      ELSE s!1(choose(add(k!1, singleton(e!1)))) o
            curry(s!1, rest(add(k!1, singleton(e!1))))
      ENDIF
       = s!1(k!1) o curry(s!1, singleton(e!1))

Rule? (SMASH)
Repeatedly simplifying with BDDs, decision procedures, rewriting,
and if-lifting,
this yields  2 subgoals: 
curry_add.1.1 :  

{-1}  singleton?(add(k!1, singleton(e!1)))
  |-------
[1]   member(k!1, singleton(e!1))
{2}   s!1(the(add(k!1, singleton(e!1)))) =
       s!1(k!1) o curry(s!1, singleton(e!1))

Rule? (HIDE 2)
Hiding formulas:  2,
this simplifies to: 
curry_add.1.1 :  

[-1]  singleton?(add(k!1, singleton(e!1)))
  |-------
[1]   member(k!1, singleton(e!1))

Rule?

... And this is where is gets dicey for me. [-1] implying [1] seems
perfectly reasonable, but every attempt I've tried at proving it
hasn't worked out.

Any comments on that, my overall proof structure, or even the theory
itself are welcomed. Thanks.

jerome