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