## 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?

## Interactive Theorem Proving

### Some Current Problems

• Hard, awkward interfaces and platforms (emacs).
• Not the most appealing to students, low coolness factor.
• Easy accessibility is crucial to learning; we learn to prove and program by imitation.

• Get the proofs out of their hole! Ubiquity.
• Long tradition in literate or "embedded" teaching books, but not runnable.
• Alternatives, like Edukera, non-free, non realistic.

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

• Write once, run anywhere, MOOCs.
• Decent math support.
• Excellent support for interactivity.

#### Coq

• Industrial-strength, mature theorem prover.
• Standard in the domain, many high-profile users.
• Extreme demand for experts.

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

• The DFT with MathBox (by Kevin Reid).
• DFT in Coq/MathComp.

## JsCoq Architecture

### Two Layers

• Providers: Editor widgets, textareas, pre/elements; they provide the next piece of code, invalidate old ones...
• Manager: Manages a set of providers that constitute a document.

### Modularity

• We expect to use the same framework for other kind of interactive programs, i.e.: Faust. or provers: Lean.

## Conclusions

• Still pretty much a technology demo, but quickly approaching to a usable state.
• Public alpha release soon, already gathered some interest and positive feedback from Coq community.
• Size/Time: 5 MiB (4 sec), Libs, 10 -- 100 MiB (< 20 secs)
• Works in progress: introduction to Coq, several interactive blog posts, DFT tutorial, Mini Faust tutorial, port of "Software Foundations".

Open source project at github.com/ejgallego/jscoq

/