Aakash Sinha

Rémy Cazabet
email: remy.cazabet@gmail.com

Rémi Vaudaine

Systematic Biases in Link Prediction: comparing heuristic and graph embedding based methods

Keywords: graph embedding, link prediction, systematic biases, filter bubble

Link prediction is a popular research topic in network analysis. In the last few years, new techniques based on graph embedding have emerged as a powerful alternative to heuristics. In this article, we study the problem of systematic biases in the prediction, and show that some methods based on graph embedding offer less biased results than those based on heuristics, despite reaching lower scores according to usual quality scores. We discuss the relevance of this finding in the context of the filter bubble problem and the algorithmic fairness of recommender systems.

Introduction

Graph data occurs in various real-world applications such as social networks, biological networks, communication networks and many more.

In this article, we focus on the problem of link prediction (LP). LP is a classic problem on graph data, with numerous applications, from the identification of missing data to recommender systems. Several surveys have been written on the topic [START_REF] Hasan | A survey of link prediction in social networks[END_REF][START_REF] Lichtenwalter | New perspectives and methods in link prediction[END_REF][START_REF] Lü | Link prediction in complex networks: A survey[END_REF][START_REF] Yang | Evaluating link prediction methods[END_REF]. These articles have notably discussed the best way to evaluate and compare LP methods, and have studied the properties, advantages and drawbacks of different approaches. Studied approaches can be unsupervised or supervised, and be based on heuristics (e.g. the number of common neighbors, Adamic Adar index, etc.) or other approaches (block modeling, random walks, etc.).

Graph embedding is a new technique that gained significant popularity amongst the research community in recent years. Embeddings convert graph data into vectors, creating a representation of nodes in a lower dimensional vector space, on top of which various prediction and detection algorithms can be applied. These embeddings can be used, for instance, in node classification [START_REF] Bhagat | Node classification in social networks[END_REF][START_REF] Goyal | Graph embedding techniques, applications, and performance: A survey[END_REF], community detection [START_REF] Fortunato | Community detection in graphs[END_REF][START_REF] Tsitsulin | Verse: Versatile graph embeddings from similarity measures[END_REF] and role detection [START_REF] Ribeiro | struc2vec: Learning node representations from structural identity[END_REF]. Recent surveys [START_REF] Cai | A comprehensive survey of graph embedding: problems, techniques and applications[END_REF][START_REF] Goyal | Graph embedding techniques, applications, and performance: A survey[END_REF][START_REF] Cui | A survey on network embedding[END_REF] present in details the rationale, the different methods and applications of graph embeddings.

In recent years, several articles (e.g., [START_REF] Tsitsulin | Verse: Versatile graph embeddings from similarity measures[END_REF][START_REF] Grover | node2vec: Scalable feature learning for networks[END_REF][START_REF] Goyal | Graph embedding techniques, applications, and performance: A survey[END_REF]) have proposed to use graph embedding for link prediction. Such papers often claim that these approaches outperform the state of the art. It must be noted, however, that these articles are focused on proposing new embedding approaches, and do not proceed to in-depth evaluation. In particular, they often do not use the quality scores recommended in the literature, and do not investigate the results behind computing such a score.

This article is organized in three parts 1. Using a rigorous evaluation framework, we compare quantitatively recent approaches based on graph embeddings on the task of link prediction with earlier methods 2. We evaluate systematic biases introduced by each approach according to three aspects: the distance in the graph, the degrees of nodes and the community structure 3. We discuss the potential effect of the observed biases in the context of the filter bubble problem and the algorithmic fairness of recommender systems.

Link Prediction Evaluation Framework

In this section, we define a rigorous framework to compare link prediction methods. According to our experience, many recent articles on link prediction do not specify precisely their experimental sections, leading to great difficulties in reproducing the reported results. We split the evaluation framework into three independent steps, each described in the corresponding section:

1. Creation of training and test sets 2. Link Prediction 3. Evaluation using an appropriate score function

Creation of learning and prediction sets

To evaluate link prediction methods, one starts from a network dataset, and split it into a learning set and a prediction set, even if the method to test is considered as unsupervised. The learning set is considered the current state of the network, based on which predictions are made. The prediction set is considered as the future evolution of the network, i.e. the list of edges that will appear and that should be predicted. In this article as in most of the literature, we focus only on added edges, and not removed ones. Note that since methods are supervised, they need to split the learning set into a training and test set in order to learn where edges should appear. This is independent of the described distinction between learning and prediction set. In real applications, the input is an observed graph -that can be static or dynamic-and that graph corresponds to our learning set.

Static graph If the original dataset used for evaluation is a single, static graph, we remove randomly a fraction of edges of a given size. These removed edges constitute the prediction set. Following a common practice [START_REF] Goyal | Graph embedding techniques, applications, and performance: A survey[END_REF], we ensure that the resulting network is composed of a single connected component, using the following procedure:

-Remove randomly the desired number of edges -Conserve only the largest component of the resulting graph Dynamic graph For dynamic graphs, the order of edge apparition is known. A date is chosen to split the dataset in two: all edges appearing before or at the chosen date constitute the learning set, and all those appearing after the date constitute the prediction set. If the original data contains information on edges that disappear, this information is ignored. To stay coherent with the static case, the single connected component constraint also applies: in the learning set graph, only the largest connected component is conserved.

In our experiments, the learning set is composed of 80% of the original dataset. The trained classifier could be used to predict, given an unseen pair of nodes, if it should be connected by an edge or not (Yes/No prediction). However, this does not make sense in realistic settings, since we often want to answer questions such as which edges might appear in the next hours/day/month ? or What are the three most likely edges to appear connecting node n x ?. As a consequence, following previous works [START_REF] Hasan | A survey of link prediction in social networks[END_REF][START_REF] Grover | node2vec: Scalable feature learning for networks[END_REF], we assign to each pair of nodes a score corresponding to the decision function of the classifier for this sample.

Link Prediction

For each experiment, we run the link prediction process 5 times and report the average and standard deviation values.

Choice of an appropriate score function

To evaluate the quality of the prediction provided by a link prediction method, it is necessary to use a relevant score function.

It must be noted that link prediction is characterized by an extreme class imbalance. On realistic networks of large size, the density is low (<0.001%), thus the number of edges that will appear is much lower than the number of edges that will not appear.

To evaluate a model correctly, the prediction should be made on all possible |V | * |V | -|E| edges. Since this test size can be very large for real graphs, we need to reduce the size of the test set by taking a random sample without introducing any or minimal bias. In this article, we fix a sample size of 500 000. Two important observations must be made about the constitution of this sample:

-Most scores yield very different results according to the fraction of negative examples in the sample. Unlike for classifier training, it is thus essential [START_REF] Yang | Evaluating link prediction methods[END_REF] to keep its original ratio, and not take a 50%/50% sample, which is highly unrealistic.

-Due to the extreme imbalance, the number of positive examples can be extremely low even in a large sample, leading to noise in the results. Therefore we fix a lower value on the number of positive samples (10 in this article).

Two metrics, the Average Precision (AP) and the Area Under Receiver Operating Characteristic curve (AUROC) have been identified [START_REF] Yang | Evaluating link prediction methods[END_REF][START_REF] Lü | Link prediction in complex networks: A survey[END_REF] to be relevant for this task. AUROC has the property of being independent of the fraction of positive examples in the test set, while AP is favored by some because it gives a higher importance to the first few predictions, that are the most useful in link prediction settings.

Methods evaluation

In this article, we present results on three graphs previously used in articles on graphembedding techniques.

We selected large graphs, the first two being static and the last one dynamic. These graphs are FACEBOOK [START_REF] Leskovec | Learning to discover social circles in ego networks[END_REF], ASTROPH [START_REF] Leskovec | Graph evolution: Densification and shrinking diameters[END_REF] and VK [START_REF] Tsitsulin | Verse: Versatile graph embeddings from similarity measures[END_REF]. Due to space constraint, the reader can refer to their original descriptions in the referenced articles.

Method based on Heuristics

The heuristics used in all experiments are Common Neighbors, Adamic Adar, Preferential attachment, Jaccard Coefficient, nodes degree (for both endpoints) and Resource allocation index (Table 1).

Heuristics can be used for unsupervised prediction if a single of them is used: the score of the heuristic is used directly to rank pairs of nodes. They can also be used for supervised prediction by using some or all of them as features, together with a classifier. In this article, we use all heuristics together and a logistic classifier (implementation of sklearn). This supervised approach has been shown to give the best results [START_REF] Hasan | Link prediction using supervised learning[END_REF].

Heuristics Definition Common Neighbors |Γ (u) ∩ Γ (v)| Adamic Adar ∑ w∈Γ (u)∩Γ (v) 1 log |Γ (w)| Preferential attachment |Γ (u) * Γ (v)| Jaccard Coefficient |Γ (u)∩Γ (v)| |Γ (u)∪Γ (v)| Resource allocation index ∑ w∈Γ (u)∩Γ (v) 1 |Γ (w)|
Table 1: Heuristic scores for Link prediction. u,v represent the nodes, Γ (u) represents the set of neighbors of node u.

Methods based on Graph embeddings

Different embedding algorithms preserve different properties (first/second/higher order proximities) and capture different features. The four embeddings we test are:

-Laplacian Eigenmaps (LE) [START_REF] Belkin | Laplacian eigenmaps and spectral techniques for embedding and clustering[END_REF] -High-Order Proximity preserved Embedding (HOPE) [START_REF] Ou | Asymmetric transitivity preserving graph embedding[END_REF] -node2vec [START_REF] Grover | node2vec: Scalable feature learning for networks[END_REF] -Versatile Graph Embeddings from Similarity Measures (VERSE) [START_REF] Tsitsulin | Verse: Versatile graph embeddings from similarity measures[END_REF] Different operators are used to combine the vectors of nodes into edge vectors: Hadamard for LE and VERSE, Normalized Hadamard for HOPE and node2vec These operators are those observed by the authors to yield the best results. We use embeddings in 128 dimensions, as is a common practice in the literature.

Due to space constraints, we refer the reader to the original article for each method detailed description. We have chosen these methods due to their frequent use and good results observed in the recent literature, e.g., [START_REF] Goyal | Graph embedding techniques, applications, and performance: A survey[END_REF]. We have used the most common parameters. In particular for node2vec, we have systematically tested with parameter sets (p=4,q=0.5), (p=0.5, q=4), (p=1,q=1) and we report the highest score.

Results

