Context {$d k : nat$}.

Hypothesis $Hd : 1 < d$.

Hypothesis $Hk : k \neq 0$.

Context {$vtx : [0..d] \to '\mathbb{R}^d$}.

Hypothesis $Hvtx : aff_indep_ms vtx$.

Lemma $Hface_unisolvence^2 : \forall \{i\} p, Pdk d k p \to$

($\forall$ (idk : [0..pbinom d k]), $Hface vtx i$ (node vtx idk) $\to$ $p$ (node vtx idk) = 0) $\leftrightarrow$

($\forall$ x, $Hface Hvtx i x \to p x = 0$).

Backwards implication is immediate. The proof of the forward one directly derives from
**unisolvence_inj_Hface**^2 established in Section 9.3, where the induction hypothesis is
fulfilled here by the full unisolvence result.

# 10 Conclusion and Perspectives

After an insight of the contributions, we describe some difficulties and design choices, before giving perspectives.

## 10.1 Contributions

After some mathematical background on Finite Elements, we have described our Rocq formalization on this topic. To the best of our knowledge, this is the first time a finite element has been fully formalized and instantiated by defining the Lagrange finite elements.

To give an idea, the contributions presented in this article amount to about a hundred files (more than half are for Algebra), more than 7,000 statements (such as lemmas, definitions, and canonical structures), for about 45 kloc of vanilla Rocq.

All this is free and available at

https://lipn.univ-paris13.fr/rocq-num-analysis/-/tree/2.0/,

as the Opam packages rocq-num-analysis-subset,<fnref n="20" /> rocq-num-analysis-algebra,<fnref n="21" /> and rocq-num-analysis-fem.<fnref n="22" /> The respective dependencies of these packages are shown in Figure 15. This development has led to a major reorganization of the previous coq-num-analysis package.

This formalization includes both generic and dedicated components. Among the generic components that could be reused for other projects, we find the finite families (a.k.a. vectors of a given size), affine spaces, substructures and restrictions of functions (that belong to the *rocq-num-analysis-subset* and *rocq-num-analysis-algebra* packages), but also multi-indices and multivariate polynomials of bounded degree. The dedicated components are the definition of what a finite element is with a precise *Record* including both values and requirements, and the instantiation of this record in the (popular) case of simplicial Lagrange finite elements.

<footnote n="20">²⁰https://rocq-prover.org/p/rocq-num-analysis-subset/2.0.0</footnote>

<footnote n="21">²¹https://rocq-prover.org/p/rocq-num-analysis-algebra/2.0.0</footnote>

<footnote n="22">²²https://rocq-prover.org/p/rocq-num-analysis-fem/2.0.0</footnote>
## 10.2 Difficulties

The main difficulties we encountered are of two types: either due to mathematics or to formalization. As far as mathematics are concerned, the proofs are mostly based on [22], but with adaptation. For instance, we decided to work with almost no tools of analysis, and to employ purely affine arguments, only based on barycenters, for almost all steps of the construction of the simplicial Lagrange FE, see Sections 2.1 and 5, and [8]. We nevertheless relied on derivation in order to establish the linear independence of monomials in the space of multivariate polynomials, see Section 8.2.1.

The most difficult mathematical proof is the unisolvence of the Lagrange FE (see Section 9). It relies on a complex double induction with a polynomial factorization on a face. The formalization nicely follows the mathematical proof, but it still requires many steps, the connections being explained in Section 9.3. Another difficult mathematical proof is the freedom of monomials $(X^\alpha)_{\alpha \in \mathcal{A}_k^d}$ (see Section 8.2.1). There exist several proof paths and we chose one with the greatest number of already formalized tools. So, based on the derivative of *Coquelicot*, we defined derivatives of multivariate polynomials at any order to derive $X^\alpha$ and proved that it is a linearly independent family.

Another kind of difficulty is that of formalization choices. Given a mathematical object, how can we define it in Rocq, so that it is usable and even user-friendly? An example is the multi-indices and more precisely the $\mathcal{A}_k^{d'}$'s (see Section 8.1.1), that can be sets, or lists, but we chose to make them finite families of the expected size and we proved an injectivity property. There are several ways to build them (with different orderings), and we chose what we called the grsymlex ordering, forcing the definition to fit this ordering. Contrary to mathematics, we made heavy use of the indexing of the multi-indices.

Another example is how to formally handle substructures. We have several subsets (such as polynomials, face hyperplanes) that preserve the algebraic structure of their support type. For instance, functions to $\mathbb{R}$ are a *ModuleSpace*, and so are polynomials. This subspace can be represented as a predicate $E \to \text{Prop}$ and the properties by an assumption. But from these, we can also define, with a dependent type, a set that can be instantiated as *ModuleSpace* itself. This is formalized and was used at one point (notably for unisolvence), but it proved less practical than handling subsets as additional parameters of, for instance, bijectivity, see Section 4.1.

A last example is the definition of affine spaces (see Section 4.3). This is a known geometric object (such as a hyperplane, shifted from the origin), but it ended up creating formalization hardships. The reason is that of canonical structures and the fact that there may be several paths to create such a structure. Consider the example of Figure 14 that describes the eight paths to build the fact that $\mathbb{R}^d$ is an instance of the *AffineSpace* structure. The mechanism of the canonical structures forces us to choose one of these paths (the blue one), but the path we need may be different depending on the proof at stake (e.g. a *ModuleSpace* instance). It is of course much worse in the case of $(\mathbb{R}^d)^{d+1}$ which is very common in our application (for the vertices of the geometrical element, i.e. $d+1$ affinely independent points in $\mathbb{R}^d$). For a given definition on an affine space, such as *barycenter* or the predicate *aff_indep*, we add
another definition with the suffix _ms equal to the preceding one, but typing only on
a module space. This means duplicating some code, but helps choose the canonical
structure path we need in several proofs.

<figure><img src="image_14.png" /><figcaption>**Fig. 14** Various ways to equip $\mathbb{R}^d$ with the affine space structure.</figcaption></figure>

Double-edged boxes denote actual instances of canonical structures in the Rocq system for $\mathbb{R}$, that is to say possible terminal points for the canonical structure search. Rectangular boxes denote the intent to equip a space (either $\mathbb{R}$ or $\mathbb{R}^d$) with an algebraic structure. Arrows correspond to generic canonical structures in our library, or in the Coquelicot library (when there is no link annotation). Names are abbreviated, Ring_AS actually means Ring_AffineSpace, an instance of AffineSpace, and fct_MS means fct_ModuleSpace, an instance of ModuleSpace. Then, the possibilities are all the paths from the wanted space and algebraic structure to a double-edged box.

For instance, there is only one way to equip $\mathbb{R}^d$ with the ring structure: by applying the fct_Ring canonical structure. $\mathbb{R}^d$ is then of type fct_Ring [0..d) R_Ring, which is an instance of Ring. This is automatic.

For the module space $\mathbb{R}^d$, there is a true diamond problem, with two distinct mathematical interpretations: either $\mathbb{R}^d$ is a module space over itself (Ring_ModuleSpace (fct_Ring [0..d) R_Ring)), or it is the regular module over $\mathbb{R}$ (fct_ModuleSpace [0..d) (Ring_ModuleSpace R_Ring)). But, there is also a third path, fct_ModuleSpace [0..d) R_ModuleSpace, which is the direct one, and is automatic.

Finally, for the affine space $\mathbb{R}^d$, there are eight distinct paths, the chosen one being the blue one. Again, the automatic path is the shortest one fct_AffineSpace [0..d) R_AffineSpace (blue arrows). But this path prevents us from seeing $\mathbb{R}^d$ as a ModuleSpace, preventing us from using some lemmas.

On top of all this complexity, affine spaces can also be mathematically equipped with a module space structure by choosing some origin and making it the zero vector. Fortunately, our proofs were not based on such construction, as it makes Rocq loop.

## 10.3 Design Choices

Now let us discuss our design choices. First, as explained in Section 3.4, we rely on several axioms, including classical logic. Given the mathematical proofs we want to formalize, this seems the best choice, as we want our statements to be similar to the mathematical ones. For instance, constructive analysis can lead to the statement $\neg\neg(\exists x \in \neg\neg P)$ instead of $\exists x \in P$, and that would not convince mathematicians of the
maturity of our tools. We therefore preferred more understandable statements using classical logic.

A weakness of our formalization is that there are not enough requirements for the geometric element *K* in the record type FE. It can be empty, or have an empty interior while this is usually forbidden in mathematics. Note that most of the constructed finite elements (in Sections 6 and 9) are suitable as the simplex *K* is built from affinely independent vertices. A solution would be to require that a nonempty ball is included in *K*, but another appealing solution would be to build *K* by a regular-enough function from reference vertices (be they simplex or cuboid reference vertices). In the record, the vertices would be replaced by the function and the rest of the record would be kept (unisolvency included) and most of this development would still apply, a notable exception being the geometric transformation of a FE of Section 7.4. This perspective would also allow us to deal with general hexahedra in 3D, whose faces are not necessarily planar and that are not convex in general. Such nonconvex geometric elements can be used for instance in metal forming [49].

<figure><img src="image_15.png" /><figcaption>**Fig. 15** Dependency graph, including the literature (in green), our contributions presented in this article (in yellow), and perspectives (in blue). Plain arrows are current dependencies between libraries, while dotted arrows are expected dependencies.</figcaption></figure>
## 10.4 Perspectives

A straightforward perspective is to consider cuboid finite elements and their properties. This will require to factorize part of our development between simplex and cuboid finite elements. Cuboid Lagrange finite elements are often defined as the tensorization of 1D Lagrange FE (i.e. taking $P_k^1$ for each variable). Their unisolvence proof would be simpler and by induction on the dimension only. What is more delicate is the fact that the geometric transformation is no longer affine in general, see [22, Sec. 13.5].

Another important and challenging perspective is to handle face or edge elements, i.e. finite elements of dimension $l$ that live in $\mathbb{R}^d$ with $l < d$ (typically $l = d-1$). They can be used to apply the boundary conditions of the PDE, but also for the treatment of fractures [50], or for the boundary finite element methods, see for instance [51] and references therein. These boundary elements do not fit in our formalization so far.

It would be also interesting to extend the record FE to finite elements whose approximation space $P_{approx}$ takes its value in $\mathbb{R}^q$, with $q \ge 1$ (often $q = 1$ or $q = d$). This is a necessary step for the construction of Raviart-Thomas flux FE [22, Chap. 14], that require a significant development of integral, differential calculus and geometry components (such as face integrals, normals, and non-affine geometric transforms).

More than other finite elements, we have several long-term perspectives described in Figure 15. We want to formally prove the finite element method, meaning the full algorithm to solve a PDE. As explained in Section 2.3, the PDE is solved on each finite element and glued together, the FEM guaranteeing the continuity of the computed solution. Therefore, we need to formalize Sobolev spaces (and prove they are Hilbert spaces).

The ultimate goal is to guarantee some (part of a) library implementing the finite element method, such as XLiFE++.<fnref n="23" /> It will be a different kind of proofs: more than proving the finite element method as a mathematical algorithm, it requires to prove it complies with the C++ program. A specific point out of the literature is to ensure that the floating-point errors do not mess too much with the results, relying on automatic provers or on the Flocq library [2].

## Acknowledgments

The authors thank Alexandre Ern, Guillaume Melquiond, and Pierre Rousselin for fruitful discussions about proof details, canonical structures, and notations. The authors are also thankful to David Hamelin for his help in tuning the CI and about the Nix package manager.

This work was partly supported by the European Research Council (ERC) under the European Union's Horizon 2020 Research and Innovation Programme – Grant Agreement n°810367.

## Bibliography

[1] Fernández, M.A., Gerbeau, J.-F., Martin, V.: Numerical simulation of blood flows

<footnote n="23">²³https://xlifepp.pages.math.cnrs.fr/</footnote>
through a porous interface. M2AN Math. Model. Numer. Anal. **42**(6), 961–990
(2008) https://doi.org/10.1051/m2an:2008031

[2] Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: Proc. of the IEEE 20th Symposium on Computer Arithmetic (ARITH 2020), pp. 243–252. IEEE, Los Alamitos (2011). https://doi.org/10.1109/ARITH.2011.40

[3] Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. **50**(4), 423–456 (2013) https://doi.org/10.1007/s10817-012-9255-4

[4] Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax–Milgram theorem. In: Proc. of the 6th ACM SIGPLAN Internat. Conf. on Certified Programs and Proofs (CPP 2017), pp. 79–89. Association for Computing Machinery, New York (2017). https://doi.org/10.1145/3018610.3018625

[5] Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formalization of Lebesgue integration of nonnegative functions. J. Autom. Reason. **66**(2), 175–213 (2022) https://doi.org/10.1007/s10817-021-09612-0

[6] Boldo, S., Clément, F., Martin, V., Mayero, M., Mouhcine, H.: A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Proc. of the 25th Internat. Symp. on Formal Methods (FM 2023). LNCS, vol. 14000, pp. 39–55. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_4

[7] Boldo, S., Clément, F., Leclerc, L.: A Coq formalization of the Bochner integral. Research Report RR-9547, Inria (2022). https://inria.hal.science/hal-03516749/

[8] Clément, F., Martin, V.: Finite element method. Detailed proofs to be formalized in Coq. Research Report RR-9557, Inria (2024). Release 1.0 (v1). https://inria.hal.science/hal-04713897/

[9] de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Proc. of the 25th Internat. Conf. on Automated Deduction (CADE 2015). LNCS, vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26

[10] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin - Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

[11] Meikle, L., Fleuriot, J.: Automation for geometry in Isabelle/HOL. In: Schmidt, R.A., Schulz, S., Konev, B. (eds.) Proc. of the 2nd Workshop on Practical Aspects
of Automated Reasoning (PAAR 2010). EPiC Series in Computing, vol. 9, pp. 84–94. EasyChair, Bramhall, UK (2012). https://doi.org/10.29007/r5k7

[12] Dufourd, J.-F., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) Proc. of the 1st Internat. Conf. on Interactive Theorem Proving (ITP 2010), pp. 211–226. Springer, Berlin - Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_16

[13] Bertot, Y.: Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs. In: Fischer, B., Uustalu, T. (eds.) Proc. of the 15th Internat. Colloquium on Theoretical Aspects of Computing (ICTAC 2018), pp. 3–10. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02508-3_1

[14] Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: Beringer, L., Felty, A.P. (eds.) Proc. of the 3rd Internat. Conf. on Interactive Theorem Proving (ITP 2012). LNCS, vol. 7406, pp. 377–392. Springer, Berlin - Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_26

[15] Otsuki, S., Kawamoto, P.N., Yamazaki, H.: A simple example for linear partial differential equations and its solution using the method of separation of variables. Formaliz. Math. 27(1), 25–34 (2019) https://doi.org/10.2478/forma-2019-0003

[16] Deniz, E., Rashid, A., Hasan, O., Tahar, S.: On the formalization of the heat conduction problem in HOL. In: Buzzard, K., Kutsia, T. (eds.) Proc. of the 15th Internat. Conf. on Intelligent Computer Mathematics (CICM 2022). LNCS, vol. 13467, pp. 21–37. Springer, Cham (2022). https://doi.org/10.48550/arXiv.2208.06642

[17] Tekriwal, M., Duraisamy, K., Jeannin, J.-B.: A formal proof of the Lax equivalence theorem for finite difference schemes. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds.) Proc. of the 13th Internat. Symp. NASA Formal Methods (NFM 2021). LNCS, vol. 12673. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76384-8_20

