Stream: Coq users

Topic: Proving the number of permutations for n distinct objects


view this post on Zulip Heime (Apr 25 2024 at 19:16):

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!

view this post on Zulip Heime (Apr 25 2024 at 21:34):

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

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

view this post on Zulip djao (Apr 25 2024 at 21:57):

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

view this post on Zulip Heime (Apr 25 2024 at 22:46):

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

view this post on Zulip djao (Apr 25 2024 at 23:00):

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

view this post on Zulip Heime (Apr 25 2024 at 23:05):

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

view this post on Zulip Heime (Apr 25 2024 at 23:08):

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

view this post on Zulip djao (Apr 25 2024 at 23:26):

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.

view this post on Zulip Heime (Apr 25 2024 at 23:49):

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

view this post on Zulip Heime (Apr 25 2024 at 23:51):

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

view this post on Zulip Heime (Apr 25 2024 at 23:52):

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

view this post on Zulip djao (Apr 25 2024 at 23:56):

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 card(S):=iS1\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 card(A×B)=card(A)card(B)\operatorname{card}(A \times B) = \operatorname{card}(A) \cdot \operatorname{card}(B) before you try to tackle the permutations theorem.

view this post on Zulip djao (Apr 25 2024 at 23:57):

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/

view this post on Zulip Heime (Apr 26 2024 at 00:01):

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

view this post on Zulip djao (Apr 26 2024 at 00:02):

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.

view this post on Zulip djao (Apr 26 2024 at 00:03):

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.

view this post on Zulip Heime (Apr 26 2024 at 00:05):

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

view this post on Zulip djao (Apr 26 2024 at 00:06):

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

view this post on Zulip Heime (Apr 26 2024 at 00:10):

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

view this post on Zulip djao (Apr 26 2024 at 00:11):

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.

view this post on Zulip Huỳnh Trần Khanh (Apr 26 2024 at 01:00):

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

view this post on Zulip Huỳnh Trần Khanh (Apr 26 2024 at 01:01):

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

view this post on Zulip Huỳnh Trần Khanh (Apr 26 2024 at 01:05):

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

view this post on Zulip Heime (Apr 26 2024 at 08:02):

Quite right. I concur your definition of cardinality.


Last updated: Jun 23 2024 at 05:02 UTC