Re: [tlaplus] About Finite Set of records

[saksha...@xxxxxxxxxxxxxx]

Thanks Stephan! That's exactly what I'd written.

On Monday, March 27, 2017 at 10:44:13 AM UTC-4, Stephan Merz wrote:

Hi Saksham,

thanks for asking – here is your proof (I'm assuming that your module EXTENDs FiniteSetTheorems, included in the distribution of TLAPS).

LEMMA

  ASSUME NEW S, IsFiniteSet(S)

  PROVE  IsFiniteSet({s.f: s \in S})

<1>. DEFINE T == {s.f: s \in S}

            proj == [s \in S |-> s.f]

<1>. proj \in Surjection(S,T)  BY DEF Surjection

<1>. QED  BY FS_Surjection

Cheers,

Stephan

On 27 Mar 2017, at 16:32, saks...@xxxxxxxxxxxxxx wrote:

Hi gang,

Given a set S, of records where each record has a field f such that \A s \in S: s[f] \in Nat, I am trying to prove the following lemma:

    IsFiniteSet(S) => IsFiniteSet({s.f: s \in S})

As far as I could tell, there is no direct theorem in FiniteSetTheorems which can discharge this. There however are other ways. Some of them are:

    1) Prove that {s.f: s \in S} can be obtained from a surjection on S and then use FS_Surjection.
    2) Prove that \A s \in S : IsFiniteSet({s.f}) using FS_Singleton and then use FS_UNION to prove {{s.f}: s \in S} is finite. But I think here the above surjection would still be needed.
    3) Write an inductive proof on S.

I was wondering if others have tried to prove something along the lines of this before (collection of elements of finite sets of records), and how have others tried to prove it.

Thanks,
Saksham Chand

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.