[18] Ciarlet, P.G.: The Finite Element Method for Elliptic Problems. Classics in Applied Mathematics, vol. 40. Society for Industrial and Applied Mathematics (SIAM), Philadelphia (2002). https://doi.org/10.1137/1.9780898719208. Reprint of the 1978 original [North-Holland, Amsterdam]

[19] Babuška, I., Strouboulis, T.: The Finite Element Method and Its Reliability. Numerical Mathematics and Scientific Computation, p. 802. The Clarendon Press, Oxford University Press, New York (2001). https://doi.org/10.1093/oso/9780198502760.001.0001

[20] Quarteroni, A., Valli, A.: Numerical Approximation of Partial Differential Equations. Springer Series in Computational Mathematics, vol. 23. Springer,
Berlin - Heidelberg (1994). https://doi.org/10.1007/978-3-540-85268-1

[21] Ern, A., Guermond, J.-L.: Theory and Practice of Finite Elements. Applied Mathematical Sciences, vol. 159. Springer, New York (2004). https://doi.org/10.1007/978-1-4757-4355-5

[22] Ern, A., Guermond, J.-L.: Finite Elements I. Approximation and Interpolation. Texts in Applied Mathematics, vol. 72. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-56341-7

[23] Ern, A., Guermond, J.-L.: Finite Elements II. Galerkin Approximation, Elliptic and Mixed PDEs. Texts in Applied Mathematics, vol. 73. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-56923-5

