Bringing Theorem Proving to the (sonic) Masses

Emilio J. Gallego Arias, Benoit Pin, Pierre Jouvelot

MINES ParisTech, PSL Research University, France

3 Novembre 2015 - CIEREC Saint-Etienne
Des outils et des méthodes innovantes pour l’enseignement de la musique et du traitement du signal

Theorem Proving
$\cap$
Signal Processing =
? Potential of Combining Topics?

JsCoq

Accessible Theorem Proving

Interactive Theorem Proving

Some Current Problems

"The Youtube Epoch"

Signal Processing:

Under-explored Area in ITP!
  • Provides interesting, small but not trivial examples.
  • Sound processing has high coolness factor.
  • Future of math proofs and exercises want to be computer checked.
  • "Experts" in DSP can really benefit from some education in ITP, but we need to lower the barrier to entry.
  • Formal considerations at the Faust design-level.

The Platform

HTML5

Coq

Coq: Some Facts

  • Functional programming language.
  • Provides very strong evindence, minimal kernel.
  • Programs are proofs types are specifications.
  • Strong automation.
  • Particularly well-suited for algebra, program verification.

A Typical Theorem:

$$ \mathsf{Thm1} : \mathsf{Hyp1} \to \ldots \to \mathsf{HypN} \to \mathsf{Concl} $$

Coq: An Example

"Alt-→": Coq's panel; "Alt-Enter" go to point; "Alt-N/P": Navigate.

Rewrite/Equality

$$ n + m = m + n $$

Another very important tool: big operators!

$$ \sum_i^N F(i) \qquad \ldots \qquad \prod_j^N F(j)$$ $$ \sum_{i = m + a}^{n-1} F(i) + \sum_{i = m}^{(n-a)-1)} F(i)$$

Demo I:
Discrete Fourier Transform

Demo II: Mini Faust

JsCoq Architecture


Two Layers

Modularity

Conclusions

Open source project at github.com/ejgallego/jscoq

/