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

help discharging a TCC



I want to discharge a TCC generated by the following declaration:

   elements(a: finseq): finite_set[T] = {x: T | exists (n: nat):
       n < length(a) and seq(a)(n) = x}

The function, elements, takes a finite_sequence and returns the set of
components of the sequence.

The TCC generated requires me to show that for any finite sequence, the
set of its components is a finite set (required since I have
"finite_set[T]" as the range for the elements function):

elements_TCC1: OBLIGATION
   (FORALL (a: finseq[T]):
     is_finite[T]({x: T | EXISTS (n: nat): n < length(a) AND seq(a)(n) = x}));

If you apply (grind) right off you get a subgoal to show that there is an
injective function, f, on the component set of the sequence that maps its
elements of the naturals less than some N.  I've tried doing this by
supplying "length(a)" for the N and various functions for f, but have not
succeeded.

I need some help figuring out a way to prove this.  Anyone have some time
to give me some pointers?

Mark Aronszajn
Reusable Software Research Group
Department of Computer Science & Electrical Engineering
West Virginia University