How can I write the proof in TLA for the number of permutations of n distinct elements ?

I am not looking for the complete implementation for the Coq Prover though. But to show how one can write a structured proof in TLA for teaching mathematics, rather

than for showing how to use Coq.

My proof is as follows

Let S = {a1,a2,...an}

First Choice c1 \in S

Cardinality(c1) = n

Second Choice

c2 \in S\{c1} (remove first choice c1)

Cardinality(c2) = n-1

Continued Choice ci \in S\{c1,c2,...,c{i-1}}

Cardinality(ci) = n-(i-1)

Final Choice cn \in S\{c1,c2,...,c{n-1}}

Cardinality(ci) = 1

Thus Cardinality(S) = n!

I define cardinality in the following way. Would this be the way to do it in TLA ?

Cardinality (S) = |S| == count (S)

I think your definition of cardinality is circular. How do you define count? How do you define | |?

How should it be done ? I need to state that |S| is the notation to mean cardinality of set S.

Notation is one thing, but it does not convey a definition. If you haven't thought seriously about how cardinality is defined mathematically, it's unlikely that you can complete this kind of proof according to modern standards, even disregarding the use of Coq. You might start with https://en.wikipedia.org/wiki/Cardinality

Cardinality as the number of elements in a set. Nothing exotic

I want to do something like page 24 and 25 in https://lamport.azurewebsites.net/pubs/proof.pdf

Cardinality is actually one of the most unexpectedly exotic fundamental notions in mathematics. It's surprisingly hard to define rigorously. Converting between TLA+ and Coq is not straightforward, because Coq is based on type theory whereas TLA+ is based on set theory; if you try to do the conversion, you'll end up doing as much work as what I posted earlier in my github repo. I don't think it's productive to think in those terms trying to relate Coq to your previous knowledge. If you want to learn Coq, learn type theory from scratch. Others have already recommend the mathcomp book which will get you started. For open intervals and real analysis specifically, there is the mathcomp analysis library.

How about

Cardinality(set) == (+ e \in DOMAIN set: IF set[e] THEN 1 ELSE 0)

I want to describe it in TLA, even though not too rigorous. Much better than doing nothing.

What is a good book on type theory that would help me ?

Ok, too many questions to answer at once. For your definition of cardinality, that's actually a better attempt than most. I'll rephrase your definition as $\operatorname{card}(S) := \sum_{i \in S} 1$. I think this does work, although then you have to define the summation symbol, which is about as much work as defining cardinality in the first place. And now you perhaps start to see the problem: your proof outline that you gave above doesn't reference summations at all, and it would have to reference summations at some point if you were to use this definition. I strongly suggest that you prove easier results such as $\operatorname{card}(A \times B) = \operatorname{card}(A) \cdot \operatorname{card}(B)$ before you try to tackle the permutations theorem.

For your TLA questions, sorry, this is a Coq discussion group, and I don't know TLA. Maybe someone else can help. I do know that TLA is based on set theory which is not directly compatible with type theory.

For book recommendations, several have already suggested https://math-comp.github.io/mcb/

My hope was that some could have also delved in TLA. Yes. but that book is not about Type Theory.

Actually, type theory itself is largely irrelevant if you want to learn how to prove things using type theory. Analogy: English is a Germanic language, but if you want to learn English, the correct strategy is to look for resources on the English language, not resources on Germanic languages in general.

Similarly, yes, Coq is based on type theory, but if you want to learn how to use Coq, you should look for resources targeted at Coq, not at type theory in general. You'll learn what you need of type theory as you go along.

I remind you about your actual comment " If you want to learn Coq, learn type theory from scratch." !!!

Yes, I will now clarify. Learn it from scratch as part of learning Coq, not by itself.

You can put those knowing Coq well in a room. It is not encouraging to use.

Certainly it is not easy to use, but that is because the math itself is hard, not because of any fault of Coq. Defining cardinality really is bloody hard.

I don't understand most of what you said but I was taught that if cardinality is a natural number then set A has cardinality n if there is a bijection from A to fin n, where fin n is the set of all natural numbers less than n. This is a way to define cardinality in Coq

If cardinality is something like aleph then it's more complicated

Generally speaking formal verification is different from normal math because it is much more rigorous. You pretty much have to accept that your mental model in normal math might not translate very well into formal verification. There are "proofs" in normal math that are not really proofs at all, they're just mnemonics for us to remember a fact. An example is the stars and bars thing that counts the number of possible multisets

Quite right. I concur your definition of cardinality.

Last updated: Jun 23 2024 at 05:02 UTC