Each method has been tested on each graph. Results are summarized in Table 2. We can observe that, compared with state of the art supervised heuristics approaches, graph embeddings do not yield clear better results. Using the AP score, heuristics always perform best. Using the ROC score, the VERSE algorithm is the only algorithm to obtain higher results. To confirm this result, we plot the precision@k score. In many applications, only the first few predictions are used, thus the relevance of this analysis.

To perform this experiment, we select randomly pairs of nodes that are not linked in the training set until we obtain 1000 positive examples, i.e., edges that do appear according to the ground truth. which allows us to preserve a balance between positive and negative examples coherent with the dataset.

Results are plotted in fig. 1. We observe that results are coherent with the scores obtained, i.e., heuristics and VERSE tend to give the best scores both for the first few predictions and for a realistic number of predictions (1000, corresponding to the number of real positive examples in the sample). In some settings, some algorithms do not yield useful predictions after the first few hundreds one (LE for ASTROPH dataset, node2vec for VK).

Analysis of systematic biases

New edges in a network can appear for different reasons, and between nodes with different properties. For instance, in a social network such as Twitter, a new follower relationship might be due to two close friends following each other, to a user following a raising celebrity they recently discovered, to strangers connecting because they think they have a common topic of interest, etc. A link prediction algorithm might have a tendency to predict some types of links more than others, a phenomenon that we call systematic bias. In this article, we focus on biases induced by the network topology. More particularly, we focus on three types of biases:

-Graph distance -Node degree -Community structure
To evaluate the biases, we study the evolution of the fraction of new edges verifying a given property. Since predicted edges are ordered, from most probable to less probable, we define the f raction@k, corresponding to the ratio of pairs of nodes satisfying this property among the k most likely edges. The dataset is selected as previously explained for the precision@k.

We define the reference value of f raction@k as the value among all edges that do appear in the ground truth (positive examples in the test set). In the scenario of a perfect prediction, the f raction@k curve should follow the ground truth scenario until 1000 (corresponding to the real number of observed edges in the test sample), and then move towards the value corresponding to the whole dataset (all pairs of nodes not linked in the training set). Edges can appear between nodes that were close or far in the graph in term of graph distance, i.e. length of the shortest path between them. It has been observed that most edges appear between nodes at a short distance, a phenomenon often called triangle closure. It is intuitively known in social network analysis by the saying "friends of my friends are my friends". Since the number of edges appearing at a distance more than two is usually very low, we consider only two cases:

Graph distance

-Short distance link: the new edge appear between nodes that were previously at distance two in the graph. -Long distance link: the new edge appear between nodes that were previously at distance three or more.

Fig. 2 presents the f raction@k of short distance link for the different methods. We can make the following observations:

-In the ground truth, most edges appear between nodes at distance 2, although the value is much lower for VK dataset. -The Heuristic-based approach is highly biased towards predicting short distance links.

-Most other approaches tend to be biased towards short distance links in the first (most probable) predictions, this value later decreases and the fraction often becomes lower than expected when the expected number of edges (1000) is reached. Most real networks have heterogeneous degree distributions, that can often be approximated by scalefree distributions [START_REF] Barabási | Scale-free networks: a decade and beyond[END_REF]. In those networks, there is a small fraction of nodes of high degrees that concentrate most of the edges. We define this class of nodes, called Hubs, as the 10% of nodes of highest degrees.

Node degree

Fig. 3 presents the f raction@k of new links that have at least a Hub among their endpoints.

We can make the following observations:

-In the three studied datasets, the f raction@k is between 0.5 and 0.6 -The Heuristic-based approach is highly biased towards high f raction@k, i.e. predicting too many edges involving hubs.

-One method seems to be clearly biased towards underestimation (LE), most other methods do not have clear tendencies. -The VERSE method is the closest to the Ground Truth at the realistic threshold (1000) in all 3 settings. Most real networks have mesoscale structures known as communities [START_REF] Fortunato | Community detection in graphs[END_REF]. The field of community detection and analysis is very active, and there is an intricate relationship between link prediction and community structure [START_REF] Clauset | Hierarchical structure and the prediction of missing links in networks[END_REF]. Because communities are dense groups of nodes, edges are more likely to appear inside communities than between them, a property that can be used both for link prediction and for community discovery in dynamic settings [START_REF] Rossetti | Community discovery in dynamic networks: a survey[END_REF].

We therefore distinguish between two types of edges, those appearing inside communities and those appearing between them.

To discover the community structure, we apply the Louvain algorithm [START_REF] Blondel | Fast unfolding of communities in large networks[END_REF], which is the most often used in the literature. This algorithm is based on Modularity optimization, thus, by definition, discover communities denser than the rest of the network. Note that the problem could be studied in more details using overlapping communities, that can introduce different effects, such as higher probabilities of edges on the overlapping parts [START_REF] Yang | Community-affiliation graph model for overlapping network community detection[END_REF] Fig. 4 presents the f raction@k of new links that appear inside communities, as found by the Louvain Algorithm.

We can make the following observations:

-In different datasets, the fraction of edges in the ground truth appearing inside communities varies widely. -The Heuristic-based approach is systematically biased towards high f raction@k, i.e. predicting too many edges inside communities. -Most methods (except n2v in FACEBOOK and LE in ASTROPH) are also biased towards overprediction of internal edges. -The bias is particularly strong among the first few prediction 5 Discussion: effect of biases on recommender systems

In recent years, both the scientific community and the civil society have started to pay attention to the problem of biased results provided by machine learning algorithms in real-life applications. Two problems have particularly been identified:

-The filter bubble phenomenon is known to occur at least in two settings: in Online Social Networks such as Facebook and Twitter, and on web search engines such as Google or Bing. The problem comes from a reinforcement phenomenon: machine learning algorithms learn the preferences of users, and show them more results according to these preferences. As a consequence, users see results that are less diverse than they should, but rather biased towards the opinions or interests that the algorithm has inferred they had in the beginning. This process has been accused to amplify the polarization phenomenon in political and social opinion [START_REF] Pariser | The filter bubble: What the Internet is hiding from you[END_REF].

-The problem of fairness of algorithms [START_REF] Berk | Fairness in criminal justice risk assessments: the state of the art[END_REF] arrises in many real-life applications of machine learning algorithms. In its most famous occurrences, a decision is taken by an algorithm that will impact individuals (who gets a loan, a job, is accepted at a university, is put in a list of potential terrorists, etc.), but the decisions taken by the algorithms are unfair towards a category of people. Typically, the algorithm learns that an ethnic or social group -or, if not present in the data, another highly correlated attribute such as locations or name-correlates with unfavorable outcomes, and therefore learns to discriminate based on this property.

These two problems are now widely known, and solutions have been proposed to mitigate them [START_REF] Bolukbasi | Man is to computer programmer as woman is to homemaker? debiasing word embeddings[END_REF], in particular by ensuring the preservation of some identified properties.

The systematic biases highlighted in the present article however have several interesting features:

-They arise without labeled data, but simply due to the network structure -The problem is not that unwanted problematic correlations are preserved, but rather that some network properties that were not explicitly required to be preserved are lost.

We can note that the efficiency of the link prediction is not necessarily linked to the absence of bias, on the contrary, methods based on heuristics clearly yield the best results in term of overall link prediction compared with recent techniques based on embeddings. However, in term of biases, we have observed that heuristics usually suffer from the highest biases. Furthermore, those biases are constantly of the same types: they tend to favor nodes at a short distance in the graph, large nodes, and nodes belonging to the same communities. In other terms, these biases can be associated with a loss in diversity. In a social network, recommendations of new contacts will favor exaggeratedly either the most similar profiles (same community, closer distance) or the most popular profiles (hubs), but will fail to identify more nuanced possibilities that would add diversity. In product or content recommendation, an algorithm based on link prediction with heuristics will propose the items the most similar to those already consumed, or the most consumed overall, ignoring the relevant possibilities in-between.

New methods based on embeddings might be part of the solution to this problem, as some of them tend to reduce those biases. In particular, it seems that the recent VERSE algorithm, that offers the best overall results among embedding techniques for link prediction accord to scores and precision@k, also consistently show lesser biases than previous techniques.

On top of that, one could follow techniques already proposed [START_REF] Bolukbasi | Man is to computer programmer as woman is to homemaker? debiasing word embeddings[END_REF] to fight against the fairness of algorithm issue, for instance by training separately for the different properties to preserve (e.g., training different classifiers to predict edges at distance 2 and at distance 3 or more).

Conclusion

We have shown that the most widely used techniques for link prediction suffer from systematic biases towards some network properties, and that those biases might play a role in the filter bubbles and algorithmic fairness problems.

We have also identified that some of the most recent techniques proposed based on graph embedding are able to somewhat reduce that problem, although they do not yet manage to improve over heuristic based methods for the overall quality of the link prediction.

We think that this work can be extended in two directions:

-On the one hand, we need to understand where do those biases come from. While it can be intuitively understood for heuristics -the features are not learned but selected according to prior knowledge, and they have been designed with triangle closure and preferential attachment properties in mind-the reason why feature learning based methods have similar biases is, to the best of our knowledge, unknown. -On the other hand, we must develop link prediction methods adapted to mitigate or eliminate those systematic biases. Ideally, such a method should not only remove the three biased identified in this article, but ensure using statistical methods that the network formed by adding the predicted edges has a similar network structure profile than the original network.

Fig. 1 :

 1 Fig. 1: Precision@k

Fig. 2 :

 2 Fig. 2: Ratio@k for the graph distance.

Fig. 3 :

 3 Fig. 3: Fraction@k for High degree nodes (hubs)

Fig. 4 :

 4 Fig. 4: Fraction@k for the community structure

  A classifier is trained from examples to recognize the pairs of nodes that are the most likely to see edges appear between them. Examples are composed of 50% of positive examples (i.e. examples of pairs of nodes that are connected by a link) and 50% of negative examples (i.e. pairs of nodes that are not connected by a link). Both positive and negative examples are picked randomly from the learning set graph. In this article, we pick 1 4 of edges in the learning set as positive examples, and an equal number of non-edges as negative examples.

