coq_fft_proof

Proof that the FFT implements the DFT, written in Coq.

This proof was developed using Coq 8.10.1.

Usage

Compile the complex numbers library with:

coqc Complex.v

Then you can proceed to load the FFT.v into CoqIDE and step through it.