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

Re: help on finite sequences

Hi Venkatesh,

I tried to prove this directly, and found it to be very difficult.
The problem is that lemmas involving recursive definitions almost
always need induction, but it is difficult to give an induction for
this definition.

So I then tried to prove the same thing for lists:

  every_list_filter: LEMMA
   FORALL (ll: list[T], p: pred[T]):
    LET filtered_list = filter(ll, p) IN
     FORALL (i: below[length(filtered_list)]):
      p(nth(filtered_list, i))

This has a straightforward proof, included below.  The next thing I
did was to rewrite the definition as it would be for lists, and
provide some extra definitons and an induction scheme for
finite_sequences.  The proof then was essentially the same, as you
can see below.  I'll probably add all this to the prelude for the
next PVS release.