Approximation Theory and Proof Assistants: Certified Computations

Master d'informatique fondamentale of École Normale Supérieure de Lyon, Fall-Winter 2024.

As of today, when it comes to perform numerical computations such as integrals, global optimization, etc. most scientists or engineers use well-known software like MATLAB or Maple, and numerical analysis-based routines that they offer. Though effective and correct most of the time, these results are returned with no guaranty at all on their quality (such as a certified error, say). This can be a real issue in various contexts where reliability and accuracy of computations are at stake. Examples include not only computational methods for hard mathematical problems appearing in nonlinear dynamics, but also practical critical systems such as control units of aircrafts or particle accelerators for instance.

In this course, we will present some aspects of the theory of polynomial approximation, we will introduce you with the Coq proof assistant and we will combine both subjects to address some examples of certified computations.

Informations Lecture notes and slides of the course Coq files Coq Cheat Sheet Evaluation M2 internship proposals References

Informations


Lecture notes and slides of the course

Draft version of NB's lecture notes.

Coq files


Evaluation


Coq Cheat Sheet

For an exhaustive list, see Coq documentation on tactics (you can look for a specific tactic there).

Basic tactics

intro H. intros HA HAB. intros H [H|H']. (introduce hypotheses, possibly decomposing them on the fly)
apply H. apply H, H'. apply (H H'). apply (te A). apply H in H'. (apply an hypothesis, a theorem, or a term)
assert(H: T). assert(H: T) by tac. have H: T. (prove a lemma inside a proof)
split. left. right. exists. (proving a conjunction, a discjunction, an exists)
destruct H as [H1 H2]. destruct H as [H1|H2].
  destruct H as [x Hx]. destruct (te A) as [HA HnA].
(decompose an hypothesis or a term)
contradict H. (close the goal by contradicting an hypothesis)
assumption. (close the goal by using one of the hypotheses)
reflexivity. (prove an equality by reflexivity)
rewrite H (plus_comm x). rewrite H in H'. rewrite -H. rewrite {2}H. (rewrite using an equality)
transitivity t (prove an equality by transitivity through t)
unfold f. rewrite /f. (unfold a definition)
induction n as [|m IH]. (proceeed by induction on n ( = destruct + induction hypothesis))
set x:=e. (give a name to a term or a pattern)
simpl. simpl in H. rewrite /=. (simplify the goal or an hypothesis by computation)
discriminate. discriminate H. (éliminer une égalité fausse)
injection H as [H']. (déduire des sous-égalités d'une égalité (injectivité des constructeurs))

High-level tactics

tauto. (solve a propositional tautology)
trivial. (try simple things such as assumption or reflexivity, leave the goal unchanged if it does not work)
easy. (try simple things such as assumption or reflexivity, fails if this does not solve the goal)
congruence. (theory of equality of uninterpreted symbols and constructors)
ring. (solve ring equations (polynomials))
ring_simplify. (expand/simplify polynomials)
field. (solve field equations)
field_simplify. (expand/simplify field expressions)
lia. (linear integer arithmetic - max, plus, minus, le, lt... but not mult)
lra. (linear real arithmetic - idem)

Tactic combinators

tac1; tac2. (apply tac2 to all subgoals generated by tac1)
repeat tac. (repeatedly apply tac)
now tac. (apply tac and conclude easily (e.g., with assumption))
try tac. (try to apply tac, not complaining if it fails---à consommer avec modération)

M2 internship proposals


References

Articles

Lecture notes

Books

More advanced level:

PhD theses

Softwares