Table 2 :

 2 Results for each method on each graph. Results are significant (i.e. Variance is inferior to reported precision.

	Graph Method	Heuristics LE HOPE n2v VERSE
		FACEBOOK 0.74	0.50 0.68 0.44 0.60
	AP	ASTROPH 0.79	0.06 0.43 0.22 0.48
		VK	0.063	-	-	0.006 0.021
		FACEBOOK 0.995	0.994 0.981 0.988 0.995
	ROC	ASTROPH 0.988	0.922 0.943 0.973 0.992
		VK	0.87	-	-	0.77 0.89


Reynald Affeldt

Cyril Cohen

Damien Rouhling

Formalization Techniques for Asymptotic Reasoning in Classical Analysis

Formalizing analysis on a computer involves a lot of epsilon-delta reasoning, while informal reasoning may use some asymptotic hand-waving. Whether or not the arithmetic details are hidden using some abstraction like lters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable delta. We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.

INTRODUCTION

In classical analysis, formalization problems occur when we have local reasoning, i.e. proof of facts that are only true in some neighborhood. One very early and trivial example when such reasoning occurs is to prove that the sum of two converging functions is converging. Indeed from ∀ε > 0. ∃δ f > 0. ∀x. |x -a| < δ f ⇒ |f (x) -l f | < ε ∀ε > 0. ∃δ g > 0. ∀x. |x -a| < δ g ⇒ |g(x) -l g | < ε , we get ∀ε > 0. ∃δ > 0. ∀x. |x -a| < δ ⇒ |f (x) + g(x) -(l f + l g )| < ε.

Formally proving this requires to show the existence of such a δ, here it may be the minimum of the two δ f , δ g we can get from the hypotheses applied to ε 2 . Giving δ explicitly makes the proof less stable and less readable than it would be with a correct informal reasoning. By stable proof, we mean that changes in its statement, or in statements it depends on, will break only the parts of the proof where the changes actually matter. When we provide an existential witness way before using it, the distance between the place it is used (and breaks), and the place where it is introduced, makes it dicult to maintain the proof script. Indeed, the maintainer has to go back and forth in the proof script to understand how changing the existential leads to breakage.

Filters slightly improve stability and readability by hiding arithmetic reasoning, as successfully demonstrated by previous work in the Isabelle/HOL library [START_REF] Hölzl | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL[END_REF] and in the Coquelicot library [START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF]. However, the explicit existential quantiers are still replaced by forward reasoning with statements that depend on Journal of Formalized Reasoning Vol.11, No.1, 2018, Pages 4376.

how the proof will be led. Our rst contribution is to solve this problem by giving a set of tactics and lemmas to handle existential variables in a consistent way.

Another common tool in informal classical analysis is asymptotic developments using Bachmann-Landau notations, often called little-o and big-O notations [START_REF] Bachmann | Die Analytische Zahlentheorie[END_REF][START_REF] Landau | Handbuch der Lehre von der Verteilung der Primzahlen[END_REF]. They are used to write developments such as f (x) = a 0 + a 1 x + . . .

+ a n x n + o x→0 (x n )
or in the denition of dierential: it is the linear operator df x such that f (x + h) = f (x) + df x (h) + o (h) .

Using Bachmann-Landau notations, one performs arithmetic operations with developments and uses laws like o x→0

(x n )+ o x→0 (x n ) = o x→0 (x n ).
At rst sight, the abuse of notation seems to make such a law impossible to represent as an equation on functions in a formal logic. Our second contribution is to provide a solution for this problem with a set of notations and lemmas which make the user believe that she is doing arithmetic with little-o and big-O at the same time. To our knowledge, this is the rst formalization that mixes in a purely equational manner little-o and big-O functions with arithmetic operations. The formalizations of Bachmann-Landau notations [AD04, BCF + 13, BLM15, Ebe17, GCP18] we know about either handle sets of functions or do not mix little-o and big-O.

We believe that the contributions discussed in this article are a key to make proofs in classical analysis easier in Coq [START_REF] Coq | The Coq proof assistant reference manual[END_REF], both in the development of an analysis library and in its use. We extensively tested our tools in an on-going eort to provide Mathematical Components [G + 15] with analysis [ACM + 18a]. Both the development from this article and its numerous applications can be found in the latter repository.

Outline of this Article. In Sect. 2, we remind the reader of the concept of lter and explain how we extend the ideas from the Coquelicot library with a few structures and notations to make it look closer to mathematical practice. Then, in Sect. 3, we describe our methodology to make explicit existential quantiers disappear from the proof ow; it can be seen as a special introduction rule. We provide a commented example of script that has been considerably shortened and made more stable using this methodology. In Sect. 4, we introduce our implementation of Bachmann-Landau notations. We discuss in particular in Sect. 4.1 how we represent laws using Bachmann-Landau notations as equations on functions in formal logic. We also give a few examples of informal reasoning that can actually be done as such with our techniques. Our formalization primarily targets classical analysis, which naturally calls for an extension of Coq's otherwise constructive logic. In Sect. 5, we explain the axioms on which our techniques rely, how we justify them, and why they are important to develop practical asymptotic reasoning in Coq. We discuss related work in Sect. 6 where we review in particular other formal proof libraries for Bachmann-Landau notations. Finally, we conclude in Sect. 7. We also provide in Appendix A a short overview of the contents of the Mathematical Components Analysis library [ACM + 18a], which is used both as a basis for our work and as a test base. We believe our work does not strongly depend on it, but About Notations. In this article, we introduce a number of notations that we explain as they appear (and summarize at the end of this article in Fig. 3). For the convenience of the reader, we summarize in Fig. 1 other standard Coq and Mathematical Components notations, as well as notations from previous work. This article uses and extends SSReflect tactics. For explanations about the standard ones, the reader is referred to a tutorial introduction [START_REF] Gonthier | An introduction to small scale reection in Coq[END_REF], as well as a precise documentation [START_REF] Gonthier | A Small Scale Reection Extension for the Coq system[END_REF] available online. As for the new tactics introduced in this article (namely, near=>, near • =>, near:, and end_near), they are explained in details in Sect. 3.2. They are designed as a conservative extension of SSReflect, except that they overload the tacticals => and : for introduction and discharge of hypotheses.

Coq comes with a mechanism for implicit arguments: thanks to type constraints, some arguments in denitions can be inferred. We follow in this article Coq's syntax for implicit arguments. When giving a new denition, implicit arguments are declared using curly brackets, as in Definition fct {arg1 : type1} (arg2 : type2) := ... . Then, arg1 is omitted in subsequent uses of fct, which all are of the form fct arg2.

ABSTRACTING ASYMPTOTIC STATEMENTS USING FILTERS

The use of lters in the Coquelicot library [START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF] and the Isabelle/HOL library [START_REF] Hölzl | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL[END_REF] proved that they dene a good abstraction for convergence proofs in analysis. We rst recall in Sect. 2.1 the denition of lters and give a few examples.

Then, we explain in Sect. 2.2 how our hierarchy of topological structures compares to the one of Coquelicot. We try to give just enough details to explain how to use our tools in practice. More details about these can be found in Appendix A.

Finally, we detail in Sect. 2.3 the structures and notations we use in order to make the use of lters more natural in Coq.

Denition and Use of Filters

Let us rst start with the denition of lters. A lter F on T is a set of sets of elements of T that satises the following three laws:

T ∈ F, ∀A, B ∈ F. A ∩ B ∈ F and ∀A, B. A ⊆ B ⇒ A ∈ F ⇒ B ∈ F.
Our Coq representation of lters is exactly the same as in the Coquelicot library, i.e. the propositional predicate Filter F, which states that the set of sets F : set (set T), is a lter. Additionally, this predicate is a class, in order to trigger type-class inference when needed 1 .

Class Filter {T : Type} (F : set (set T)) := { filterT : F setT ; filterI : forall

P Q : set T, F P -> F Q -> F (P `&`Q) ; filterS : forall P Q : set T, P `<=`Q -> F P -> F Q }.
We additionally provide the type filter_on T of lters on a type T, with an implicit coercion so that F : filter_on T may also be seen as a set of sets on T, satisfying the property Filter F. Structure filter_on T := FilterType { filter :> (T -> Prop) -> Prop; filter_class : Filter filter }.

This structure is used to register canonical lter instances in addition to typeclass instances. Eventually, we might unify both inference mechanisms by choosing canonical structures over type-classes. The topic of structure inference is however beyond the scope of this article, and we recommend dedicated papers about it. [START_REF] Sozeau | First-class type classes[END_REF][START_REF] Mahboubi | Canonical Structures for the Working Coq User[END_REF] The most important sort of lters used for analysis and local reasoning is the lter of neighborhoods. The set of neighborhoods of a point x indeed denes a lter, called locally(x) in Coquelicot [START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF] and in our work. In Coquelicot, the notion of neighborhood is dened using balls in a uniform space. Thus, the neighborhood lter of x is locally

(x) = {A | ∃ε > 0. ball ε (x) ⊆ A} .
Balls can also be used to dene another lter which is the set of entourages. An entourage is a set that is a neighborhood of the diagonal set {(x, x) | x ∈ T }, i.e. a set that contains all the pairs (x, y) such that y ∈ ball ε (x) for some positive ε.

An important point to notice here is the fact that the lter of entourages is dened as the set of supersets of the family of sets ({(x, y) | y ∈ ball ε (x)}) ε>0 .

In fact, we often use this kind of construction in proofs about lters. Hence, we dene a function filter_from that takes a family of sets and returns its set of Here, D should be understood as the domain of indices and B denes the family. We also use notations for set comprehension and set inclusion that have been introduced in a previous work [START_REF] Cohen | A Formal Proof in Coq of LaSalle's Invariance Principle[END_REF] (see Fig. 1). If the domain is not empty and if for any two indices i and j in the domain one can nd a third index k in the domain such that B k ⊆ B i ∩ B j , then we say that the family denes a lter base and we prove that filter_from D B indeed denes a lter. The entourage lter is then easily dened using filter_from and the family of sets described above 2 . Since we are using balls, this denition is valid in a uniform space, denoted by uniformType in our work (note there is an implicit coercion from a uniformType to its carrier in Type). In fact, a more abstract denition of entourages, which does not rely on balls, could replace balls as primitive for the denition of the type representing uniform spaces. This would lead to an equivalent denition of uniform spaces where the pseudometric is abstracted, but we kept Coquelicot's denition for this work.

We can also use the filter_from function to dene the lter product: if F and G are respectively lters on spaces T and U , then the lter product of F and G is a lter on the Cartesian product T × U and is dened as the set of supersets of the family (P 1 ' * ' P 2 ) P1∈F,P2∈G where A ' * '

B = {(a, b) | a ∈ A, b ∈ B}.
Definition filter_prod {T U : Type} (F : set (set T)) (G : set (set U)) := filter_from (fun P => F P.1 /\ G P.2) (fun P => P.1 `*`P.2).

This is a simplication of the lter product from the Coquelicot library, which is dened using an inductive predicate. This can easily be generalized to the n-ary lter product, allowing us in particular to build the neighborhood lter of a vector in R n as the n-ary lter product of the neighborhood lters of its components.

A last construction which is of interest for analysis is the image of a lter by a function. Given a function f from T to U and a lter F on T , the image of

F by f , dened by f (F ) = B | f -1 (B) ∈ F ,

Mathematical Components Analysis hierarchy

The main benet of lters for analysis is to rephrase ε-δ phrasing into more concise statements. For instance, f (locally(x)) ⊇ locally(y) stands for lim x f = y and ((x, y) → (f (x), f (y)))(entourages) ⊇ entourages states that f is uniformly continuous. Preserving this abstraction also shortens the proofs.

About the Mathematical Components Analysis Hierarchy

Our library inherits several of its topological structures from the Coquelicot library (see Fig. 2). We remove the structures that can be replaced with those of the Mathematical Components library, e.g. the Ring structure from Coquelicot is replaced with Mathematical Components's ringType, and we reimplement the other structures. We mentioned in Sect. 2.1 the type representing uniform spaces (uniformType). We also reimplement the structure representing normed modules (normedModType K) over a ring K equipped with an absolute value (absRingType). In this work, the norm of x is denoted by `|[x]|. Finally, we also adapt to our context the types representing complete spaces (completeType), analogous to complete metric spaces but with a lter-based notion of convergence, and complete normed modules (completeNormedModType K). The corresponding formal denitions can be found in [ACM + 18a, le hierarchy.v] together with their main properties, and we provide a short description of them in Appendix A.

Moreover, we extend Coquelicot's hierarchy with our own structures. Having uniform spaces at the bottom of the hierarchy as in the Coquelicot library makes some proofs harder or even impossible. In particular, Tychono 's Theorem has a very concise proof in terms of lters where the topology induced by balls in a uniform space is not appropriate [START_REF] Rouhling | A Formal Proof in Coq of a Control Function for the Inverted Pendulum[END_REF].

Topological spaces come with their own notion of neighborhood: the set A is a neighborhood of p if A contains an open set B which contains p. Although the neighborhoods dened by balls (recall the denition of locally(x) in Sect. 2.1) are compatible with this notion of neighborhood for the uniform topology, some sets cannot be expressed as neighborhoods of a point in a topological space. Indeed, neighborhoods of +∞ (dened as Rbar_locally +oo in Sect. 2.3) are for instance subsets of R and +∞ is not a point of R.

In order to reconcile the dierent notions of neighborhoods, we put three structures below our copy of Coquelicot's hierarchy (as shown in Fig. 2). Elements of each of these structures have an implicit coercion to their carrier and can be used as if they were types.

A structure for non-empty types, with a distinguished point, represented by the pointedType structure (see [ACM + 18a, le classical_sets.v]).

A family of types T : filteredType U, such that elements t of T represent sets of sets on U, through the ltered space operator locally : T -> set (set U). This is just for sharing purposes, so we do not enforce that locally t is a lter yet. Moreover, having T dierent from U makes it possible to have locally +oo equal to Rbar_locally +oo, thanks to an instantiation of the filteredType R structure as the canonical lter on R associated to +oo : Rbar. We require T to be non-empty (see [ACM + 18a, le topology.v] for details).

Finally, a topological space structure topologicalType, for which we enforce that the T and U in the operator locally are the same and that locally t is exactly the proper lter generated by the lter base of open neighborhoods of t

(see [ACM + 18a, le topology.v] for details).

In the uniform space structure (copied from Coquelicot), we enforce that locally t also coincides with the lter generated by the lter base of uniform balls, which was not necessarily chosen the same as the basis for open sets.

These additions also give us the opportunity to provide shorter and generic notations, closer to the mathematical practice, in order to improve readability, as explained in the next section.

Notations for Limits and Convergence

In a previous work [START_REF] Cohen | A Formal Proof in Coq of LaSalle's Invariance Principle[END_REF], we introduced notations in order to represent the convergence statement lim

x f = y as f @ x --> y in Coq. In fact, we provide the notation f @ F for the lter f (F ) and the notation F --> G for reverse lter inclusion (F ⊇ G). However, in the notation f @ x --> y, usually the variables x and y are not lters but points in a uniform space. Hence, we also have a mechanism based on canonical structures [START_REF] Mahboubi | Canonical Structures for the Working Coq User[END_REF] to automatically infer the lter corresponding to the type of the point. For instance, if x is in a uniform space, then the neighborhood lter locally(x) is inferred, or if x is +∞, or +oo in Coq using our notations, then it is Coquelicot's lter of neighborhoods of +∞ [START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF] Rbar_locally +oo = {A | ∃M. ]M, +∞[ ⊆ A} .

In the particular case of functions, dedicated canonical structures are dened to match their source type. If it is nat, then the function is a sequence, hence we infer the lter u @ eventually, where eventually is Coquelicot's equivalent of Rbar_locally +oo for sets of natural numbers, in order to be able to write u --> y for lim u = y. If the source type is a function type, then we recognize in particular the case where x is a function of type (T -> Prop) -> Prop, hence a set of sets. The inferred lter is then x itself.

For pointed types (and hence every structure from our hierarchy), using our classical axioms from Sect. 5, we can dene an Hilbert's epsilon function we call get.

It takes a predicate P and outputs a point which satises P if there is one (and outputs a default point otherwise). This function makes it possible to dene functions computing the limit of a function (see lim_in below), the generic mklittleo operator (see Sect. 4.2), or the dierential of a function (see Sect. 4.5).

Definition lim_in {U : Type} {T : filteredType U} := fun F : set (set U) => get (fun l : T => F --> l).

Here, the function lim_in takes as input a lter and outputs a limit of F if there is one; T denes canonical lters on U. We say then that l is a limit of F if the canonical lter associated to l is contained in F. In particular, if the lter F is of the form f @ x for some function f and some point x, then lim_in F is the limit of f at point x. We provide the notation [lim F in T] to represent the limit of lter F in T : filteredType U.

The lim_in function also makes it possible to express the fact that a lter or function converges without using an existential quantier: a lter or function converges if and only if it converges to its limit.

Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]).