[24] Ern, A., Guermond, J.-L.: Finite Elements III. First-Order and Time-Dependent PDEs. Texts in Applied Mathematics, vol. 74. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-57348-5

[25] Brenner, S.C., Scott, L.R.: The Mathematical Theory of Finite Element Methods, 3rd edn. Texts in Applied Mathematics, vol. 15. Springer, New York (2008). https://doi.org/10.1007/978-0-387-75934-0

[26] Zienkiewicz, O.C., Taylor, R.L., Zhu, J.Z.: The Finite Element Method: Its Basis and Fundamentals, 7th edn. Elsevier/Butterworth Heinemann, Amsterdam (2013). https://doi.org/10.1016/B978-1-85617-633-0.00001-0

[27] Ciarlet, P.G.: Basic error estimates for elliptic problems. In: Finite Element Methods (Part 1). Handbook of Numerical Analysis, vol. 2, pp. 17–351. Elsevier Science Publishers B.V., North-Holland (1991). https://doi.org/10.1016/S1570-8659(05)80039-0

[28] Wahlbin, L.B.: Local behavior in finite element methods. In: Finite Element Methods (Part 1). Handbook of Numerical Analysis, vol. 2, pp. 353–522. Elsevier Science Publishers B.V., North-Holland (1991). https://doi.org/10.1016/S1570-8659(05)80040-7

