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

Re: help discharging a TCC



Mark Aronszajn wrote:
> 
> 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?
> 

That's not strictly necessary, but to simplify things a bit, you could 
introduce a name for your set, e.g.

(NAME-REPLACE "E" "{ x: T | EXISTS (n: nat): n < length(a) AND seq(a)(n)
= x }" 
   :hide? nil).

Then you could take N=length(a) and  
f = lambda (z: (E)): epsilon! (n: below(length(a))): z=seq(a)(n).

To show that f is injective, you need to use epsilon_ax and show

  (FORALL (z: (E)): seq(a)(f(z)) = z).


A simpler way to do the proof is to use lemmas from the finite
set library. In finite_sets@finite_sets_eq, there is:

  E : VAR finite_set[T1]
  U : VAR set[T2]

  surjection_from_finite_set : PROPOSITION
        (EXISTS (f : [(E) -> (U)]) : surjective?(f)) IMPLIES
is_finite(U)

The TCC can be proved using this lemma with 

  E = { n: nat | n < length(a) }
  U = { x: T | EXISTS (n: nat): n < length(a) AND seq(a)(n) = x }
  f = seq(a).

There's a lemma in finite_sets@finite_sets_nat that shows that E
is finite and seq(a) is easily shown to be surjective.

---
Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717