Lemma cvg_ex (U : Type) (T : filteredType U) (F : set (set U)) : [cvg F in T] <-> (exists l : T, F --> l).

We also provide the notation cvg F, which triggers the inference of T in order to build the term [cvg F in T]. The complete formalization of limits and convergence can be found in [ACM + 18a, le topology.v].

SMALL-SCALE FILTER ELIMINATION

Although lters are a good way to hide epsilon-delta in statements, in order to prove F P for some ultimately true proposition P, one might be tempted to replace the lter F by its denition. This may result in a breakage of abstraction and lead to longer and less stable proof scripts (e.g. if the lter slightly changes).

Libraries such as Coquelicot already provide tools to combine results on lters without doing any unfolding. We copy and extend the same tools in Sect. 3.1. We then show how to go one step further in the transparency of lters in Sect. 3.2. Section 3.3 explains how to phrase Cauchy lters so as to make their denition usable more easily by our tools. Finally, Sect. 3.4 illustrates our tools in action in a real proof and Sect. 3.5 details the dierences between this proof and the corresponding one in Coquelicot.

Combining Filters by Hand

The dening properties of lters entail the following facts.

Lemma filter_app (T : Type

) (F : set (set T)) : Filter F -> forall H G : set T, F (fun x => H x -> G x) -> F H -> F G.
Lemma filterE (T : Type) (F : set (set T)) : Filter F -> forall G : set T, (forall x, G x) -> F G.

The rst lemma can be used to combine hypotheses of the form F H i and a conclusion F G into F (fun x => H 1 x -> . . . -> H n x -> G x), and the second lemma removes the lter so that we shall prove instead the (hopefully) simpler goal forall x, H 1 x -> . . . -> H n x -> G x.

However this forces forward reasoning, since the user has to anticipate every fact H i x that will be used in the proof of G x beforehand. This means the statements H i have to be written explicitly by the user, and they often depend on the choice of splitting of epsilons in the rest of the proof, which was also the main source of instability of proof scripts without using lters. This clearly appears in the proofs of the lemmas of the double limit theorem filterlim_switch_1 and filterlim_switch_2 in the Coquelicot library [BLM18, le Hierarchy.v].

We now show a novel method which absolves the user from providing explicitly the statements H i .

The Tactics near=>, near • =>, near:, and end_near

The purpose of this section is to explain the new near tactics we provide to perform small-scale lter elimination.

The basic principle of lter elimination is to make the user believe that instead of proving F Q she should instead prove Q x directly, where x can be in an arbitrarily precise set belonging to F. The lemma filter_near_of describes this formally3 : the in_filter record is the type of sets belonging to F, hence P represents the arbitrarily precise set containing x. Record in_filter T (F : set (set T)) := InFilter { prop_in_filter_proj : T -> Prop; prop_in_filterP_proj : F prop_in_filter_proj }.

Lemma filter_near_of T F (P : in_filter T F) (Q : set T) :

Filter F -> (forall x, prop_in_filter_proj P x -> Q x) -> F Q.

From now on, we sometimes use the notation \forall x \near F, G x, which is a notation for F (fun x => G x). This should be read for all x which is near F, G x holds, and we will use this phrasing instead of the too specic ultimately true or eventually true. We also dene the notation x \is_near F for prop_in_filter_proj P x for some P : in_filter T F. This notation deliberately hides P since it is not meant to be given by the user but rather instantiated trough the use of the near tactics.

3.2.1

Using near=>, near: and end_near (1) The tactic near=> x performs an introduction.

On a goal of the form \forall x \near F, G x, it puts into the local context a variable x and an hypothesis x \is_near F and yields the goal G x. The latter hypothesis hides an existential variable ?H for the neighborhood to which x belongs, so that the membership proof F ?H is actually delayed. This is in fact a simple application of Lemma filter_near_of. Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?.

We call the x which is now in the local context a near-variable. A near-variable could be dened as variables x which come with an hypothesis x \is_near F, hiding an existential variable, in the local context.

(2) The tactic near: x discharges the near-variable x.

On a goal of the form H i x such that the hypothesis x \is_near F is in the context, it yields the goal \forall x \near F, H i x. This partially instantiates the existential variable ?H associated with the hypothesis x \is_near F as the intersection between H i and a fresh existential variable ?H'. The user is invited to prove the goal right away.

If H i had already been added to the set hidden in the hypothesis x \is_near F through a previous use of near: x, then it immediately closes the goal without modifying ?H.

(3) Once the main goal has been proved, there remain existential variables that have not been instantiated. These correspond to the ?H' in the last calls of the near: x tactic. They can be instantiated with the total set, since it belongs to any lter. This is the purpose of the end_near tactic.