[29] Roberts, J.E., Thomas, J.-M.: Mixed and hybrid methods. In: Finite Element Methods (Part 1). Handbook of Numerical Analysis, vol. 2, pp. 523–639. Elsevier Science Publishers B.V., North-Holland (1991). https://doi.org/10.1016/S1570-8659(05)80041-9

[30] Babuška, I., Osborn, J.: Eigenvalue problems. In: Finite Element Methods (Part 1). Handbook of Numerical Analysis, vol. 2, pp. 641–787. Elsevier Science Publishers B.V., North-Holland (1991). https://doi.org/10.1016/S1570-8659(05)80042-0

[31] Fujita, H., Suzuki, T.: Evolution problems. In: Finite Element Methods (Part 1).
Handbook of Numerical Analysis, vol. 2, pp. 789-928. Elsevier Science Publishers B.V., North-Holland (1991). https://doi.org/10.1016/S1570-8659(05)80043-2

[32] Gostiaux, B.: Cours de Mathématiques Spéciales - 1. Algèbre [Lecture Notes in Special Mathematics - 1. Algebra]. Mathématiques. Presses Universitaires de France, Paris (1993). In French. https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre

[33] Gostiaux, B.: Cours de Mathématiques Spéciales - 4. Géométrie Affine et Métrique [Lecture Notes in Special Mathematics - 4. Affine and Metric Geometry]. Mathématiques. Presses Universitaires de France, Paris (1995). In French. https://www.puf.com/cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique

[34] Brezis, H.: Analyse Fonctionnelle. Collection Mathématiques Appliquées pour la Maîtrise. [Collection of Applied Mathematics for the Master’s Degree]. Masson, Paris (1983). In French. https://www.dunod.com/sciences-techniques/analyse-fonctionnelle-theorie-et-applications-0

[35] Ciarlet, P.G., Raviart, P.A.: General Lagrange and Hermite interpolation in Rn with applications to finite element methods. Arch. Ration. Mech. Anal. **46**(4), 177-199 (1972) https://doi.org/10.1007/BF00252458

[36] Paulin-Mohring, C.: Définitions inductives en théorie des types [Inductive definitions in type theory]. Habilitation à diriger les recherches, Université Claude Bernard Lyon I (1996). In French. https://hal.science/tel-00431817/

[37] Werner, B.: Une théorie des constructions inductives [A theory of inductive constructions]. Thèse de Doctorat, Université Paris VII (1994). In French. https://hal.science/tel-00196524v2

[38] Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci. **9**(1), 41-62 (2015) https://doi.org/10.1007/s11786-014-0181-1

[39] Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique [Formalization and proof automation in real and numerical analysis]. Thèse de Doctorat, Université Paris VI (2001). In French. https://www-lipn.univ-paris13.fr/%7Emayero/publis/these-mayero.ps.gz

[40] Semeria, V.: Nombres réels dans Coq [Real numbers in Coq]. In: Dargaye, Z., Regis-Gianas, Y. (eds.) Actes des 31es Journées Francophones des Langages Applicatifs (JFLA 2020), pp. 104-111 (2020). IRIF. In French. https://inria.hal.science/hal-02427360/

