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

Re: proving a property over finite_sets

Borzoo Bonakdarpour <borzoo@cse.msu.edu> wrote:
> I have been struggling to prove an easy-looking property of the following
> specification:
>   state: TYPE
>   f: finite_set[[state, state]]
>   s0, s1: VAR state
>   X: finite_set[state]
>   set1(rs: finite_set[state]): finite_set[state] =
>     {s0 |  EXISTS (s1): (member(s1, rs) AND member((s0, s1), f))}
>   func (fpSet: finite_set[state]) : RECURSIVE finite_set[state] =
>       LET rs = set1(fpSet) IN
>         IF nonempty?(rs) THEN
> 		func (union(rs, fpSet))
> 		fpSet
>        	ENDIF
>   MEASURE card(complement(fpSet))
>   prop: LEMMA FORALL(s0, s1): (member((s0, s1), f) AND member(s1,
> func(X))) IMPLIES member(s0, func(X))
> I tried induction schemes on finite_Sets and mucalculs without any
> success.  I appreciate if your share your thoughts on how to prove this
> with me.

Your specification has a couple of problems.  First, the measure for
your recursive function is over "complement(fpSet)".  But since the type
"state" is not known to be finite, "complement(fpSet)" may be infinite,
making the "card" function inapplicable.  If you meant the state type to
be finite, you'll have to say so; if not, then you need to rethink the
definition of "func".

Second, you cannot prove the termination property of "func" as stated.
Here is a counterexample:

state = { s0, s1 }
f = { (s0, s1), (s1, s0) }

Now func({s0, s1}) will never terminate, since rs is nonempty each time,
but rs = union(rs, fpSet).  If you mean for f to be a function, then
you'll have to say that.  Or perhaps you meant for the conditional to be
"IF nonempty?(difference(rs, fpSet))" instead?

Once you get those problems cleared up, I'll bet that you'll find it
easier to prove the result you want.  I'd start with an easier lemma,
something along these lines:

func_monotonic: LEMMA
  FORALL (A: finite_set[state]), s0:
    member(s0, A) IMPLIES member(s0, func(A))

As for induction, how does your paper proof look?  What is it that you
are inducting over?

Jerry James
Assistant Professor
EECS Department
University of Kansas