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

Re: proving a property over finite_sets




Hi,

Thanks for your reply.  Actually I didn't have the mentioned problems in
my original specification (such as defining "state" as a finite type and
...).  The main problem was using finite_sets induction schemes.  I
modified my finite_set based recursive function to another function which
is based on the number of steps that makes the final set and I proved all
my lemmas and theorem :)  It is much easier to deal with induction on
integers rather than finite-sets.  Here is what I did:

  func(i: nat): RECURSIVE finite_set[state] =

        IF i = 0 THEN
		init
	ELSE
		union(func(i-1), set1(func(i-1)))
	ENDIF

  MEASURE (LAMBDA (x: nat): x)

I was also able to prove that this definition is equal to the previous
using a couple of intermediate lemmas.

Thanks,
Borzoo


On Mon, 18 Aug 2003, Jerry James wrote:

> 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))
> > 	ELSE
> > 		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?
>
> Regards,
> --
> Jerry James
> Assistant Professor
> EECS Department
> University of Kansas
>