3.2.2

Using near F => x, near: and end_near. Instead of acting on the goal, the tactic near F => x introduces a variable x along with the x \is_near F hypothesis, once again hiding an existential variable. After using near F => x, one may use near: and end_near in exactly the same ways as before. The tactic near F => x requires the lter F to be proper, i.e. no set H in F is empty.

3.2.3

Combining all Near Tactics. The tactics near=> x and near F => y may be combined any number of times, and in any order. Near-variables can be discharged by using near: z provided that the statement contains only variables introduced before z was. This limitation, guaranteed by Coq type checking, is legitimate as we must not be able to introduce circular dependencies in the existential variables.

For the detailed implementation of the near tactics, we refer the reader to the formalization [ACM + 18a, le topology.v].

Rephrasing Concepts

Our methodology requires that some lemmas are phrased in a particular way.

For example there are several equivalent ways to dene a Cauchy lter. The most (ε-δ)-ish way is Definition cauchy_ex {T : uniformType} (F : set (set T)) := forall eps : R, 0 < eps -> exists x, F (ball x eps).

However it is easier to use the following equivalent denition:

Definition cauchy {T : uniformType} (F : set (set T)) := forall e, e > 0 -> \forall x & y \near F, ball x e y.

Indeed, the existential quantication is then encapsulated in the \near F notation and can thus be treated in a systematic way in our proofs. This rephrasing could be disturbing for users that might not immediately see these are the same concepts. Hopefully they can be convinced by simple equivalence lemmas.

Lemma cauchyP (T : uniformType) (F : set (set T)) : ProperFilter F -> cauchy F <-> cauchy_ex F.

Although this particular equivalence is only true for proper lters, it is sucient since in practice we manipulate only lters that are proper.

Note that the point of view of uniformType in terms of entourages leads to an even more compact equivalent denition, which we use as an intermediate step in the proof of cauchyP.

Lemma cauchy_entouragesP (T : uniformType) (F : set (set T)) : Filter F -> cauchy F <-> (F, F) --> entourages.

Here, the lter associated to (F, F) in the • --> • notation is inferred as the product lter filter_prod F F thanks to the canonical structures mentioned in Sect. 2.3.

In the same vein, our denition of big-O in Sect. 4.1, which is equivalent to standard ones, encapsulates both existential quantiers from the mathematical denition in the \forall \near notation to work better with the near tactics.

Use-Case: a Short Completeness Proof

We detail a proof that the type of functions from an arbitrary (choice) type to a complete type is again complete. This proof is interesting for several reasons. Before all, observe that the implicit type of the Cauchy lter is not T -> U as it may appear at rst sight; it is actually inferred to be fct_uniformType T U, the type of functional metric spaces, which is a uniformType, as required by the denition of Cauchy lter (see Sect. 3.3). The mechanism at work here is (again) the one of canonical structures [START_REF] Mahboubi | Canonical Structures for the Working Coq User[END_REF].

We start by proving that for all t of type T, the lter {{f (t) | f ∈ A} | A ∈ F} is Cauchy in U. This lter can be expressed succinctly as soon as one observes that it is the image of the lter F by the function fun f => f t. More precisely, it can be written ((fun f => f t) @ F) using the inx notation @ that denotes the image of a lter (see Fig. 1). Line 1 below states that this lter is Cauchy 4 ; line 2 proves this fact. The proof is very simple since it is a direct consequence of cauchy F (the local hypothesis labeled Fc introduced at the beginning of line 1).

move=> Fc; have /(_ _)/complete_cauchy Ft_cvg : cauchy (@^~_ @ F). by move=> t e ?; rewrite near_simpl; apply: filterS (Fc _ _).

At this stage, we have to prove cvg F, knowing that cauchy F holds as well as forall t : T, cvg ((fun f => f t) @ F). This latter hypothesis is a direct consequence of the subgoal we explained just above. It results from the application performed at line 1 of Lemma complete_cauchy to the following subgoal, proved by line 2, forall t : T, cauchy ((fun f => f t) @ F). Under these hypotheses, the function fun t => lim ((fun f => f t) @ F) is the pointwise limit of the lter F. We now prove that this limit is uniform. apply/cvg_ex; exists (fun t => lim (@^~t @ F)).

Under the same hypotheses as before, we now have to prove: F --> (fun t : T => lim ((fun f => f t) @ F)).

Since the right-hand side is a point of T -> U, it is interpreted as the lter of neighborhoods of this point. So it suces to prove, for all e such that e > 0, that we have \forall f \near F, ball (fun t : T => lim ((fun f => f t) @ F)) e f. This goal transformation is achieved at the beginning of line 4 by the application of the Lemma flim_ballPpos. After application of this lemma, we are in a position to use the near tactics as we will explain shortly. apply/flim_ballPpos => e; near=> f => t; near F => g => /=.

The rst near tactic used at line 4 has the following consequence: we are asked to prove for all f which are near F and for all t that ball (lim ((fun f => f t) @ F)) e (f t) holds. The proof goes by introducing a g, which is near F as well; this is also achieved at line 4 by the second near tactic.

We then split the ball around (g t) (using Lemma ball_splitl, see line 5) and are left to prove two goals:

(1) ball (lim ((fun f => f t) @ F)) (e / 2) (g t), and

(2) ball (f t) (e / 2) (g t) which will both be true when g is near F, so that we will use the near: g tactic.

We claim that this reasoning is an informal one in the sense that this proof step does not need to be interleaved with technical proofs that can be handled later as mere consequences of near facts.

The rst goal can be proved by Ft_cvg (the hypothesis obtained from line 1).

The terseness of SSReflect tactics actually allows us to prove it on the same line of proof script as the application of Lemma ball_splitl:

apply: (@ball_splitl _ (g t)); first by near: g; exact/Ft_cvg/ locally_ball.

The second goal can be proved for all values of t, when f is near F, so that we rst generalize t, using move: (t), and then discharge g and f using near: twice: by move: (t); near: g; near: f; apply: nearP_dep; apply: filterS (Fc _ _).

After calling near: f, we have to prove \forall f \near F, \forall g \near F, forall t, ball (f t) (e / 2) (g t).

This is achieved by using Lemma nearP_dep (see line 6). We can conclude because the lter F is Cauchy and e / 2 is obviously positive (this is automatically proved by using another set of canonical structures).

The last line of the proof script is for proving automatically the remaining trivial existentials:

Grab Existential Variables. all: end_near. Qed.

Dierences with the Proof in Coquelicot

Several dierences occur between both the statements and the proofs of Lemma fun_complete (Sect. 3.4) and Lemma complete_cauchy_fct (Coquelicot library [BLM18, le Hierarchy.v]). Let us clarify them. First, let us compare the statements. Both Lemma fun_complete and Lemma complete_cauchy_fct state that for any proper lter on the function space T -> U, if it is Cauchy, then it converges, but both the denitions of Cauchy lters and lter convergence dier. For Cauchy lters, we use the cauchy predicate from Sect. 3.3 while cauchy_ex is used in Coquelicot. This forces the authors of Coquelicot to use in their proof an additional lemma [BLM18, Lemma cauchy_distance, le Hierarchy.v], which states the equivalence between cauchy_ex and a predicate which is very close to cauchy once the \forall \near notation is unfolded.

For lter convergence, the authors of Coquelicot use an epsilon phrasing which amounts to: \forall eps, 0 < eps -> F (ball (lim F) eps).

We choose instead the cvg F notation (recall Sect. 2.3), which is equivalent to F --> lim F, i.e. F contains the neighborhood lter of lim F. In our denition, balls are thus abstracted through the use of the topology. However, our proof of Lemma fun_complete still resorts to balls so we have to use an additional lemma [ACM + 18a, Lemma flim_ballPpos, le hierarchy.v] in order to get back the epsilon phrasing.

These two dierences taken into account, the two proofs follow the same reasoning. Apart from the impact of the near tactics, the remaining dierences in the proofs are due to naming conventions and to slight reformulation of some lemmas.

MECHANIZATION OF BACHMANN-LANDAU NOTATIONS

When Donald Knuth addresses the editor of the Notices of the American Mathematical Society about teaching calculus, he insists on using the big-O notation such as it blends smoothly into equational reasoning [START_REF] Knuth | Teach Calculus with Big O[END_REF]. [I]t signicantly simplies calculations because it allows us to be sloppy but in a satisfactorily controlled way.

He goes as far as dream[ing] of writing a calculus text entitled O Calculus. This section synthesizes the key ideas that mechanize Knuth's dream in a provably correct fashion. We explain the basic intent of our mechanization in Sect. 4.1, show how we recover an equational view with little-o and big-O notations in Sect. 4.2, describe a few aspects of the equational theory in Sect. 4.3, and provide concrete evidence of its usefulness in Sections 4.44.6.

The Notations f = o(e) and f = O(e)

The little-o and big-O notations are traditionally dened by

f = o 0 (e) or f (x) = o x→0 (e(x)) ⇔ ∀ε > 0. ∃δ > 0. ∀x. |x| < δ ⇒ |f (x)| ε|e(x)|, f = O 0 (e) or f (x) = O x→0 (e(x)) ⇔ ∃k > 0. ∃δ > 0. ∀x. |x| < δ ⇒ |f (x)| k|e(x)|.
For the sake of readability we gave the denitions of these notions at a neighborhood of 0, but they are generalized to any lter in our library [ACM + 18a, le landau.v].

The equality in the notation f = o(e) is a well-known abuse of notation. Indeed it is neither symmetric, since one cannot write o(e) = f , nor transitive, since f = o(e) and g = o(e) do not imply f = g and not even f ∼ g (cf. Sect. 4.4).

In fact, f = o(e) should be read as f is a little-o of e. It is not rare to see this reading enforced by the notation f ∈ o(e) in undergraduate-level teaching, allegedly to prevent students' confusion (see for example in [START_REF] Arnaudiès | Cours de mathématiques[END_REF], a textbook from the eighties still popular in France). It is therefore no surprise to nd o 0 (e) viewed as a set of functions, or equivalently a predicate on functions, even in recent formalizations [START_REF] Guéneau | A stful of dollars: Formalizing asymptotic complexity claims via deductive program verication[END_REF].

Our formalization builds on the set-theoretic notation using a type-theoretic variant. Indeed, we provide both a predicate littleo_def for functions that are little-o of other functions at some lter, and a sigma-type littleo_type. Similarly for big-O, we provide a predicate bigO_def and a type bigO_type. The formal denitions of the predicates advantageously use the \near notation introduced in Sect. In this article, we make a strong case for the equational viewpoint, and we explain in the next section how to recover it.

