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

help on finite sequences




Hello,

I am trying to prove a property about a finite_sequence that I build
recursively:

filter(fs: finite_sequence[T], k: below[fs`length], p: pred[T]):
RECURSIVE finite_sequence =
 IF k = fs`length - 1 THEN
  IF p(fs`seq(k)) THEN
   (# length := 1,
      seq := LAMBDA(n: below[1]): fs`seq(k) #)
  ELSE
   empty_seq[T]
  ENDIF
 ELSE
  IF p(fs`seq(k)) THEN
   o((# length := 1,
        seq := LAMBDA(n: below[1]): fs`seq(k) #),
     filter(fs, k+1, p)
  ELSE
   filter(fs, k+1, p)
  ENDIF
 ENDIF
 MEASURE fs`length - k;

 every_filter: LEMMA
  FORALL (fs: finite_sequence[T], p: pred[T]):
   LET filtered_sequence = filter(fs, 0, p) IN
    FORALL (i: below[filtered_sequence`length]):
     p(filtered_sequence`seq(i));

Essentially I am trying to say that every element of the sequence that is
built using filter(...) with predicate p satisfies the predicate p. This
looks really easy to prove except that I am unable to extract the ith
element of the filter(...) sequence, or the seq function that is being
built up. Ignoring the TCCS for the moment, does anyone have any ideas
about how to go about this proof?

Thanks for your help,

Venkatesh.