library of simple finite set properties?

[David N. Jansen]

Dear all,

I would like to get proofs of a few simple lemmas about IsFiniteSet and Cardinality, properties like:

\A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => IsFiniteSet(S \union T)

\A S: IsFiniteSet(S) => Cardinality(S) \in Nat
\A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => Cardinality(S) <= Cardinality(T)
\A i, j \in Int: Cardinality(i .. j) = IF i > j THEN 0 ELSE j - i

I guess that someone has already proofs of these and similar properties and I don't need to redo them. I want to use them to prove correctness of an algorithm and don't want to reinvent mathematics; and while I am ok to leave some of such simple lemmas unproven, I still prefer having a proof if it already exists.

Can someone of you help me? Thank you.

Kind regards,
David N. Jansen.

[Hillel Wayne]

Yup, you can find the theorems at
https://github.com/tlaplus/v2-tlapm/tree/master/library

H

[Stephan Merz]

The modules containing theorems about operators defined in standard TLA+ modules come with the TLAPS distribution, typically in /usr/local/lib/tlaps. For example, the module FiniteSetTheorems contains proofs about finite sets and cardinalities (and FiniteSetTheorems_proofs contains the full proofs for these theorems in case you are curious).

Of course, it is very likely that there are useful theorems beyond those contained in the distribution, and we welcome any suggestions and contributions.

Regards,
Stephan

> --
> 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...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.