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

Re: [tlaplus] library of simple finite set properties?

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


On 3/20/19 11:00 PM, David N. Jansen wrote:
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.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.