I want to read a book about Coq that would help me construct proofs of theorems in signal processing, particularly Fourier and Wavelet Transforms.
Have seen https://coq.inria.fr/documentation but unsure which book would be most suitable.
5
-
$\begingroup$ That is a mighty specific subject for a book. I’d instead look for a Coq project which does that. There might one or there might be none. $\endgroup$– Jason RuteCommented Apr 24 at 21:59
-
$\begingroup$ How about simpler proofs in mathematics ? Is there any one of them that delves into proving actual mathematical theorems (e.g. series, combinatorics, ...). $\endgroup$– DjoserCommented Apr 24 at 22:05
-
$\begingroup$ I found some related resources regarding doing analysis in Coq: perso.crans.org/cohen/CoqWS2018.pdf $\endgroup$– ice1000 ♦Commented Apr 25 at 1:01
-
$\begingroup$ Why not look at some research papers on this topic? I think most books serve general purposes. Perhaps you may find these papers helpful: inria.hal.science/hal-01728828/file/CICM18.pdf css.csail.mit.edu/6.888/2015/papers/jrubin.pdf Nevertheless, formalizing the digital processing algorithms in Coq can be challenging since you have to take care of every single detail. Good luck! $\endgroup$– Hiroki ChenCommented Apr 25 at 1:13
-
2$\begingroup$ This is a stretch, but Mathematics in Lean covers a lot of mathematical topics in Lean (not Coq). $\endgroup$– Jason RuteCommented Apr 25 at 3:46
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
Unfortunately, Coq is maybe not your tool of choice.
Real analysis in Coq is still work in progress, and not much has been formalized yet. The state of the art, to the best of my knowledge, is MathComp-Analysis. It should already have most of the machinery required to define the Fourier and wavelet transforms, but you'd still have to first develop all the mathematical machinery yourself. If you have a good and rigorous grasp of all the relevant mathematics, you could have a go at it, but I don't expect it to be easy.
Lean is probably somewhat bit better in terms of classical analysis, but I'd expect not too much. I think maybe you should look into Isabelle too.
