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.

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.

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

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

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 ?

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.

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

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...

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.

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.

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.

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 theSsreflectproof language

I will read the book.

The lemma you are looking for already exists in MathComp: https://github.com/math-comp/math-comp/blob/1c2d5a9b65e1331af6af75758a80e92967961595/mathcomp/fingroup/perm.v#L264

Last updated: Jun 13 2024 at 21:01 UTC