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

*To*: pvs-help@csl.sri.com*Subject*: Re: help discharging a TCC*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Wed, 09 Jun 1999 14:17:35 -0700*CC*: pvs-help@csl.sri.com*References*: <Pine.GSO.4.05.9906090925200.19319-100000@naur.csee.wvu.edu>*Sender*: bruno@csl.sri.com

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

**References**:**help discharging a TCC***From:*Mark Aronszajn <aronsz@csee.wvu.edu>

- Prev by Date:
**help discharging a TCC** - Next by Date:
**trigonometry** - Prev by thread:
**help discharging a TCC** - Next by thread:
**Q; list (additional information)** - Index(es):