The Notations

f = g + o(e) and f = g + O(e)
Indeed it is also in the folklore to write f = g + o(e) to mean f -g = o(e) in the previous acceptation. Since expressions involving the little-o notation are to be considered as classes of functions, the formula f = g + o(e) suggests a reading in terms of a congruence relation. It might therefore seem like a good idea to formally dene the corresponding equality and let it be denoted by a ternary notation. However, doing so carelessly might preclude routine mathematical practice, rst 57 because the bound e changes a lot from one equality to another, for example, if

f (x) = g(x) + o x→0 (x) then xf (x) = xg(x) + o x→0
x 2 . Second, mathematicians add little-o and big-O from various scales as in:

if f (x) = g(x) + o x→0 (x) and g(x) = O x→0 x 2 then f (x) = o x→0 (x).
To reect this mathematical practice, we decided to stress that f = g + o(e) means f = g + h where h is a little-o of e, which is dened formally as follows.

Denition 4.2.1. We dene o(e)[h] to be h if h is a little-o of e, and 0 otherwise.

In particular, the statement

f = g + o(e)[h] means f = g + h if h is little-o of e,
and f = g otherwise. In Coq, to dene o(e)[h], we provide a function mklittleo5 that builds a little-o from an arbitrary function. Given a function h, mklittleo tries to coerce it to the subtype of little-o's and, when it fails, it returns the null little-o (using the function littleo0 mentioned in Sect. 4.1). This mechanism of partial projection into a subtype is provided by the generic operator insubd from the Mathematical Components library: Definition mklittleo (F : filter_on T) (h : T -> V) (e : T -> W) := littleo_fun (insubd (littleo0 F e) h).

Notation "[o_ x e 'of' h ]" := (mklittleo x h e) (at level 0, x, e at level 0, only parsing).

In order to avoid stating witnesses explicitly, we notice that if f = g + h, then h = f -g hence h is a little-o of e if and only if f -g is. This leads us to dene the sought ternary notation to be:

Notation "f = g '+o_' x e" := (f = g + [o_x e of f -g]).

The ternary notation f = g +o_x e expands to f = g + [o_x e of f -g]. We then deliberately hide the h in the printing of the notation so that [o_x e of h] prints back 'o_x e.

However, if we try to prove f = g +o_x e in a purely arithmetical way, we might rewrite with equations for f and g and nally get a goal of the form o(e) = o(e). In a paper-and-pencil proof, this is considered as trivial, but in a formal proof, both little-o hide functions h and h , and the statement to prove is in fact the equality o(e)[h] = o(e)[h ]. In this situation there is very little chance that this unication succeeds, so our methodology consists in replacing h by an existential variable ?h as soon as possible. This is made possible because of the following observation:

f = g + o (e) [f -g] ⇔ ∃h. f = g + o (e) [h] , (1)
which allows to replace a goal f = g +o_x e by a goal f = g + [o_x e of ?h] (printed f = g + 'a_o_x e) where ?h is an existential variable.

Equational Theory

Our main concern is to preserve the benets of the equational view of little-o and big-O. That means developing a small theory containing the main equations one Context {F : filter_on T}.

Lemma equiv_sym (f g : T -> V) : f ~_F g -> g ~_F f. Proof. move=> fg; have /(canLR (addrK _))<-:= fg. by apply: eqaddoE; rewrite oppo (equivoRL _ fg). Qed.

The rst line of the proof script is made of standard tactics that change the goal to f -o(g) ∼ f . Lemma eqaddoE implements the idea of (1): it introduces an existential variable ?h such that the goal becomes f -o(g

) = f + o(f )[?h].
Rewriting with Lemma oppo turns f -o(g) into f + o(g) and Lemma equivoRL turns o(g) into o(f ) (it uses the hypothesis f ∼ g). The right-and left-hand sides can now be unied and the proof is completed.

The transitivity of ∼ is mechanized as follows: Lemma equiv_trans (f g h : T -> V) : f ~_F g -> g ~_F h -> f ~_F h. Proof. by move=> -> ->; apply: eqaddoE; rewrite eqoaddo -addrA addo. Qed.

After the application of Lemma eqaddoE, the goal is

h + o (h) + o h + o (h) ∼ h + o (h) [?e],
where ?e is an existential variable. Lemma eqoaddo transforms o(h + o(h)) into o(h) and Lemma addo transforms o(h) + o(h) into o(h). After rewriting, the goal is h + o(h) ∼ h + o(h)[?e], so that unication succeeds and completes the proof.

Application: Dierential of a Function

We use the little-o notations, in combination with the get function from Sect. 2.3, in order to dene the dierential of a function: Definition diff (F : filter_on V) (f : V -> W) := (get (fun (df : {linear V -> W}) => forall x, f x = f (lim F) + df (x -lim F) +o_(x \near F) (x -lim F))).

where the x of (x \near F) is used to nd the function hidden by the little-o, and, let us recall from Sect. 4.1, where V and W are normed modules over a ring K equipped with an absolute value (see [ACM + 18a, le derive.v] for details).

We remarked in previous work [START_REF] Cohen | A Formal Proof in Coq of LaSalle's Invariance Principle[END_REF][START_REF] Rouhling | A Formal Proof in Coq of a Control Function for the Inverted Pendulum[END_REF] that having such a function for the dierential and using additional hypotheses that state which functions are dierentiable makes proofs more natural and easier than using only a predicate stating that an expression is the dierential of a function. Theoretically, many theorems proved using these axioms might in practice be established without them, at the cost of changing the notion of equality. Indeed, we could replace many uses of the generic (Leibniz) Coq equality with a weaker form of equality such as pointwise equality for functions or equivalence for propositions. However, this would make proofs considerably longer, for no particular benets. Moreover, the main proof assistants where classical logic is primitive (i.e. Isabelle/HOL, HOL Light, HOL4, Mizar) also have a primitive equality which is extensional for functions and propositions, and so does Lean.

These extensionality axioms are particularly useful in stating and reasoning about equality on sets and equality on lters (which ultimately boils down to the former).

Indeed, since we represent sets on a type T as functions of type T -> Prop the combination of the two axioms helps state and reason about equality of functions whose target is a proposition. This is so pervasive that we even have the following lemma (as well as several variants):

Lemma predeqE {T} (P Q : set T) : (P = Q) = (forall x, P x <-> Q x).

Classical Axioms

The other two axioms on which our development relies are classical axioms:

pselect: forall (P : Prop), {P} + {~P}. gen_choiceMixin: forall {T : Type}, Choice.mixin_of T.

The axiom pselect is a strong version of the law of excluded middle, where the result can be used to give a value in Type. The axiom gen_choiceMixin states the existence of a choice function on any type, which we do not detail here as it is specic to the Mathematical Components library (see [START_REF] Mahboubi | Mathematical Components[END_REF]Sect. 7.3]). These two axioms are justied by the axiom constructive_indefinite_description from the Coq standard library, which is one formulation of Hilbert's epsilon, and by the axiom of propositional extensionality from Sect. 5.1. This is best illustrated by the proof of the axiom pselect. The latter is established in part as a consequence of the standard law of excluded middle (i.e. in Prop), which we prove as Diaconescu's theorem [START_REF] Diaconescu | Axiom of choice and complementation[END_REF] using both indenite description and propositional extensionality.

These classical axioms are used in particular in our implementation of Bachmann-Landau notations. The latter indeed relies on an operation that takes a function, nds out whether it is a little-o and outputs the proof when it is the case, and otherwise returns the null little-o. We do not know if there is a constructive alternative, like taking the minimum of two functions, in order to force it to be a little-o.

In contrast, it is likely that the near tactics still work without classical axioms, since their ancestor bigenough did work to prove facts about Cauchy reals [START_REF] Cohen | Formalized algebraic numbers: construction and rstorder theory[END_REF].

RELATED WORK

Our work takes its starting point in the re-implementation of the Coquelicot library [START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF] to make it fully compatible with the Mathematical Components library [GAA + 13], in order to be able to combine algebra and analysis in the same framework. We alter Coquelicot's hierarchy by adding more structures (see Fig. 2), and with notations that make formal statements closer to the mathematical ones (see Fig. 1 and Sect. 2.3). We reformulate many denitions and theorems involving asymptotic reasoning to take advantage of the near tactics, which make proofs shorter. On the other hand, several parts of the Coquelicot library have not been adapted to our new context yet (mostly, sequences, integrals, and series).

The Coquelicot library also contains ternary predicates dening little-o and asymptotic equivalence of functions. Our denitions are basically the same (in particular the ternary predicate littleo) but their theory is not quite developed in Coquelicot. We provide a set of notations (see Fig. 3) and a more substantial equational theory on top of our denitions, which make them easier to manipulate.

We also have notations and a theory for big-O.

The Coquelicot library provides total functions to compute the limit and the derivative of a function. They are however restricted to functions from R to R. We dene a limit function for any function whose domain and codomain are equipped with canonical lters and a dierential function for any function whose domain and codomain are normed modules. The crucial dierence is that we include the existence of choice functions in our hierarchy at the cost of additional axioms, which give us these functions for free, while in the Coquelicot library they are constructed from the limited principle of omniscience.

Avigad and Donnelly's formalization in Isabelle/HOL [START_REF] Avigad | Formalizing O notation in Isabelle/HOL[END_REF] views big-O as sets. They describe inclusion and equational reasoning on big-O at the set level, and they manage to prove the prime number theorem using it. Thirteen years later, Eberl improves and extends their work by providing, in addition to big-O, the littleo, Ω, ω, and Θ notations, in order to prove the complexity of divide-and-conquer algorithms [START_REF] Eberl | Proving divide and conquer complexities in Isabelle/HOL[END_REF]. Coupled with Isabelle/HOL's heavy automation, his Landau symbols halve the size of his proofs [Ebe17, Sect. 3.2.2]. His Landau symbols are dened using the eventually construct of the standard library that applies a predicate to a lter. Formal proofs therefore enjoy the eventually_elim tactic that automates the application of lter-related lemmas together, and is often combined with other lemma collections (such as field_simps). The tactic eventually_elim is a simpler form of the near tactics, well adapted to Isabelle/HOL proof style. Indeed, when using eventually_elim one lists upfront a list of hypothesis that will be used by the automated proof search. Using near, these sets are inferred at the appropriate places while writing the proofs in an imperative style.

