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

*To*: Venkatesh Phadnavis <vphadnav@eecs.ku.edu>*Subject*: Re: help on finite sequences*From*: Sam Owre <owre@csl.sri.com>*Date*: Fri, 17 Oct 2003 15:37:29 -0700*cc*: pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Sat, 11 Oct 2003 15:19:56 CDT." <20031011145847.N5516@tesla.eecs.ku.edu>*Sender*: pvs-help-owner@csl.sri.com

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. Regards, Sam

**References**:**help on finite sequences***From:*Venkatesh Phadnavis <vphadnav@eecs.ku.edu>

- Prev by Date:
**help on finite sequences** - Next by Date:
**Problem importing theories** - Prev by thread:
**help on finite sequences** - Next by thread:
**PVS/Cygwin** - Index(es):