[41] Geuvers, H., Niqui, M.: Constructive reals in Coq: Axioms and categoricity.
In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Proc. of the Internat. Workshop on Types for Proofs and Programs (TYPES 2000). LNCS, vol. 2277, pp. 79–95. Springer, Berlin - Heidelberg (2002). https://doi.org/10.1007/3-540-45842-5_6

[42] Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Proc. of the 4th Internat. Conf. on Interactive Theorem Proving (ITP 2013). LNCS, vol. 7998, pp. 19–34. Springer, Berlin - Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_5

[43] Mahboubi, A., Tassi, E.: Mathematical Components. Zenodo, Genève (2020). https://doi.org/10.5281/zenodo.7118596

[44] Affeldt, R., Cohen, C., Mahboubi, A., Rouhling, D., Strub, P.-Y.: Classical Analysis with Coq. The 9th Coq Workshop (2018). https://easychair.org/smart-slide/slide/n3pK

[45] Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Research Report RR-6455, Inria (2008). https://inria.hal.science/inria-00258384/

[46] Boldo, S., Clément, F., Hamelin, D., Mayero, M., Rousselin, P.: Teaching divisibility and binomials with Coq. In: Narboux, J., Neuper, W., Quaresma, P. (eds.) Proc. of the 13th Internat. Workshop on Theorem Proving Components for Educational Software (ThEdu 2024). EPTCS, vol. 419, pp. 124–139 (2024). https://doi.org/10.48550/arXiv.2404.12676

[47] Kerjean, M., Mayero, M., Rousselin, P.: Maths with coq in l1, a pedagogical experiment. In: Narboux, J., Neuper, W., Quaresma, P. (eds.) Proc. of the 13th Internat. Workshop on Theorem Proving Components for Educational Software (ThEdu 2024). EPTCS, vol. 419, pp. 112–123 (2024). https://doi.org/10.48550/arXiv.2505.05990

[48] Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms. Undergraduate Texts in Mathematics. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16721-3

[49] Fernandes, J.L.M., Martins, P.A.F.: All-hexahedral remeshing for the finite element analysis of metal forming processes. Finite. Elem. Anal. Des. **43**(8), 666–679 (2007) https://doi.org/10.1016/j.finel.2007.02.001

[50] Martin, V., Jaffré, J., Roberts, J.E.: Modeling fractures and barriers as interfaces for flow in porous media. SIAM J. Sci. Comput. **26**(5), 1667–1691 (2005) https://doi.org/10.1137/S1064827503429363

[51] Joly, P., Rodríguez, J.: Mathematical aspects of variational boundary integral equations for time dependent wave propagation. J. Integral Equ. Appl. **29**(1),
List of Figures and Tables

<table><tr><td>1</td><td>3D mesh of a cerebral aneurysm</td><td>4</td></tr><tr><td>2</td><td>Reference Lagrange finite elements in 2D and 3D</td><td>5</td></tr><tr><td>3</td><td>Hierarchy of algebraic structures.</td><td>22</td></tr><tr><td>4</td><td>Affine geometric transformation in 2D</td><td>36</td></tr><tr><td>5</td><td>Injection onto a face hyperplane in 3D</td><td>41</td></tr><tr><td>6</td><td>Geometric transformation with a transposition in 3D</td><td>42</td></tr><tr><td>7</td><td>Affine transformation of a finite element in 2D</td><td>44</td></tr><tr><td>8</td><td>Inputs and hypotheses for the finite element transformation</td><td>45</td></tr><tr><td>9</td><td>Lagrange nodes of the reference simplex in 2D and 3D</td><td>46</td></tr><tr><td>10</td><td>Vertical slices of the reference simplex in 3D</td><td>47</td></tr><tr><td>11</td><td>Grsymlex ordering of the multi-indices in 2D and 3D</td><td>49</td></tr><tr><td>12</td><td>Lagrange nodes in 1D, 2D and 3D</td><td>56</td></tr><tr><td>13</td><td>Subvertices and Lagrange subnodes in 3D</td><td>60</td></tr><tr><td>14</td><td>Various ways to equip ℝ<sup>d</sup> with the affine space structure</td><td>68</td></tr><tr><td>15</td><td>Dependency graph of our packages and of perspectives</td><td>69</td></tr></table>