Guéneau et al. [START_REF] Guéneau | A stful of dollars: Formalizing asymptotic complexity claims via deductive program verication[END_REF] have developed in Coq a library to formalize the timecomplexity of OCaml programs. To represent asymptotic bounds, they provide a formalization of the big-O notation. Similarly to us, their denition relies on lters, but only on nite lter products of the eventually lter (see Sect. 2.3) and its equivalent in Z. Furthermore, they dene a type for types equipped with one lter, while we make it possible to have a dierent lter for each element of the type. Their proofs also use delayed production of witnesses of existential quantiers in the particular case of the computation of cost functions. They use Procrastination [START_REF] Guéneau | Procrastination, a proof engineering technique[END_REF], a small library of tactics similar to our near tactics. Both our work and the Procrastination library are a generalization of the bigenough library from previous work [START_REF] Cohen | Formalized algebraic numbers: construction and rstorder theory[END_REF], which only dealt with statements that are eventually true in N. The main dierence between Procrastination and the near tactics is the following. To prove a given goal using Procrastination, one can introduce variables and accumulate properties about them. Once the goal is proved, the user is asked to provide an actual value for these variables which satises every accumulated property. Our work is more centered on lters: we do not have to provide a witness of the satisability of a predicate, but only to prove that the accumulated predicates belong to a given lter. The implementation of Procrastination also have more tactics, which are more complex, while we try to minimize them, following the Small-Scale Reection strategy [START_REF] Mahboubi | Mathematical Components[END_REF].

A particular formalization of big-O to be mentioned is the one by Boldo et al. [BCF + 13]. Their uniform big-O can be expressed with our denition through the choice of the appropriate lter, as described in Sect. 4.6.

Finally, lters à la Hölzl, Immler and Human [START_REF] Hölzl | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL[END_REF], are also used in an ongoing formalization of classical analysis in Lean [START_REF]The Lean mathematical components library developers. Lean mathematical components library[END_REF].

CONCLUSION

In this work, we provide a set of techniques and notations (notations are summarized in Fig. 3) in order to make asymptotic reasoning as smooth as possible in Coq. We integrate a mechanism for lter inference into a hierarchy of mathematical structures [ACM + 18a], together with notations and denitions that make lter manipulation easier.

We dene tactics that make it possible to delay the instantiation of existential witnesses in order to allow for rigorous asymptotic hand-waving. These tactics are more generally designed to do lter elimination while avoiding forward reasoning.

We then take advantage of our new framework to design equational Bachmann-Landau notations and to develop a small theory of little-o and big-O that removes all explicit local reasoning from some proofs.

Future Work. We plan to build a full classical analysis library, with convergence criteria for innite sums or integrals based on asymptotic comparison, and also innite sums and integrals of little-o, big-O and equivalences. We plan in particular to experiment with the same kind of construction as the mklittleo function for upper bounds, limits, derivatives and dierentials.

Our strategy in this work is to provide a minimalistic set of tactics that makes it easier to build a small library in the tradition of the Mathematical Components library [G + 15]: our tactics are small-scale [START_REF] Mahboubi | Mathematical Components[END_REF] (they perform elementary steps, hence proofs are more stable) and we focus on proving a collection of Record mixin_of (K : absRingType) (V : lmodType K) loc (m : @Uniform.mixin_of V loc) := Mixin { norm : V -> R ; ax1 : forall (x y : V), norm (x + y) <= norm x + norm y ; ax2 : forall (l : K) (x : V), norm (l *: x) = abs l * norm x; ax3 : Uniform.ball m = ball_ norm; ax4 : forall x : V, norm x = 0 -> x = 0 }.

Record class_of (T : Type) := Class { base : GRing.Lmodule.class_of K T ; pointed_mixin : Pointed.point_of T ; locally_mixin : Filtered.locally_of T T ; topological_mixin : @Topological.mixin_of T locally_mixin ; uniform_mixin : @Uniform.mixin_of T locally_mixin; mixin : @mixin_of _ (@GRing.Lmodule.Pack K (Phant K) T base T) _ uniform_mixin }.

The type lmodType K is a structure with an addition operation and a scaling operation with coecients in K [START_REF] Gonthier | Point-free, set-free concrete linear algebra[END_REF]. A.2.5 landau.v and derive.v. These two les are original developments that strongly rely on the tools we described in this article. They contain numerous results about limits, continuity, and dierentiation presented using Bachmann-Landau notations and with proofs made shorter and more robust thanks to our contribution.

  supersets. Definition filter_from {I T : Type} (D : set I) (B : I -> set T) := [set P | exists2 i, D i & B i `<=`P].

First, it illustrates

  our main technical contributions: it uses all of our tactics and demonstrates our use of lters, in particular, this proof uses two lters on two dierent types. Second, it shortens the original proof in Coquelicot[START_REF] Boldo | The Coquelicot library[END_REF] Lemma complete_cauchy_fct, le Hierarchy.v] from about 40 lines to 7 lines (see Sect. 3.5 for a brief explanation of the dierences between the two proofs), by removing in particular the three explicit witnesses. Finally, it shows how our work leads to formal proofs that look like informal ones: arguments can be stated without being cluttered by technical constructions of witnesses (see line 5), the latter being delayed and constructed by resorting to lemma applications (see lines 56), which makes for shorter and more stable proof scripts. The proof script we explain below is part of the formalization accompanying this article [ACM + 18a, le hierarchy.v]. Lemma fun_complete (T : choiceType) (U : completeType) (F : set (set (T -> U))) {FF : ProperFilter F} : cauchy F -> cvg F. Proof.

  3.2: Context {T : Type} {K : absRingType} {V W : normedModType K}. Let littleo_def (F : set (set T)) (f : T -> V) (e : T -> W) := forall eps : R, 0 < eps -> \forall x \near F, `|[f x]| <= eps * `|[e x]|. Let bigO_def (F : set (set T)) (f : T -> V) (e : T -> W) := \forall k \near +oo, \forall x \near F, `|[f x]| <= k * `|[e x]|.Regarding notational conventions in the remaining of this article, note that, like in the code snippet just above, T is a type, K is a ring equipped with an absolute value, and V and W are normed modules over K; they all are implicit arguments of forthcoming denitions.The sigma-types littleo_type and bigO_type directly follow from the corre-spondingternary predicates: Structure littleo_type (F : set (set T)) (e : T -> W) := Littleo { littleo_fun :> T -> V; littleoP : littleo_def F littleo_fun e }. Structure bigO_type (F : set (set T)) (e : T -> W) := BigO { bigO_fun :> T -> V; bigOP : bigO_def F bigO_fun e }. For the sake of readability, we slightly simplied the denitions compared to the source code: we removed Prop to bool coercions and the littleoP and bigOP elds are lemmas deduced from unnamed elds in the actual code. The unaltered denitions can be found online [ACM + 18a, le landau.v]. Let us comment more specically on the structure littleo_type. It packs a function, namely the littleo_fun projection, with a proof that it is a little-o of e, providing us with the type of functions that are a little-o of another function. In particular, we can inhabit this type with the null function (and the trivial proof that it is a little-o). Let us call littleo0 this record with the null function. The type littleo_type F e is furthermore equipped with the notation {o_F e} to improve reading. So littleo_type and bigO_type provides a type-theoretic variant of the settheoretic notation for little-o and big-O, but it can be argued that such a settheoretic notation is misplaced because it precludes the equational viewpoint that Knuth advocates [Knu98], along with formal-proof practitioners, and even anachronistic now that today's students use symbolic algebra systems like Maple and Wol-framAlpha where the big-O notation appears in power series calculations.

4. 6

 6 Application: Uniform Big-O Boldo et al. designed a notion of uniform big-O in their work on the numerical resolution of the wave equation [BCF + 13]. They are interested in relations of the form f (x, ∆) = O ∆→0 (g (∆)) , axioms propositional_extensionality and functional_extensionality_dep from the Coq standard library.

  However, in the face of the diculties encountered to reproduce the (apparently sloppy) manipulation of the big-O notation, they give up on producing proofs as simple [...] as their paper counterparts, choose to formalize the big-O notation as a dominance relation, and deprive themselves of Coq equational reasoning ca-pabilities. Their library would require extension with the little-o notation and to arbitrary lters for it to have other applications in mathematics. In comparison, our work already provides both notations, retains equational reasoning, and already ts together with a hierarchy of mathematical structures [ACM + 18a] designed on the model of Mathematical Components [GGMR09, MT16].

  This structure was modied from Coquelicot by replacing the inequality in axiom ax2 by an equality. Complete Normed Modules. Finally, the structure completeNormedModType combines normedModType with completeType: Record class_of (T : Type) := Class { base : NormedModule.class_of K T ; mixin : Complete.axiom (Uniform.Pack base T) }.

  For example, they include the following results: eqolimP (in landau.v): a function f converges to a limit l if and only if f = l + o(1), linear_for_continuous (in landau.v): locally bounded linear functions are continuous, differentiable_continuous (in derive.v): dierentiable functions are continuous, is_diff_comp (in derive.v): the dierential of a composition is the composition of the dierentials, Rolle and MVT (in derive.v): Rolle's Theorem and the Mean Value Theorem.

  Notations from previous work used in this article a description might be useful for the reader to understand how our tools t in the bigger picture and to help her nd many examples of use.

	Standard Coq/Mathematical Components notations:
	exists2 x, P x & Q x existence of an x that satises both P and Q
	.1, .2	rst, second projection of a pair
	@^~x	application at x, i.e. fun f => f x
	{linear U -> V}	linear functions of type U -> V
	Denitions/notations from [CR17]:
	set A	A -> Prop
	A `<=`B	set inclusion
	[set a | P a]	the set of elements a that satisfy P
	F --> G	reverse set inclusion for lters F ⊇ G
	f @ F	lter f (F ), see Sect. 2.3
	+oo	+∞
	Fig. 1.

  Notations used in Sections 3 and 4 (see [ACM + 18a, le topology.v] for details): \forall x \near F, G x for all x near F, G x holds, i.e. F G where F is a lter over T and G : T -> Prop (a set over T) \forall x & y \near F, H x y (filter_prod F F)(fun x => H x.1 x.2) where F is a lter over T and H : T -> T -> Prop x \is_near F x is in a set that belongs to F little-o notations used in Sect. 4 (see [ACM + 18a, le landau.v] for details and big-O notations): {o_F e} the type littleo_type F e of little-o's of e [o_F e of f] a function with a canonical structure of little-o of e, f if it is indeed a little-o and the null function otherwise f = g +o_F e f = g + [o_F e of f -g] f =o_F e f is a little-o of e near F, i.e. f = (mklittleo F f e) [littleo of f] recovers the canonical structure of little-o of f 'o_F e printing of [o_F e of h] (h is hidden) 'a_o_F e printing of [o_F e of ?h] (?h is an existential variable) f ~_F g f and g asymptotic equivalence f x = g x +o_(x \near F) (e x) f x = g x + h x where h is the function hidden by the little-o of e Fig. 3. Summary of the new notations introduced in this article reusable lemmas that hides the most technical parts. Other strategies exist, see for example [Ebe17, GCP18] that we already discussed in Sect. 6.

