Stream: Coq users

Topic: Using Coq for proving mathematical theorems in combinatorics


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Heime (Apr 25 2024 at 13:38):

I will read the book.

view this post on Zulip Kazuhiko Sakaguchi (Apr 25 2024 at 22:40):

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