## Stream: Coq users

### Topic: Using Coq for proving mathematical theorems in combinatorics

#### Heime (Apr 24 2024 at 22:35):

I want to show that the number of permutations of n distinct objects in n!. How can I do this in Coq. Have not been able to prove anything yet and want to start with something simple and see how it can be done, as an example for me.

Looked at the list of books but not quite sure which one would be most useful is showing me how to prove some elementary mathematics theorems.

My task is to prove some theorems in signal processing, Fourier and Wavelet Transforms, e.g. linearity.

#### djao (Apr 24 2024 at 22:46):

I've actually proved this theorem, but not likely in a way that is useful to you, since I was motivated by the metamathematics of ZFC rather than signal processing. But in case you'd like to see it, it's here: https://github.com/davidjao/zfc-coq/blob/2ff354e1fb5b901159c9eda63f9e2ec8262c3438/combinatorics.v#L583

For what you want, some online searching yields https://blog.poisson.chat/posts/2022-05-27-formalizing-finite-sets.html which is not everything that you want but at least moves in the right direction.

#### Li-yao (Apr 24 2024 at 22:46):

An applied resource for formalizing math in theorem provers is the natural number game in Lean https://adam.math.hhu.de/#/g/leanprover-community/nng4

#### Li-yao (Apr 24 2024 at 22:48):

Perhaps surprisingly, bijective combinatorics is not a great starting point because you run immediately into very technical problems with representing sets in a way suitable to do combinatorics

#### Heime (Apr 24 2024 at 23:24):

What would be good topics for starting theorem proving in Coq ? Want to start with Coq rather than Lean at this moment. Is it difficult to prove Fourier Transform Linearity, or the Convolution and Correlation Theorem in Coq ?

#### Heime (Apr 25 2024 at 00:03):

djao Could you help me write a proof and forget signal processing for now ? Your code does a super amount of things for me to understand. Or perhaps some other simple theorem.

#### djao (Apr 25 2024 at 01:40):

Heime said:

djao Could you help me write a proof and forget signal processing for now ? Your code does a super amount of things for me to understand. Or perhaps some other simple theorem.

I have a video tutorial here that I made for one of my classes: https://www.youtube.com/watch?v=Npg3a3P_YME

The corresponding file to follow along is here: https://djao.math.uwaterloo.ca/pre.v

#### Huỳnh Trần Khanh (Apr 25 2024 at 03:29):

Li-yao said:

Perhaps surprisingly, bijective combinatorics is not a great starting point because you run immediately into very technical problems with representing sets in a way suitable to do combinatorics

Setoids? But I mean the problem only needs to be solved once and it's actually not very hard...

#### Huỳnh Trần Khanh (Apr 25 2024 at 09:55):

I guess I get it. It's definitely not a good starting point for a person completely new to interactive theorem proving, but it isn't something that requires a lot of expertise to do either.

#### Li-yao (Apr 25 2024 at 10:19):

Most combinatorics books will start with set theory basics, with union, intersection, powerset, which are not natural operations to have on types (at least in the type theories of our favorite theorem provers). You can come up with a coherent story but to untrained eyes it will look alien.

#### Heime (Apr 25 2024 at 10:42):

What is the easiest way to learn how to use Coq to prove some simple mathematics ? How is a good way to continue assuming that the task does not require a lot of expertise.

#### Théo Winterhalter (Apr 25 2024 at 12:43):

Perhaps you could learn with @Assia Mahboubi and @Enrico Tassi's book? https://math-comp.github.io/mcb/

beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language