Unless stated otherwise, the code snippets displayed in this section can be found in [ACM + 18a, le topology.v].

The formalization of uniformType and the formal denition of the entourage lter can be found in [ACM + 18a, le hierarchy.v] and in Appendix A.2.4

We have slightly simplied the presentation; the actual statement does not use directly the projection prop_in_filter_proj [ACM + 18a].

We display the actual proof script where fun f => f t is abbreviated @^~t using Mathematical Components notations.

Here again the denition is simplied by removing Prop to bool coercions and phantom types.

ACKNOWLEDGMENTS

We thank Assia Mahboubi for her feedback on Bachmann-Landau notations, Assia Mahboubi and Guillaume Melquiond for their feedback on the near tactics and Assia Mahboubi and Pierre-Yves Strub for designing a library for real numbers from which we drew inspiration. We are also grateful to Coquelicot authors Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond for their inspiring library and the many conversations we have had. We also thank Yves Bertot and Laurence Rideau for their feedback on the draft. Finally, we would like to thank anonymous reviewers who gave us many constructive comments which allowed to improve the presentation of our work. This work was partially funded by the ANR project FastRelax (ANR-14-CE25-0018-01) of the French National Agency for Research and by JSPS KAKENHI Grant Number 15H02687.

may need in order to combine them easily. Once suciently many equations are proved, that allows the user to prove facts about little-o and big-O using informal reasoning, without having to go back to the denition of little-o and big-O and to do explicit local reasoning, except in particular cases where the theory lacks an equation (see Sect. 4.4 for examples where the lter characterization of little-o is completely abstracted from the proof ).

We do not claim to have reached such a complete set of equations, but we proved a few equations that seemed important to us. Let us give examples. First, we have arithmetic rules for little-o and big-O. For instance, little-o absorbs addition and the product of a O(h 1 ) and a O(h 2 ) is a O(h 1 • h 2 ). Context {F : filter_on T}.

Lemma addo (f g : T -> V) (e : T -> W) :

[o_F e of f] + [o_F e of g] =o_F e.

Lemma mulO (h1 h2 f g : T -> R) :

[O_F h1 of f] * [O_F h2 of g] =O_F (h1 * h2).

We also have a few rules combining little-o and big-O. For example, a o(e) is also a O(e) and a little-o of a O(g) is a o(g). Lemma littleo_eqO (e : T -> W) (f : {o_F e}) :

(f : _ -> _) =O_F e.

Lemma littleo_bigO_eqo (g : T -> W) (f : T -> V) (h : T -> X) : f =O_F g -> [o_F f of h] =o_F g.

Of course, in order to prove this set of equations, local reasoning is necessary at some point. This is where the near tactics from Sect. 3.2 come into use. For instance, let us have a look at the proof of Lemma littleo_bigO_eqo 6 . The function f is a O(g) and the function [o_F f of h] is a o(f), either equal to h if it is a o(f), or to the null function (recall Sect. 4.2). Since the goal is to prove that the function [o_F f of h] is a o(g), the rst step is to go back to the denition of little-o and introduce the universally quantied epsilon. This is the application of lemma eqoP at line 1 that recovers the denition littleo seen in Sect. 4.1. 1 move->; apply/eqoP => _/posnumP[e]; have [k c] := bigO _ g.

In line 1, we also replaced f in [o_F f of h] with [O_F g of f]. We also abstract the latter function using a fresh function k and, since it was a big-O of g, we get as an hypothesis a positive constant c such that \forall x \near F, `

6 The proof script can be found in [ACM + 18a, le landau.v].

59

We use filter_app to combine both statement so that we should now prove \forall x \near F, `

Now we give ourselves an x which is near F thanks to the near=> x tactic.

apply: filter_app; near=> x.

We have to prove that

by manipulating the inequalities until we reach the goal

as the result of multiple rewritings and transitivity (see line 3).

rewrite -!ler_pdivr_mull //; apply: ler_trans; rewrite ler_pdivr_mull // mulrA.

The latter goal should be true for x which is near F since 'o_(x \near F) (k x) is a little-o of k and eps / c is positive.

To nish the proof, we can now call the near: x tactic. At this point, the remaining goal is by near: x; apply: littleoP.

The last line of the proof script calls the end_near tactic to dispose of the remaining existentials:

Grab Existential Variables. all: end_near. Qed.

Application: Asymptotic Equivalence

Two functions f (x) and g(x) are equivalent as x goes to a (notation: f ∼ a g) when f = g + o a (g). Thanks to the ideas explained in Sections 4.1 and 4.2 and to the equations already proved in Sect. 4.3, the fact that ∼ is an equivalence relation can be established by short proof scripts. For the sake of illustration, let us explain how we show that ∼ is symmetric and transitive (see [ACM + 18a, le landau.v] for details).

The symmetry of ∼ is mechanized as follows (f ~_F g is the Coq notation for f ∼ F g):

but with a uniform denition with respect to x, i.e. with the following denition:

We can formalize this uniform big-O as (fun p => f p) =O_F (fun p => g p.2) where p represents the pair (x, ∆) and p.2 is thus ∆ (recall Fig. 1), and with an appropriate choice for the lter F.

The lter F must be a lter on a Cartesian product and can be dened using the lter product function filter_prod (see Sect. 2.1). Its rst argument is the lter corresponding to x. Since there is no constraint on x, we can choose the trivial lter containing only the total set. The second argument, corresponding to ∆, is the neighborhood lter of 0 (i.e. locally 0).

In fact, in their source code, Boldo et al. force ∆ to be within a particular domain and use sigma types instead of the existential quantier. We can still provide an equivalent denition thanks to a restriction operator on lters and prove that it is indeed equivalent to their denition thanks to the axioms from Sect. 5. The interested reader may refer to the source code for more details [ACM + 18a, le misc/uniform_bigO.v].

COQ AXIOMS TO MAKE CLASSICAL ANALYSIS PRACTICAL

The formal tools we have explained so far have been developed with classical analysis in mind. However, the native logic of Coq (the Calculus of Inductive Constructions) is constructive. Fortunately, there exist several axioms that can be safely added. In this section, we explained the axioms on which our development relies. In short, they bring to the logic of Coq: extensionality, the law of excluded middle, and the axiom of choice. These are arguably much-needed axioms for classical analysis and it is therefore no wonder that they are important to make the Mathematical Components Analysis library practical. In the following, we explain how they are used in the tools we described in this article. For the sake of presentation, we divide our four axioms into two categories: the extensionality axioms and the classical axioms.

Extensionality Axioms

The rst two axioms on which our development relies are extensionality axioms:

propext: forall (P Q : Prop), Section A.1 is about the rst part of the library (boolp.v, reals.v, Rstruct.v, Rbar.v, forms.v). This part is based on previous work or work-in-progress . We do not enter into details and mostly refer to available resources when they exist (e.g. the documentation embedded in the Coq les, publications by their authors, historical information), or provide explanations otherwise. Section A.2 depicts the second part of the library (posnum.v, classical_sets.v, topology.v, hierarchy.v, landau.v, and derive.v). This part was introduced by the authors of the current article to have a ground to develop and test the asymptotic tools. We provide more details for that part. In particular, topology.v and hierarchy.v are based on previous work but required substantial adjustments which are described in Sections 2.1 and 2.2; we provide here more technical details at the risk of being redundant with existing literature. This le reals.v provides a classical axiomatization of real numbers, as a discrete real archimedean eld with a least upper bound operator, which we use in a noncritical way as an abstraction of the reals from the Coq standard library. This axiomatic has been indeed instantiated in le Rstruct.v (see below), but there are some plans to provide a model solely based on axioms from boolp.v. We did not modify the les altreals/*.v. They were written before the existence of the Mathematical Components Analysis library, and are thus independent from all of the les below. They are waiting to be ported to the new framework, and we expect their rewriting will benet greatly from the present work.

A.1 Library Files Based on Previous Work

A.1.2

Rbar.v and Rstruct.v. Both les deal with the reals of the Coq standard library.

The le Rbar.v originally comes from the Coquelicot library [START_REF] Boldo | The Coquelicot library[END_REF] and has been mostly rewritten using posnum.v.

To the best of our knowledge, the le Rstruct.v has been rst released in the and for dot products on nite dimensional vector spaces.

A.2 Library Files Introduced with this Article

The les introduced with this article provide in particular several interfaces corresponding to mathematical structures. These interfaces come as extensions of existing Mathematical Components interfaces. The methodology for extension is the one of packed classes [START_REF] Garillot | Packaging mathematical structures[END_REF]. Below, when it comes to interfaces, we present only the mixin and the class.

A.2.1 posnum.v. This le provides small-scale automation to rule out proofs of positivity for ε's. Its use is illustrated in Line 7 of the proof script of Lemma fun_complete in Sect. 3.4. We use canonical structures as an inference mechanism [START_REF] Mahboubi | Canonical Structures for the Working Coq User[END_REF].

A.2.2 classical_sets.v. This le develops a theory of sets represented by a predicate over a type (the type set) with Mathematical Components-like notations (indeed, Mathematical Components only provides nite sets). Some of these notations can be seen in Fig. 1. This is inspired by previous work by Cyril Pointed types sit at the bottom of the Mathematical Components Analysis hierarchy, as described in Sect. 2.2.

The formalization of Zorn's lemma by Daniel Schepler [START_REF] Schepler | coq-zorns-lemma: Naive set theory library for Coq[END_REF] Types with Canonical Filters. The type filteredType U extends pointed types with an operator locally such that for any t of type filteredType U, the object locally t is a set of sets around t over the type U. In subsequent structures, this will be identied with the lter of neighborhoods of t. Given a T of type topologicalType, for any t of type T, the set of sets locally t is now the proper lter of neighborhoods of t (see Sect. 2.1). Indeed, it is dened using the lter base of the open's of t.

The proof of Tychono 's Theorem by Daniel Schepler [START_REF] Schepler | coq-topology: Topology library for Coq[END_REF] has been ported to this setting.

The le topology.v also contains the near notations and tactics explained in