Olivier Huber
email: olivier.huber@inria.fr

Vincent Acary
email: vincent.acary@inria.fr

Bernard Brogliato
email: bernard.brogliato@inria.fr

Enhanced matching perturbation attenuation with discrete-time implementations of sliding-mode controllers

Continuous-time Sliding Mode Control yields when embedded into Filippov's mathematical framework, closed-loop systems with a set-valued controller, represented by differential inclusions. In particular, besides finite-time convergence to the sliding surface and robustness to matched disturbances, such controllers allow an exact compensation of the disturbance on the sliding manifold. In other words, the set-valued input is the exact copy of minus the perturbation. A novel discretization methodology has been recently introduced by the authors, which is based on an implicit discretization of the Filippov's differential inclusion, which in theory totally suppresses the chattering due to the discretization (numerical chattering). In this work we propose an extension of the implicit method, enhancing the perturbation attenuation (in terms of chattering) by using previous values of the set-valued input. This allows to estimate on-line the unknown perturbation, with a time delay due to the sampling. Simulation results illustrate the effectiveness of the method.

I. INTRODUCTION

The time discretization of sliding-mode controllers has witnessed an intense activity in the past 30 years [START_REF] Sarpturk | On the stability of discrete-time sliding mode control systems[END_REF], [START_REF] Drakunov | On discrete-time sliding modes[END_REF], [START_REF] Furuta | Sliding mode control of a discrete system[END_REF], [START_REF] Utkin | Sliding mode control in discrete-time and difference systems[END_REF], [START_REF] Gao | Discrete-time variable structure control systems[END_REF], [START_REF] Golo | Robust discrete-time chattering free sliding mode control[END_REF] and [START_REF] Milosavljević | General conditions for the existence of a quasisliding mode on the switching hyperplane in discrete variable structure systems[END_REF]. This concerns in particular the classical Equivalent-Control-Based Sliding-Mode Control (ECB-SMC), which consists of two sub-controllers: the state-continuous equivalent control u eq and the statediscontinuous control u s . The chattering phenomenon is seen as a limiting factor to a more widespread deployment of SMC. In this note, from the different sources of chattering, we shall consider the one originating from the discretization of the controller and the matching perturbations. In these past research efforts, most of the focus was on the discontinuous part of the control, since it introduces numerical chattering. In previous works [START_REF] Acary | Implicit Euler numerical scheme and chattering-free implementation of sliding mode systems[END_REF], [START_REF] Acary | Chattering-free digital slidingmode control with state observer and disturbance rejection[END_REF] and [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], a new kind of discretetime controller was proposed. The basic idea is to implement the discontinuous input u s in an implicit form, while keeping its causality (i.e. the controller is nonanticipative). Then this input has to be computed at each sampling time as the solution to a generalized, set-valued equation, which takes the form of a simple projection on an interval in the simplest cases. The other source of chattering considered here is the perturbations that comprise noise, unmodeled dynamics, and unknown inputs. One of the features of continuoustime sliding-mode control is the disturbance rejection of matched perturbations [START_REF] Drazenovic | The invariance conditions in variable structure systems[END_REF]. However this nice property is not preserved through discretization. Efforts aiming at improving the accuracy with discrete-time controllers include the works in [START_REF] Mitic | Sliding mode-based minimum variance and generalized minimum variance controls with O(T 2 ) and O(T 3 ) accuracy[END_REF] and [START_REF] Su | An O(T 2 ) boundary layer in sliding mode for sampled-data systems[END_REF]. In the latter, a constant prediction of the perturbation was used to improve a deadbeat controller. The work in [START_REF] Ljesnjanin | Disturbance compensation in digital sliding mode[END_REF], unknown to the authors at the time of writing, shares some similarities with the present one. Other work like the ones cited at the beginning aim at reducing the chattering in general, which includes the numerical one. The specificity of the approach in [START_REF] Mitic | Sliding mode-based minimum variance and generalized minimum variance controls with O(T 2 ) and O(T 3 ) accuracy[END_REF], [START_REF] Su | An O(T 2 ) boundary layer in sliding mode for sampled-data systems[END_REF], [START_REF] Ljesnjanin | Disturbance compensation in digital sliding mode[END_REF] and the present work is to have a dedicated treatment for the chattering not originating from the discretization.

In this work, we present a modified controller based on the one found in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], that takes advantage of the previous measured values. Indeed, in this previous work, the convergence of the discretized discontinuous input to the perturbation as the sampling time goes to 0 was studied. This motivates us to use this information in order to improve the attenuation, using finite difference methods to exploit the past informations. After presenting the basic idea, we introduce finite difference formulaeand how they can be used to derive prediction of contribution of the perturbation. We also investigate stability and finite-time convergence of the modified controller.

The type of system under study is of the form

         ẋ(t) = Ax(t) + Bu(t) + Bξ(t), u(t) := u eq (t) + u s (t) + u p (t), σ(t) := Cx(t), u s (t) ∈ -α Sgn (σ(x(t))) , (1)
with

x(t) ∈ R n , u(t) ∈ R p , σ(t) ∈ R p , C ∈ R p×n , and α > 0.
The function σ is called the sliding variable and the disturbance is denoted as ξ. As one can infer from the dynamics in [START_REF] Sarpturk | On the stability of discrete-time sliding mode control systems[END_REF], in this note only matched perturbations are considered. Furthermore we restrict ourselves to the case where ξ is smooth, with no noise component in it. Let us denote by u p the new control input, designed to cancel the effect of the perturbation. The method used to discretize the dynamics is called Zero-Order Hold (ZOH).

In the remainder of this section, we introduce the notation. In Section II we briefly recall the discrete-time sliding mode controller introduced in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF]. The basic idea is exposed in Section III and the proposed estimation scheme is presented in Section IV. Section V presents the implementation details of the controller. Simulation results using different timediscretization methods are shown in Section VI, to illustrate the different predictions. Finally, stability results are derived in Section VII. Conclusions end the paper in Section VIII.

Notations: Let x : R + ×R p ×R n → R n be the solution of system (1), x := x( • , u, x 0 ) is the solution associated with a continuous-time control u and an initial state x 0 ∈ R n , while x := x( • , ū, x 0 ) is the solution with a step function ū and the same initial state. In the latter case, we denote by σ := C x the sliding variable. The control values change at predefined time instants t k , defined for all k ∈ N : t k := t 0 + kh, t 0 , h ∈ R + . The scalar h is the sampling period. We denote xk := x(t k ) and σk := σ(t k ) for all k ∈ N. Let

• be the usual Euclidean norm.

Definition 1 (Multivalued sign function). Let x ∈ R. The multivalued sign function Sgn : R ⇒ R is defined as:

Sgn(x) =      1 x > 0 -1 x < 0 [-1, 1] x = 0. (2)
If x ∈ R n , then the multivalued sign function Sgn : R n ⇒ R n is defined as: for all j = 1, . . . , n, (Sgn(x)) j := Sgn(x j ).

Definition 2. Let f : R n × R → R p and l ∈ R. One has f = O(h l ) if for all x ∈ R n , there exists c ∈ R p such that f (x, h)/h l → c as h → 0.
Definition 3 (Discrete-time sliding phase [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF]). A system [START_REF] Sarpturk | On the stability of discrete-time sliding mode control systems[END_REF], in its sampled-data form, is in the discrete-time phase if ūs takes values in (-α, α) p , with α the gain of the controller.

II. DISCRETE-TIME CONTROLLER

We consider ūeq , ūs and ūp to be right-continuous step functions, with for instance ūs (t) = ūs k if t ∈ [t k , t k+1 ). Following previous works in [START_REF] Acary | Implicit Euler numerical scheme and chattering-free implementation of sliding mode systems[END_REF], [START_REF] Acary | Chattering-free digital slidingmode control with state observer and disturbance rejection[END_REF], [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], ūeq is designed directly in discrete-time and ūs is obtained by an implicit discretization of the Sgn multifunction. Integrating the nominal (that is ξ ≡ 0) version of system (1) over [t k , t k+1 ), we get the ZOH discretization of the system:

xk+1 = e Ah xk + B * ūeq k + B * ūs k + B * ūp k , (3)
with

B * := t k+1 t k e A(t k+1 -τ ) Bdτ. (4)
The control inputs are computed as follows: the equivalent part ūeq is given by the relation

CB * ūeq k = C(I -e Ah )x k , (5)
and with the implicit discretization, for each k ∈ N, ūs k is the solution to the generalized equation

σ k+1 = σk + CB * ūs k ūs k ∈ -α Sgn( σ k+1 ). (6)
The computation of the input ūp is described in the next section. If we set u p ≡ 0, the closed-loop system (1) is the one studied in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], and exhibits properties as finitetime duration of the reaching phase and convergence of the discretized discontinuous input ūs to the continuous-time one u s . In Section VII, we shall investigate when those properties are also shared by our modified controller.

III. PROBLEM STATEMENT In continuous time, while in the sliding phase, the discontinuous control input u s takes values to reject the perturbation action, according to Filippov's concept of solutions. Let us illustrate this using an academic example, ẋ(t) ∈ -Sgn(x) + d(t), x scalar and d a continuous unknown perturbation, with |d(t)| ≤ 1 for all t. In the sliding phase, the value taken by Sgn(x(t)) is d(t). In [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], it was established that in the discrete-time sliding phase the input ūs is approximating the opposite of contribution of the perturbation in the evolution of the sliding variable. But this action is a posteriori, in the sense that at time t k , ūs corrects for the contribution of the perturbation over the time interval

[t k-1 , t k ].
Hence the attenuation of the perturbation is limited since the control is lagging by one sampling period.

Our approach to enhance the perturbation attenuation consists in using the past values of the sliding variable in order to predict the contribution of the perturbation on the next time interval. Then we take into account this prediction in the control input that is going to be applied for this time interval. As we shall see, this additional control input is computed independently of the other ones.

Let us study the dynamics of the ZOH-discretized discretetime system with a nonzero perturbation. We suppose the system has been in the discrete-time sliding phase for more than 1 sampling period. Adding the perturbation term to (3), we get

xk+1 = e Ah xk + B * ūeq k + B * ūs k + B * ūp k + p k (7)
and with ūeq k as in [START_REF] Gao | Discrete-time variable structure control systems[END_REF], the sliding variable dynamics is

σk+1 = σk + CB * (ū s k + ūp k ) + Cp k , (8)
with

p k := t k+1 t k e A(t k+1 -τ ) Bξ(τ )dτ. (9)
We refer to p k or Cp k as the effect, or contribution, of the perturbation. From ( 6), in the discrete-time sliding phase σ k+1 = 0, so σk + CB * ūs k = 0. Therefore the relation (8

) becomes σk+1 = Cp k + CB * ūp k . ( 10
)
If we have an estimate Cp k of Cp k at the time t k , then we can use this information in the control input u p , defined as

ūp k := -(CB * ) -1 Cp k . ( 11
)
Then injecting [START_REF] Drazenovic | The invariance conditions in variable structure systems[END_REF] in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], we get:

σk+1 = Cp k -Cp k =: C p. (12)
In the rest of this note, we name the quantity denoted by C p the residual perturbation. The chattering on the output σ is equal to the prediction error on the effect of the perturbation. Therefore to reduce the chattering imputable to perturbations like unmodeled dynamics, we can try to find a good prediction of the value of the perturbation. The better it is, the smaller the chattering will be. In the next section, we build an estimate Cp k of Cp k at the time t k .

IV. PREDICTION OF THE PERTURBATION

The method we propose to make use of is finite difference, itself based on the Taylor expansion of a function. For instance if we suppose that a function f : R → R n is twice differentiable, it holds that

f (x + h) = f (x) + h ḟ (x) + h 2 2 f (x) + O(h 3 ). ( 13
)
To use this recurrence formula for the prediction at the next time instant, one need to estimate the values of the first and second derivatives of the function. We use again the finite difference method to get them. We suppose we have access to Cp k for the previous r sampling periods. However Cp(t) is not a continuous function. It is piecewise smooth, but only right-continuous. From the definition in ( 9), we have Cp(t + k ) = 0 for all k ∈ N. This prevents us from directly applying the Taylor expansion to Cp(t) itself. Nonetheless, we can use the Taylor expansion formula on the perturbation ξ and then derive the one for the prediction of Cp k . Let us illustrate this using a second order expansion of ξ:

ξ(τ + h) = ξ(h) + h ξ(τ ) + h 2 2 ξ(τ ) + O(h 3 ). ( 14
)
Multiplying by e A(t k -τ ) and integrating, we get:

t k t k-1 e A(t k -τ ) Bξ(τ + h)dτ = t k t k-1 e A(t k -τ ) Bξ(τ )dτ + (15)
h

t k t k-1 e A(t k -τ ) B ξ(τ )dτ + h 2 2 t k t k-1 e A(t k+1 -τ ) B ξ(τ )dτ + O(h 4 ). (16)
Using the change of variable τ = τ + h in the left-hand side of (16) and using [START_REF] Acary | Chattering-free digital slidingmode control with state observer and disturbance rejection[END_REF], we obtain the relation

Cp k = Cp k-1 + hC t k t k-1 e A(t k -τ ) B ξ(τ )dτ (17)
+ h 2 2 C t k t k-1 e A(t k -τ ) B ξ(τ )dτ + O(h 4 ). (18)
Let us define Cp

(i) k := C t k t k-1 e A(t k -τ ) ξ (i) (τ )dτ .
We use the finite difference method to estimate the second and third terms in (18). Lemma 1. Suppose we have an r-step approximation of the i-th derivative of ξ, ξ (i) (τ ) = r l=0 α l ξ(τ -lh)+O(h r-i+1 ) with r ≥ i. Then the approximation formula for Cp

(i) k is r l=0 α l Cp k-l and is of order O(h r-i+2 ).
Proof. Starting from the approximation relation for the derivative and with basic operations, we get:

C t k+1 t k e A(t k+1 -τ ) Bξ (i) (τ )dτ = (19) r l=0 α l C t k+1 t k e A(t k+1 -τ ) Bξ(τ -lh)dτ + O(h r-i+2 ). (20)
For each integral, we use the change of variable τ = τ -lh.

C

t k+1 t k e A(t k+1 -τ ) Bξ (i) (τ ) = (21) r l=0 α l C t k+1-l t k-l e A(t k+1-l -τ ) Bξ(τ )dτ + O(h r-i+2 ) (22) = r l=0 α l Cp k-l + O(h r-i+2 ). (23)
Using Lemma 1 for the approximate value of the first and second derivatives in (18) yields:

Cp k ≈ Cp k-1 + h r1 l=0 α l Cp k-l + h 2 2 r2 l=0 α l Cp k-l . ( 24
)
where r 1 and r 2 (both ≤ r) are the order for the prediction of the first and second derivative. Those, with the coefficients α l and α l , are taken from [START_REF] Fornberg | Generation of finite difference formulas on arbitrarily spaced grids[END_REF]. As Equation (24) illustrates it, the i-th derivative estimate is multiply by h i . By Lemma 1 we know that the approximation error for the i-th derivative is of order O(h r-i+2 ). Then the approximation error introduced by the i-th derivative is of order O(h r+2 ).

Let us present some possible prediction formulae. Using only the first derivative, we have the relation

Cp k = 2Cp k-1 -Cp k-2 + O(h 3 ) (25) = Cp k + O(h 3 ), (26)
where both the approximation of the first derivative and the prediction have the same order. Adding the second derivative yields

Cp k = 5 2 Cp k-1 -2Cp k-2 + 1 2 Cp k-3 + O(h 3 ) (27) = Cp k + O(h 3 ). ( 28
)
The order is the same as in (26) since we use a 1-step approximation for Cp

k , of order 1 which introduces an error of order O(h 3 ) in (28). Therefore to achieve an overall error of order O(h 4 ), we need an estimate with an order 2 for Cp

(1) k , yielding Cp k = 3Cp k-1 -3Cp k-2 + Cp k-3 + O(h 4 ) (29) = Cp k + O(h 4 ). (30)
From now on, let us refer to (26) as a linear or order 1 prediction and to (28) as an order 2 prediction. Both predictions are said to be high-order in contrast with the one given by the relation

Cp k = Cp k-1 , (31)
which is said to be constant. Note that the order of the prediction indicates also the number of times the perturbation has to be differentiable for the approximation order to be guaranteed.

V. CONTROLLER IMPLEMENTATION Let p ∈ N be the approximation order. As long as the closed-loop system is not in the discrete-time sliding phase, we set ūp ≡ 0. Let k 0 ∈ N be such that σ k0 = 0, that is the system is in the discrete-time sliding phase, and let k > k 0 . For k 0 ≤ k < k 0 + p, we let ūp k = 0 and we save σk , which is Cp k-1 according to [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF]. For k ≥ p + k 0 , we compute the prediction of the perturbation Cp k using one of the formula in (26), (30) or (31) and we set ūp k = (CB) -1 Cp k . At this point, we cannot know Cp k-1 directly from σk since ūp k changes the dynamics. From [START_REF] Mitic | Sliding mode-based minimum variance and generalized minimum variance controls with O(T 2 ) and O(T 3 ) accuracy[END_REF], at time t k , Cp k-1 is obtained through the relation

Cp k-1 = σk + Cp k-1 , ( 32
)
where σk is measured and Cp k-1 is known from the last estimation.

In [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], the condition Cp k ≤ αβ for all k, with β the smallest eigenvalue of CB * s := (CB+(CB * ) T )/2, was used to guarantee a finite-time reaching phase and that the system does not exit the discrete-time sliding phase. This inequality condition Cp k < αβ gives us a "feasibility set" for the prediction Cp k . If Cp k > αβ, then we project the estimate onto the ball of radius αβ centered at the origin. With this refinement of our algorithm, we make a first step towards some stability property, which is studied in Section VII.

VI. NUMERICAL EXAMPLE

We illustrate the method on a simple 2 dimensional system, taken from [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF]:

     ẋ(t) = Ax(t) + B ū(t) + Bξ(t) σ = Cx ū(t) = ūeq (t) + ūs (t) A = 0 1 19 -2 , B = 0 1 , C T = 1 1 .
(33) The perturbation ξ is a simple sinusoid: ξ(t) = sin(4πt). It was chosen as an example of unmodeled dynamics in a mechanical system. The matrix A has the eigenvalues λ 1 = 3.47 and λ 2 = -5.47. The dynamics on the sliding surface is given by 0 1 0 -1 , which has eigenvalues 0 and -1. The initial state is (-15, 20) T and the sampling period is 10 -2 s. We have simulated with 4 different controllers: the classical implicit one, one with the assumption that the perturbation is constant (31), one with the prediction presented in ( 26) and the last one with the prediction formula in (30). The simulations run for 150 s and were carried out with the SICONOS software package [START_REF] Acary | An introduction to SICONOS[END_REF] 1 . Figures were created using Matplotlib [START_REF] Hunter | Matplotlib: a 2D graphics environment[END_REF]. We present plots of the state variables in Fig. 1, 2 and 3. Then we display the evolution of the discontinuous control ūs in Fig. 4 and5.

In Fig. 1, the state values for the last second are displayed, when each system features some kind of steady-state behaviour. The improvement obtained using the prediction is clearly visible, to the point that we need to zoom to see the chattering with higher-order estimations. In Fig. 2, Fig. 1, only the trajectories of the closed-loop systems with prediction are displayed. The behaviour between sampling times can be seen with the constant prediction (order 0). Each high-order predictions (order 1 and 2), yields a closedloop system featuring even less chattering, as we can see in Fig. 3. At this level of detail, the difference between the Fig. 3: Detail of Fig. 2, with only the trajectories of the closed-loop system with higher-order prediction visible.

two estimations with high-order becomes visible. Markers indicate the state of the system at each time instant t k , that is when the control values change. We witness that for those particular values, the prediction with order 2 yields better results with a chattering one order of magnitude smaller. However with the small contribution of the residual perturbation, the inter-sampling dynamics provides an important contribution to the behaviour of the system. For the present example, the advantages of using a prediction order higher than 1 are not so striking as the ones from using at least a linear prediction. Therefore it is important to take into account the inter-sampling dynamics when designing the prediction of the perturbation. Let us turn our attention to the control input. Firstly we plot the evolution of the discontinuous part ūs , which is, up to a constant, equal to the residual perturbation [START_REF] Mitic | Sliding mode-based minimum variance and generalized minimum variance controls with O(T 2 ) and O(T 3 ) accuracy[END_REF]. In Fig. 4, the evolution of ūs for the last 2s is displayed. As expected, the better the approximation, the smaller ūs is. In Fig. 6: Evolution of ūp for simulations of system (33) displayed in Fig. 6. From a previous study in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF], we know that with no perturbation prediction, ūs approximates the perturbation with a delay of h. Recall that with an order 0, the predicted value of the effect of the perturbation is the one the system just measured. In this case, the values taken by ūp are the ones that ūs would take with no perturbation prediction. What we can witness from Fig. 6 and 7 is that with a highorder prediction, this lag of one sampling period h seems to have vanished. This is easier to assess on Fig. 7, where if we shift the solid green curve (corresponding with the constant prediction) by -h on the time axis, then it would more or less overlap with the two other curves. This observation can also be explained in the following way: with an estimation of order 0, there is no use of a derivative of ξ to "look into the future". When this is the case, as for the order 1 and 2, the main difference between the different predictions is the value that ūp k takes. This highlights the fact that using high-order estimation yields a prediction, hence a chattering attenuation, substantially better than a constant one. A last interesting comparison is the control effort used in each of these closed-loop systems. In particular, we want to compare the sum ūs + ūp with the discontinuous input ūs in the case where u p ≡ 0. In Fig. 8, one can see that all the control inputs are quite close, in terms of shape and value. At this level of detail, there is no difference between the closed-loop system with prediction. The main difference is that without prediction, the control is shifted by h with respect to the one with a prediction. Adding a perturbation prediction yields no extra control effort in this example.

VII. STABILITY PROPERTIES

One natural question arising from this prediction procedure is whether the use of a bad prediction can degrade the closed-loop performances instead of improving them. Sliding Mode Control is known for its robustness and such a feature should not be lost while trying to reduce the chattering.

First we characterize the robustness with a discrete-time feedback loop. Since we use an implicit discretization of the discontinuous control u s , we can divide the evolution of the closed-loop system in two phases: the reaching phase, were ūs has at least one of its element taking the maximum value ±α and the discrete-time sliding phase from Definition 3. We define the robustness as the feature that the system does not leave the discrete-time sliding phase, once it enters it. Proposition 1. Suppose that CB * s is positive-definite and β > 0 is its smallest eigenvalue. Let the estimate Cp k be obtained by the mean of one of the formula in Section IV. If α > 0 is such that for all k ∈ N, 2 Cp k < αβ and Cp k is projected onto the admissible set {v ∈ R p : v < αβ}, then the perturbed closed-loop system given by ( 8) and (6) enters the discrete-time sliding phase in finite time and stays in it.

Proof. The proof is similar to one in [START_REF] Huber | Analysis of explicit and implicit discrete-time equivalent-control based sliding mode controllers[END_REF] and is therefore omitted on brevity ground.

The closed-loop system does not exit the discrete-time sliding surface, even if the estimate is quite far from the actual value. In the worst case the magnitude of the chattering is doubled. The only change change required by the prediction is to double the bound on the discontinuous control input ūs . This is possible without degrading the performance with the implicit discretization of u s , since the numerical chattering is non-existent with a LTI system discretized using ZOH.

Remark 1. If it is not possible to double the bound α, it is possible to project the estimate onto a ball with a smaller radius γαβ, where (1 + γ)α is less than the componentwise upper bound on the control input. It is then easy to adapt the previous proposition to have a result with this estimate. However the chattering reduction might be less appealing.

VIII. CONCLUSION

In this note, a modified discrete-time sliding mode controller is proposed, which can improved the perturbation attenuation of smooth perturbations. The core idea is to use the previous values of the sliding variable to provide an estimate of the effect of the perturbation on the system for the next sampling period. The method proposed here is adapted from finite-difference formulae. Numerical simulations obtained with the INRIA software package SICONOS, illustrate the effectiveness of the proposed method. Stability properties of the new controller are also discussed. Experimental comparisons between discrete-time controllers are currently conducted and are about to be submitted for publication. They illustrate that the implicit discretization allows to drastically reduce the output and the input chattering effects, as well as the input magnitude (contrarily to explicit discretizations which invariably lead to bang-bang like controllers with full switching at very high frequency). Further works will include carrying on experimental comparisons as well as dealing with perturbation having a noise component, and also studying the convergence of the proposed controller as h → 0.

detail of 1 Fig. 1 : 2 Fig. 2 :

 1122 Fig. 1: Simulations of system (33), zoomed around the origin, with h = 10 -2 s.

Fig. 4 :

 4 Fig.4: Evolution of ūs for simulations of system (33) with h = 10 -2 s.

Fig. 5 :Fig. 5 ,

 55 Fig. 5: Detail of Fig. 4.

Fig. 7 :Fig. 8 :

 78 Fig. 7: Detail of Fig. 6.

The authors acknowledge the support of the ANR grant CHASLIM (ANR-11-BS03-0007).


Nicolas Magaud
email: magaud@unistra.fr

Agathe Chollet
email: achollet01@univ-lr.fr

Laurent Fuchs
email: laurent.fuchs@sic.univ-poitiers.fr.

Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective

This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb [16], the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field [31]. The formalization is based on the work presented in [8,7] where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges [4]. Laugwitz-Schmieden numbers [20] are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investi- gated [7]. In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.

Introduction

Dealing with geometric problems (geometric constraints solving, geometric modeling) people are, finally, faced with computations that involve computer representation of real numbers. Due to their important impact, the studies about real numbers in computer science are numerous and our purpose is not to surpass them but to reactivate an effective point of view that has been forgotten for a while [START_REF] Reveillès | Back and forth between continuous and discrete for the working computer scientist[END_REF].

This point of view was built in the eighties by J. Harthong and G. Reeb [START_REF] Harthong | Une théorie du continu[END_REF] and consists in a model of the continuum based over the integers that is the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field [START_REF] Reveillès | Back and forth between continuous and discrete for the working computer scientist[END_REF]. And, at that time, the constructive content of this model was neglected even though it was explicitly noted in Diener and Reeb's book [START_REF] Diener | Analyse Non Standard[END_REF]. As the Harthong-Reeb line is at the origin of the development of numerous and significant results on discrete straight lines and discrete circles, we hope that the present work will improve the confidence we can have in theoretical results and algorithms in the discrete analytical geometry field. Moreover, the Harthong-Reeb line based on Ω-integers opens the possibility to study the properties of multiscale objects in discrete analytical geometry. So our formalization can also be a support for those studies.

In previous works [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF] it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges [START_REF] Bridges | Constructive mathematics: A foundation for computable analysis[END_REF]. However, the Harthong-Reeb line construction is based on a nonstandard arithmetic of the integers that was not explicitly built. To be short, starting with the naive integer sequence (the one that you can enumerate: 1, 2, . . .), G. Reeb argues that there must exist an integer ω that is greater than all naive integers. Using the compactness theorem4 from model theory [START_REF] Huth | Logic in Computer Science[END_REF], the existence of this nonstandard integer ω is sufficient to deduce that there exists a nonstandard model of integer arithmetic with such nonstandard integer ω and then this model can be used to build the Harthong-Reeb line.

Nevertheless, this nonstandard model of integer arithmetic is not built and, in order to be put on computers, the Harthong-Reeb line needs a constructive nonstandard model of integer arithmetic. Such a construction, based on the Ωnumbers of Laugwitz and Schmieden [START_REF] Laugwitz | Leibniz' principle and Ω-calculus[END_REF], was made by some of the authors with others in [START_REF] Chollet | Ω-Arithmetization: a Discrete Multi-resolution Representation of Real Functions[END_REF][START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF].

This work presents a formalization of the Harthong-Reeb line using the Coq proof assistant. It can be seen as a light counterpart of the seminal works about the formalization of exact arithmetic [START_REF] Geuvers | Constructive analysis, types and exact real numbers[END_REF][START_REF] O'connor | Certified Exact Transcendental Real Number Computation in Coq[END_REF][START_REF] Krebbers | Type Classes for Efficient Exact Real Arithmetic in Coq[END_REF]. Our motivations to do this work come from the difficulties that we faced when showing that the Harthong-Reeb line satisfies the axioms proposed by Bridges [START_REF] Bridges | Constructive mathematics: A foundation for computable analysis[END_REF]. Unless proofs have been read carefully we have no way to be sure that they were entirely correct. This confidence problem of proofs is mainly due to the unusual mathematics that we deal with. The arithmetic dealt with is in a nonstandard framework and the axioms are in a constructive framework. So, it was not clear that handwritten proofs did not contain subtle mistakes or imprecisions. Moreover, the formalization has entailed a better understanding of how concepts and proofs are related to one another.

From a more practical point of view, the Harthong-Reeb line provides a rich theoretical framework that allows us to analyze a wide range of geometrical objects. So, our formalization can also be thought as a computable model for geometric computations. One main advantage of such model is that computing with these algorithms and reasoning about them (e.g. to prove that they are correct) can be done in the same framework. And we hope that this will help developing geometric systems where computations are made using the Harthong-Reeb line. This is possible, as shown in this paper, because the Coq proof assistant [START_REF] Barneva | The Coq Proof Assistant Reference Manual[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions[END_REF] implements a higher order constructive logic and is also a programming language equipped with inductive definitions and recursive functions. Therefore, it is the perfect tool to carry out a constructive formalization.

Let us summarize our overall strategy and expectations: we aim at describing in Coq the Harthong-Reeb line, in a way which allows us to compute continuous functions as well as to prove its properties formally. We adopt the point of view of Bridges in [START_REF] Bridges | Constructive mathematics: A foundation for computable analysis[END_REF][START_REF] Bridges | Constructive Mathematics. The Stanford Encyclopedia of Philosophy[END_REF] where constructive mathematics are those which use intuitionistic logic only. To build the Harthong-Reeb line, we first consider an abstract (axiomatic) representation of nonstandard integers. We prove that the Harthong-Reeb line built on top of it actually verifies the axioms of Bridges for being a constructive real line. Then we try and find an actual model of these nonstandard integers, and focus on Laugwitz-Schmieden integers. Although this implementation does not allow us to prove that all axioms of Bridges hold (we can only build an alternative version of the continuum and some of Bridges' axioms need to be slightly modified), it provides us with a framework in which one can compute continuous functions and it opens some interesting perspectives for multiscale representation of more complex geometric objects (circles, etc.).

This paper is organized as follows. In section 2, we discuss related work. In section 3, we formally describe in Coq5 what a nonstandard model of arithmetic should be. In Section 4, we build the Harthong-Reeb line HR ω on top of it and prove that HR ω verifies Bridges' Axioms which capture what a constructive real line is. In Section 5, we investigate how the Ω-numbers of Laugwitz and Schmieden can be an adequate model of the nonstandard arithmetic we consider and show that we can compute continuous fonctions using Euler's arithmetization scheme. Finally, in Section 6, we discuss our results as well as future work.

Related Work

We first reported on our experiments with formalizing the Harthong-Reeb line in Coq at the ADG'2010 workshop [START_REF] Magaud | Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective[END_REF]. It led to an alternative formalization in Isabelle/HOL [START_REF] Fleuriot | Exploring the foundations of discrete analytical geometry in Isabelle/HOL[END_REF]. The two formalizations are independent and do not rely on the same foundations. Fleuriot uses the existing mechanization of nonstandard analysis available in Isabelle/HOL. His formalization is based on hyperreals, which are an extension of the real numbers R obtained using the so-called ultrapower construction [START_REF] Fleuriot | A combination of nonstandard analysis and geometry theorem proving, with application to newton's principia[END_REF]. This construction happens to be not constructive.

In our formal developement in Coq, we follow the layout of previous papers on the Harthong-Reeb line [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF][START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF] and we consider a minimal axiomatic form of nonstandard analysis, related to Nelson' s Internal Set Theory (IST) [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF]. We also intend to capture the inheritely constructive nature of the model of the Harthong-Reeb line in our formalization, using Ω-numbers, introduced by Laugwitz and Schmieden in [START_REF] Laugwitz | Eine erweiterung der infinitesimalrechnung[END_REF]. Indeed, the aim, in addition to proving formally some properties of the Harthong-Reeb line is to be able to derive actual (Ocaml) programs from the formalization of operations such as Euler's arithmetization scheme on Ω-numbers. Such programs can be directly written in Coq, and thus one can both compute using these programs and formally prove some properties about their behavior.

There exists alternative models of nonstandard analysis, e.g. [START_REF] Kaye | Models of Peano Arithmetic[END_REF][START_REF] Moerdijk | A model for intuitionistic non-standard arithmetic[END_REF]. However, we are interested in building a model which is easy to implement and practically usable to perform computations in the context of discrete analytical geometry. That is why we focus on Laugwitz-Schmieden Ω-numbers for our concrete implementation of nonstandard numbers. Indeed, such a model makes it possible to have a multi-scale representation of geometric objects.

Our research is application-driven and we expect these new results to help improve the quality of sofware used in the field of discrete analytical geometry. We did not investigate some more theoretical issues such as links with Tennenbaum's theorem; we only aim at providing a better representation of numbers (w.r.t floating-point numbers) for applications such as computations of continuous functions.

A minimal axiom system for nonstandard arithmetic

The ground idea of the Harthong-Reeb line is to introduce a non trivial rescaling on the set of integers in order to get a discrete form of the continuum. To do so a nonstandard arithmetic is used. In this section, we present a formalization of such a nonstandard arithmetic on top of which we shall build the Harthong-Reeb line.

Nonstandard Model of Arithmetic

Axiomatizing Numbers We first have to specify the axiomatic numbers we shall use in this work as well as their operations and their properties. We do that using a module type in Coq. From a programmming perspective, this can be viewed as an interface which, on the one hand, gathers all the properties of nonstandard numbers required to build the Harthong-Reeb line and on the other hand, can be implemented by a concrete datatype, operations and proofs of the axioms (as we do in section 5). This module type contains the declaration of the basic objects of the theory (A is the abstract data type denoting non standard integers): Parameter leA ltA : A -> A -> Prop.

We choose to let A live in Type, which is the topmost Sort in Coq. The Coq proof assistant features three sorts Prop, Set and Type. Usually, Prop is the type of propositions, whereas Set is the type of computations. Moreover, Type is the type of Prop and Set. For convenience, we choose to have A : Type, as the axiomatic real numbers of Coq also live in Type.

Notations can be introduced to ease reading and writing of specifications. This also allows us to stay close to the way mathematicians would write.

Notation "x + y " := (plusA x y). Notation "x * y " := (multA x y). Notation "x / y " := (divA x y).

Notation "0" := (a0). Notation "1" := (a1). Notation "-x" := (oppA x). Notation "| x |" := (absA x) (at level 60). Notation "x <= y" := (leA x y) (at level 50). Notation "x < y" := (ltA x y) (at level 50).

Then all the basic properties of A are expressed as axioms. Overall, we assume that A with the operations +,×,. . . is equipped with a ring structure. This will allow to prove basic algebraic equations automatically and also to perform some otherwise tedious simplifications of expressions. We also assume that it is equipped with an euclidian division operator and the absolute value (x → |x|).

In addition, we assume that the order relations ≤ and < enjoy their usual properties such as transitivity, regularity w.r.t operations such as addition, etc. We also assume these relations are decidable by adding the following axiom which states that forall x : A, either x < 0 or x = 0 or 0 < x. Axiom A0_dec : forall x, {x < 0}+{x = 0}+{0 < x}.

Nonstandard aspects Even if axiomatizations of nonstandard analysis, such as IST [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF], are available, we present here, in the spirit of some works of Nelson or Lutz [START_REF] Nelson | Radically Elementary Theory[END_REF][START_REF] Lutz | La force modélisatrice des théories infinitésimales faibles[END_REF], a weaker axiom system which is well suited for our purpose. First we introduce a new predicate lim over integer numbers: lim(x) "means" that the integer x is limited. This intends to capture the idea that x is not infinitely large. We also introduce the number ω denoted by w. This number is larger than all naive integers as argued by Reeb in [START_REF] Diener | Analyse Non Standard[END_REF].

Parameter lim : A -> Prop. Parameter w : A. This predicate is external to the classical integer theory and its meaning directly derives from the following axioms ANS1, ANS2, ANS3, ANS4 (and ANS5 which will be introduced later):

ANS1. The number 1 is limited.

Parameter ANS1 : lim 1.

ANS2. The sum and the product of two limited numbers are limited.

Parameter ANS2a : forall x y, lim x -> lim y -> lim (x + y). Parameter ANS2b : forall x y, lim x -> lim y -> lim (x * y).

ANS3. Non-limited integer numbers exist.

Parameter ANS3 : ~lim w.

We simply assert that w is not limited (in Coq, ~stands for logic negation).

ANS4. For all (x, y) ∈ A 2 such that x is limited and |y| ⩽ |x|, the number y is limited. For reading conveniences, we introduce the following notations [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF]:

-∀ lim x F (x) is an abbreviation for ∀x (lim(x) ⇒ F (x)) and can be read as "for all limited x, F (x) stands". -∃ lim x F (x) is an abbreviation for ∃x (lim(x) ∧ F (x)) and can be read as "there exists a limited x such that F (x)".

Following the IST flavour [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF], we say that a formula or a proposition P is external when the predicate lim occurs in P and internal otherwise. This distinction is necessary to determine when properties known for standard properties can be extended to the nonstandard ones. In fact, when a property P is internal, i.e. when it does not use the predicate lim, the extension of P to infinitely large numbers is immediate. This is given by the following Overspill principle. But for external properties, we cannot proceed in the same way. We need to introduce a new extension principle as an axiom (called ANS5 in this paper). This principle states that the formula which contains external properties can be extended to infinitely large numbers, but that we do not know whether these infinitely large numbers verify these properties. Proposition 1. (Overspill principle) Let P(x) be an internal formula such that P(n) is true for all n ∈ A, limn ∧ n ⩾ 0. Then, there exists an infinitely large6 ν ∈ A, ν ⩾ 0 such that P(m) is true for all integers m such that 0 ⩽ m ≤ ν.

Parameter overspill_principle : forall P:A -> Prop, (forall n:A, lim n /\ 0<=n -> P n) -> (exists v:A, ~lim v /\ 0<=v /\ (forall m:A, 0<=m /\ m <=v -> P m)).

The following principle, which is our last axiom, can deal with both an internal and an external formula P .

ANS5. (External inductive defining principle):

We suppose that 1. there is

x 0 ∈ A p such that P((x 0 )); 2. for all n ∈ A, n ⩾ 0 ∧ lim(n) and all sequence (x k ) 0⩽k⩽n in A p such that P((x k ) 0⩽k⩽n ) there is x n+1 ∈ A p such that P((x k ) 0⩽k⩽n+1 ).
Then, there exists an internal sequence (x k ) k∈A,k⩾0 in A p such that, for all n which verifies limn ∧ n ⩾ 0, we have P((x k ) 0⩽k⩽n ).

This principle means that the sequence of values x k for k limited can be prolonged in an infinite sequence (x k ) k∈A,k⩾0 defined for all integers. Saying that this sequence is internal means that it has all the properties of the classical sequences in usual number theory. In particular, if

Q(x) is an internal formula, then the set {k ∈ A, k ⩾ 0 ; Q(x k )} is an internal part of {k ∈ A, k ⩾ 0}.
In Coq, we choose a slighly different and more convenient definition of ANS5. First we only consider the case p = 1. In addition, we choose to have a predicate P whose arity is fixed. In the definition of ANS5 in Coq, the predicate P only applies to a single element of the sequence rather than to the whole sequence. It can be viewed as a projection on the original P on the k th element of the sequence. This means a statement such as P((x k ) 0⩽k⩽n ) is translated into ∀k, 0 ⩽ k ⩽ n → P (x k ). Finally, we have to make explicit that the sequence whose existence is shown coincides with the initial one for all k such that 0 ⩽ k ⩽ n. Overall, this leads to a weaker principle which, at the same time, is sufficient for our purposes and more convenient to use in Coq. Its statement in Coq is the following one: Here, the sequence u expects two arguments: an element n of A and a proof

H that lim n ∧ n ⩾ 0. In this context, H0 is a proof of lim 0 ∧ 0 ⩾ 0 and (ANS4_special n k Hn Hk) is a proof of lim k ∧ k ⩾ 0.
Note that {x:A|P x}, which is a convenient notation for existential Σ-types (sig P), allows us to describe sets comprehensively. Here it corresponds to the set of elements of A which verify P . This corresponds to an inductive definition in Coq. It comes together with two projections: proj1_sig, which returns a and proj2_sig which returns a proof H of P a. In addition, ANS4_special is a theorem which is derived from ANS4 and states the following property:

Lemma ANS4_special : forall n k:A, (lim n /\ 0<=n) -> (0<=k /\ k<=n) -> lim k /\ 0<=k.
4 Formalizing the Harthong-Reeb line: A modular approach 4.1 The system HR ω .

Let us now give the definition of the system HR ω . Introduced by M. Diener [START_REF] Diener | Application du calcul de Harthong-Reeb aux routines graphiques[END_REF], this system is the formal version of the so-called Harthong-Reeb line. In this section we prove that this system can be viewed as a model of the real line which is partly constructive. Indeed, we do not have means to construct an infinitely large number ω yet. In some sense, HR ω is equivalent to R (see [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF] for details). Accordingly to axiom ANS3, the construction starts by considering an infinitely large (non-limited) positive integer ω ∈ A. Our purpose is to define a new numerical system such that all the elements are integers and, in which ω is the new unit. Let us introduce the underlying set of this system. Definition 1. The set HR ω of the admissible integers considering the scale ω is defined by: HR

ω = {x ∈ A ; ∃ lim n ∈ A, n ⩾ 0 such that |x| < nω}.

This definition can be easily translated in Coq:

Definition P := fun (x:A)=> exists n:A, (lim n /\ 0 < n /\ (|x| <= n*w)). Definition HRw := {x:A | P x}.

The set HR ω is an external set. Moreover, it is an additive sub-group of A. We provide HR ω with the operations + ω and * ω , the ω-scale equality, the ω-scale inequality relations (noted = ω and ̸ = ω ) and the order relation > ω : Definition 2. Let X and Y be any elements of HR ω .

-X and Y are equal at the scale ω and we write X = ω Y when

∀ lim n ∈ A n > 0 → n|X -Y | ⩽ ω.
-Y is strictly greater than X at the scale ω and we write Y > ω X when

∃ lim n ∈ A n > 0 ∧ n (Y -X) ⩾ ω. -X is different from Y at the scale ω and we write X ̸ = ω Y when (X > ω Y or Y > ω X) -The sum of X and Y at the scale ω is X + ω Y := X + Y (like the usual sum).
For this operation, the neutral element is 0 ω = 0 and the opposite of

each element Z ∈ HR ω is -ω Z := -Z. -The product of X and Y at the scale ω is X × ω Y := ⌊ X.Y ω ⌋ (different from the usual one). The neutral element is 1 ω := ω, and the inverse of each element Z ∈ HR ω such that Z ̸ = ω 0 ω is Z (-1)ω := ⌊ ω 2 Z ⌋ .
Algebraic operations are defined on the integers of the set A onto which HR ω is built. Therefore we must ensure the result still belongs to HR ω . For the sum, it consists in proving the following lemma: Lemma Padd: forall x y:A, P x -> P y -> P ( x + y).

Then, the addition in HR ω can be defined as follows:

Definition HRwplus (x y: HRw) : HRw := match x with exist xx Hxx => match y with exist yy Hyy => exist P (xx + yy) (Padd xx yy Hxx Hyy) end end.

All lemmas and formal definitions of the objects of Definition 2 are summarized in Fig. 2.

Proving Bridges' Axioms

In the 90's, Brigdes proposed in [START_REF] Bridges | Constructive mathematics: A foundation for computable analysis[END_REF] an axiomatic definition of what a constructive real line is. It is decomposed into three groups about algebraic structure (R1), ordered set (R2) and the last group (R3) deals with special properties (see the details below). A field which satisfies these axioms is called a Bridges-Heyting ordered field. In [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF], the proof of that the Harthong-Reeb line with associated In this section, we show how the required properties can be expressed and proved correct in Coq.

R1. Algebraic structure ∀x, y, z ∈ HR ω , 1. x + ω y = ω y + ω x 2. (x + ω y) + ω z = ω x + ω (y + ω z) 3. 0 ω + ω x = ω x 4. x + ω (-ω x) = ω 0 ω 5. x × ω y = ω y × ω x 6. (x × ω y) × ω z = ω x × ω (y × ω z) 7. 1 ω × ω x = ω x 8. x × ω x (-1)ω = ω 1 ω if x ̸ = ω 0 ω 9. x × ω (y + ω z) = ω x × ω y + ω x × ω z
This first group presents the expected properties about the two operations + ω and × ω . There is not any major difficulties to prove that HR ω verifies these axioms.

All the axioms of this group can be formally proved using the definitions of the operations involved. Most of these properties are expressed using Leibniz equality of Coq. They proceed by case analysis on the elements of HR ω , destructuring them into an element x of A and a proof H that P (x) holds. We present the proof of the first one (commutativity of addition). Proving the terms HRwplus x y and HRwplus y x are equal in HR ω consists in not only proving the witnesses (in A) are equal but also proving the proofs of the properties P (x + y) and P (y + x) are equal. As what matters is only that P holds for the considered element, we use the principle of proof irrelevance to show all proofs of the same property (e.g. P (x)) are equal 7 . This principle is expressed with the following axiom in Coq:

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. This well-known principle is consistent with Coq's logic (provided P is in Prop) and therefore we can safely add it to our formal description (see [START_REF] Chlipala | Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant[END_REF]Chap. 12] for details). Some properties such as ( 6), ( 8) and ( 9) do require using the equality = ω defined above. Indeed when computations at the level of A involve products and quotients, terms can no longer be shown equal w.r.t Leibniz equality. If necessary, all properties can be established for the HR ω equality = ω . Indeed, this defined equality can be easily derived from Leibniz equality when needed.

Once all the properties of the first group have been proved in Coq, we can declare HR ω equipped with its operations and the equality relation = ω as a ring structure. It works in the same way we did it for A and also allows us to carry out simplifications of algebraic expressions of type HR ω . The only restriction is that morphisms such as

∀x, y, z, t ∈ HR ω x = ω y ⇒ z = ω t ⇒ x × ω z = ω y × ω t
needs to be proved by hand to be able to do some rewriting.

R2. Basic properties of

> ω ∀x, y, z ∈ HR ω , 1. ¬ (x > ω y ∧ y > ω x) 2. (x > ω y) ⇒ ∀z (x > ω z or z > ω y) 3. ¬(x ̸ = ω y) ⇒ x = ω y 4. (x > ω y) ⇒ ∀z (x + ω z > ω y + ω z) 5. (x > ω 0 ω ∧ y > ω 0 ω ) ⇒ x × ω y > ω 0 ω
All these properties can be proved in a very straightforward manner in Coq, following the informal proofs of [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF]. Note that this definition of inequality is quite more complex than the usual one. This comes from the fact that the decidability of > ω is not necessarily required. Thanks to this definition of inequality on the Harthong-Reeb line, these above-mentioned axioms are easily provable. We just need to assume that the basic inequality on A is decidable. This hypothesis is not a problem for the axiomatic definition of nonstandard arithmetic we consider so far but, in practice there are some problems. We shall work on these issues in Section 5 for the Laugwitz-Schmieden model where this inequality is not decidable. An alternative approach, being currently investigated by G. Wallet, would be to obtain this property using another model based on a non standard variant of Martin-Löf's Type Theory [START_REF] Martin-Löf | Intuitionnistic Type Theory[END_REF][START_REF] Martin-Löf | Mathematics of infinity[END_REF].

Links between orders in HR ω and orders in A. We recall that, in HR ω , the strictly greater relation > ω and the greater or equal relation ⩾ ω are defined from the less or equal relation on A (y > ω x ≡ ∃ lim n ∈ A n (y -x) ⩾ ω and y ⩾ ω x ≡ ∀ lim n ∈ A n (y -x) ⩽ ω). However, we can characterize the ⩾ ω relation using the > ω relation as follows:

∀a, b ∈ HR ω b ⩾ ω a ≡ ∀c ∈ HR ω a > ω c ⇒ b > ω c.
This makes proofs of properties about ⩾ ω much easier to write. Finally, we also have the two following correspondences for all a, b ∈ HR ω :

a ⩾ b implies a ⩾ ω b and a > ω b implies a > b
They are key properties of our development, allowing us to switch back and forth between properties of > and > ω , when convenient. They are easily proved in Coq.

R3. Special Properties of > ω

The two last properties to prove to fulfil the requirements of Bridges' axiom system are the following ones:

1. Axiom of Archimedes: For each X ∈ HR ω there exists a constructive n ∈ A such that X < n.

The constructive least-upper-bound principle (see next section)

Archimedes property can be easily formalized in Coq:

Lemma Archimedes : forall X:HRw, exists n:HRw, n >=w X.

Proof. Its proof is immediate because the elements x of HR ω are such that there exists a limited k ∈ N, |x| < kω. So the property can be proved using the integer kω as a witness for n.

Least upper bound

To begin, let us recall some definitions. A subset S of HR ω is the collection of elements of HR ω which satisfies a given property defined in the system. This property may be internal or external. Such a subset S is bounded above with respect to the relation ⩾ ω if there is b ∈ HR ω such that b ⩾ ω s for all s ∈ S; the element b is called an upper bound of S. A least upper bound for S is an element b ∈ HR ω such that The constructive least-upper-bound principle: Let S be a nonempty subset of HR ω that is bounded above w.r.t. the relation ⩾ ω , such that for all α, β ∈ HR ω with β > ω α, either β is an upper bound of S or else there exists s ∈ S with s > ω α; then S has a least upper bound.

-∀s ∈ S b ⩾ ω s (b is an upper bound of S); -∀b ′ (b > ω b ′ ) ⇒ (∃s ∈ S s > ω b ′ ).
Proof. To formalize and prove this property correct in Coq we follow the proof proposed in [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF], which itself uses the heuristic motivation given by Bridges in [START_REF] Bridges | Constructive mathematics, in theory and programming practice[END_REF]. It consists of two parts: we first construct a candidate b for the least upper bound and we then check that b is actually the least upper bound.

Definitions in Coq

The subset property is defined as a property, i.e. S x means x belongs to the set S. Then the notions of least upper bound and of upper bound are defined. Definition upper_bound (X:subset) (m:HRw) : Prop := forall x:HRw, X x -> m >w x. 2 sequences (s n , b n ) In the original paper [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF], four sequences (s n , b n , α n , β n ) which are mutually recursive and that will be useful to define a candidate b for the least upper bound are defined. To make it simpler in Coq, we have to simplify this definition by considering only 2 sequences (s n , b n ). Indeed, one can easily note that α n and β n only depend on the values of s n and b n . Thus there is no need to include them in the recursive process of building the sequences (s n ) and (b n ). Indeed, at each step, α n and β n can be redefined as follows:

α n = 2 3 × s n + 1 3 × b n β n = 1 3 × s n + 2 3 × b n .
Computing the next terms s n+1 and b n+1 of the sequences depends on the two preceding terms (s n , b n ). From these data, we can build α n and β n as well as a proof of the property β n > ω α n . However we need to carry around the three key properties of s n and b n :

-s n belongs to S -b n is an upper bound of S -b n -ω s n = ω ( 2 3 ) n × ω (b 0 -ω s 0 )
. Therefore, we choose to specify the function as precisely as possible when defining it, hence the numerous postconditions characterizing the output (s n , b n ) of the function when giving the parameters n and Hn a proof that lim n∧0 ⩽ n.

Definition def_s_b :

forall n:A, forall Hn:(lim n /\ 0 <= n), {sn:HRw & {bn:HRw & S sn /\ upper_bound S bn /\ bn +w (-w sn) =w ((power two_third n Hn)*w (b0 +w (-w s0)))}}.

The notation {x : A&Q x} stands for the (computational) existential quantification, i.e. there exists x of type A such that Q x holds. Initially, we have (s 0 , b 0 ) with an arbitrary element s 0 of S, b 0 an upper bound of S, and α 0 = 2 3 s 0 + 1 3 b 0 and β 0 = 1 3 s 0 + 2 3 b 0 . This requires the assumption that in Coq that we can always choose an arbitrary element s of S. This corresponds to a form of choice which can be expressed as follows:

Axiom non_empty : {x:HRw|X x}.

It states that a subset X of elements of HR ω is non-empty if and only if there exists an element x of HR ω for which X (x) holds.

Suppose for a given n, we have (s n , b n ). We can build (α n , β n ) as well as a proof of the property α n < ω β n . By hypothesis, two different cases can happen:

-First case β n is an upper bound of S. Then we choose s n+1 and b n+1 such that s n+1 = s n and b n+1 = β n . -Second case there exists s such that (S s) and that α n < ω s. Then we choose s n+1 and b n+1 such that s n+1 = s and b n+1 = b n + s -α n .

Key properties.

Several key properties of the elements of the sequences are already expressed in the type of def_s_b. They hold by construction (i.e. they are established using induction at the same time the actual sequences are computed). Among them, we know that, for each n, which is limited and positive, the property S(s n ) ∧ upper_bound S b n holds. Thus, we can deduce that for any k and n, we have b k > ω s n . We also have the property that b n and s n are connected by the relation

b n -ω s n = ω ( 2 3 ) n × ω (b 0 -ω s 0 ).
In addition to all the properties specified in the type of def_s_b, we also need to establish that the sequence (s n ) is increasing. Although this is immediate from its mathematical definition, it is rather challenging to prove it correct in Coq. Indeed it requires to apply the ad hoc induction principle nat_like_induction and its associated reduction rules without any assistance of the Coq proof engine. This happens to be fairly tedious in Coq because existential Σ-types and let-in constructs are involved in the definition of def_s_b and foldings of expanded definitions (e.g. the recursive call to nat_like_induction) have to be done manually 9 .

Thanks to axiom ANS5, the sequences (s n ) and (b n ) can be extended to all integers, including non-limited ones. In addition, the overspill principle allows us to show the existence of an infinitely large number ν such that the following property holds:

min 0⩽k⩽ν b k ⩾ s ν ⩾ . . . ⩾ s 1 ⩾ s 0 .
A candidate for the least upper bound of S : b := min 0⩽k⩽ν b k

The next step, which consists of checking that b is the least upper bound is presented in [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF] and is summarized here by proving the two following properties:

on the one hand, that b is an upper bound of S, -on the other hand, that b is actually a least upper bound, i.e. that for all b ′ < ω b, there exists s ∈ S such that s > ω b ′ .

Proof scripts are available online (especially in the files LUB*.v) :

http://dpt-info.u-strasbg.fr/~magaud/Harthong-Reeb/ So far, we showed formally that the Harthong-Reeb line, constructed from a minimal axiom system for non standard arithmetic such as the one proposed in Section 3, does verify Bridges' axiomatic definition of what a constructive real line is.

In this section, we investigate how to provide some computational contents to the axiomatization of the Harthong-Reeb line. We implement non-standard integers using the Ω-numbers of Laugwitz and Schmieden. We first define these numbers and their operations and also prove their properties in Coq. We then discuss their limitations with respect to being a well-suited model for our axiom system for non-standard arithmetic and our formalization of the Harthong-Reeb line. Finally, we show that this implementation of non-standard numbers can be used to compute continuous functions using integers.

Formalization of the Ω-numbers

The Ω-numbers of Laugwitz and Schmieden permit the extension of a classical numerical system to a nonstandard one. Here we present this extension of integers. It can be viewed as a model of the axiomatic definition of the nonstandard arithmetic presented in Section 4. In their papers [START_REF] Laugwitz | Ω-calculus as a generalization of field extension an alternative approach to nonstandard analysis[END_REF][START_REF] Laugwitz | Leibniz' principle and Ω-calculus[END_REF][START_REF] Laugwitz | Eine erweiterung der infinitesimalrechnung[END_REF], Laugwitz and Schmieden extend the rational numbers and show that their system is equivalent to classical real numbers. In this section, we will not describe the whole theory but only introduce the basic notions that are essential to understand the Harthong-Reeb line. For more details about our approach please refer to [START_REF] Chollet | Ω-Arithmetization: a Discrete Multi-resolution Representation of Real Functions[END_REF].

To extend a theory of integer numbers, Laugwitz and Schmieden introduce a new symbol Ω to the classical ones (0, 1, 2, 3, . . . , +, /, . . .). The only property that Ω verifies is named the Basic Definition (denoted (BD)) : Definition 3. Let S(n) be a statement in N depending on n ∈ N. If S(n) is true for almost n ∈ N, then S(Ω) is true.

We consider the expression "almost n ∈ N" means "for all n ∈ N from some level N", i.e. "(∃N ∈ N) such that (∀n ∈ N) with n > N ". Since Ω can be substituted to any natural number, it denotes an Ω-number which is the first example of Ω-integer. Hence, each element a of this theory will be declined as a sequence (a n ) n∈N . Immediately, we can verify that Ω is infinitely large, i.e. greater than every element of N. Indeed, for p ∈ N, we apply (BD) to the statement p < n which is true for almost n ∈ N; thus p < Ω for each p ∈ N. And Ω is the sequence (n) n∈N .

Technically speaking, Ω-integers are defined in Coq as sequences indexed by natural numbers (nat), whose values are relative integers (Z). The function Z_of_nat simply injects natural numbers into Z. Here we choose to define ω as the sequence w n = n. However, we parametrized our development so that we can choose between three different ω, defined as w n = n, w n = n 2 or w n = 2 n . The only requirement is that (w n ) must be strictly increasing. The sequence w n = 2 n is the most convenient one because all its terms are non-zero, which makes dealing with division easier in the implementation (see Section 5.3 for details).

To compare such Ω-numbers, we put the following equivalence relation: This is captured by the definition equalA.

Definition equalA (u v:A) := exists N:nat, forall n:nat, n>N -> u n=v n.

We define two classes of elements in this nonstandard theory:

-the class of limited elements: they are the elements α = (α n ) n∈N which verify ∃p ∈ Z such that ∃N ∈ N, ∀n > N, α n < p (example: (2) n∈N ). -the class of elements: infinitely large numbers, which are the sequences α = (α n ) n∈N such that lim n→+∞ α n = +∞

We recall that infinitely large numbers correspond to non-limited numbers. The definition of the operations and relations on A, the set of Ω-numbers are the following ones. It is straightforward to formalize them in Coq.

Definition 5. Let a = (a n ) n∈N and b = (b n ) n∈N two Ω-numbers, -a + b = def (a n + b n ) n∈N and -a = def (-a n ) and a × b = def (a n × b n ) n∈N ; Definition plusA (u v:A) := fun (n:nat) => Zplus (u n) (v n). Definition multA (u v:A) := fun (n:nat) => Zmult (u n) (v n). Definition oppA (u:A) := fun (n:nat) => Zopp (u n). -a > b = def [(∃N ∀n > N ) a n > b n ] and a ⩾ b = def [(∃N ∀n > N ) a n ⩾ b n ]; Definition leA (u v:A) := exists N:nat, forall n:nat, n>N -> Zle (u n) (v n).
Definition ltA (u v:A) := exists N:nat, forall n:nat, n>N -> Zlt (u n) (v n).

-|a| = def (|a n |).

Definition absA (u:A) := fun (n:nat) => Zabs (u n).

Specificity of the theory Regarding the order relation, the usual properties true on Z are not always verified on Z Ω (= A, which is N → Z). For instance

(∀a, b ∈ Z Ω ) (a ⩾ b) ∨ (b ⩾ a) (1)
is not valid as we can see for the particular Ω-integers a = ((-1) n ) n∈N and b = ((-1) n+1 ) n∈N . Nevertheless, given two arbitrary Ω-numbers a = (a n ) and b = (b n ), we can prove

(∀n ∈ N) (a n ⩾ b n ) ∨ (b n ⩾ a n ) (2)
because we have a decidability property for Z. Using the basic definition (BD), we obtain (a Ω ⩾ b Ω ) ∨ (b Ω ⩾ a Ω ) and thus (1) since a Ω = a and b Ω = b. Hence, there is a contradiction. To avoid it, we might admit that the application of (BD) leads to a notion of truth weaker than the usual notion.

Overall, this shows that the Ω-numbers can not be an exact model of the theory presented in Section 4. The main issue is the decidability property A0_dec of the order relation which is obviously not provable in this setting. In the next section, we show how the theory of Section 4 can be modified into a new (slightly different) theory of which the Ω-numbers are a model.

Nonstandard axioms

We define two predicates std and lim: (std n) states that an Ω-number n is standard (i.e. denoted by a sequence which is constant from a given rank) and (lim n) that n is limited (i.e. its absolute value is bounded by a positive, standard number).

Definition std (u:A) := exists N:nat, forall n m, n>N -> m>N -> (u n)=(u m).

Definition lim (a:A) := exists p, std p /\ leA a0 p /\ ltA (absA a) p.

From these definitions, we can derive proofs of the axioms ANS1 to ANS4 presented in Section 4. In this paper, we did not investigate whether ANS5 can be defined constructively and it remains an open question to know whether ANS5 could be proved formally in Coq for Ω-numbers.

A version of the Harthong-Reeb line based on Ω-numbers

An instantiation of the minimal axiom system for non-standard arithmetic All properties of our minimal axiom system for non-standard arithmetic (presented in Section 3) need to be actually proved in the setting of Laugwitz-Schmieden Ω-numbers. It requires the design of some sophisticated tactics using Ltac, to deal with existential statements efficiently. Let us consider the following example (A is actually a functional type nat→Z). lt_plus : ∀x y z t : A, x < y ⇒ z < t ⇒ (x + z) < (y + t).

Proving this property, which corresponds (once everything is unfolded) to: ∀x y z t : nat → Z, ∀H : ∃P : nat, ∀p : nat, p > P → (x p < y p), ∀H0 : ∃Q : nat, ∀q : nat, n > Q → (z q < t q), ∃N : nat, ∀n : nat, n > N → (x n + z n < y n + t n)

requires extracting two witnesses P and Q, building a new witness N := P +Q+1 and generalizing the hypotheses coming from the destruction of H (resp. H0) with the universally quantified variable n and a proof that it is greater than P (resp. Q) -which is the case as it is greater than P+Q+1 by hypothesis -. This yields an inequation on Z, which can be solved using omega or the adequate lemma of the ZArith library. The tactics solve_ls and solve_ls_w_l (which provides a lemma of ZArith as a hint) perform all this in one go.

Limitations of the Laugwitz-Schmieden integers Laugwitz-Schmieden integers cannot be a model of the Harthong-Reeb line as it was defined in Section 4. In [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF], some of the authors identified among all the properties required to be a Bridges-Heyting field the ones which are not immediately verified by the instantiation of the Harthong-Reeb line with Ω-numbers. This is summarized in a the theorem (from [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF]) which is quoted in Figure 3. It expresses that three of Bridges axioms do not hold (namely A.2.2, A2.3 and A3.2) when non-standard integers are represented as Laugwitz-Schmieden integers. However, these three statements can be (slightly) modified so that they hold on Laugwitz-Schmieden integers (see [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF] for details). (2)' If x, y ∈ HRω are such that x <ω y, then for each z ∈ HRω, there is a q ∈ N such that (q(yz) ⩾ ω) ∨ (q(zx) ⩾ ω) is weakly true. Our formalization in Coq confirms these issues. Let us remind the reader the problem comes with the axiom (A is instantiated with nat→Z): Axiom A0_dec : forall x: A, {x < 0}+{x = 0}+{0 < x}.

Indeed, as stated in the previous section, we have no decidability of the order for sequences a and b in general, we can only prove a decidability property for each of the elements of the sequences (a n ) and (b n ).

Axioms A2.2, A2.3 and A3.2 (the least upper bound principle) 11 can not be proved in this setting as stated in [6,[START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF]. In addition, basic properties such as generalizing the property that a sequence is increasing interfere with these decidability properties and their proofs as they were carried out in Section 4 are no longer acceptable. This is the case for the following statement:

∀n, s n ≤ s n+1 ⇒ (∀p q, p ≤ q ⇒ s p ≤ s q ).
Formalizing the theorem quoted in Figure 3 is currently under way in our formal development. It requires us to take into account the specificities of Laugwitz-Schmieden numbers compared to our first axiom system for non-standard arithmetic. We hope that proofs presented in [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF] could be easily formalized in Coq.

Computing continuous functions

The main advantage of having a concrete representation of non-standard integers is the possibility to compute with them. This is what we achieve in this section using the Ω-integers. It provides us with practical means to compute continuous functions using only integer sequences. This is based on the Ω-arithmetization scheme as described in [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF]. An arithmetization scheme is a process which provides discrete equivalents to continuous functions. The one we use is derived from the well known Euler's integration scheme  

 T 0 = A; X 0 = B T k+1 = T k + 1 h X k+1 = X k + 1 h × F (T k , X k
) This scheme computes a numerical approximation (T k , X k ) k⩾0 of the continuous function X : T → X(T ) defined on an interval of R with values in R which is the solution of the Cauchy problem X ′ = F (X, T ), X(A) = B. It is well known that the error of the approximation |X(T k ) -X k | converges to 0 when h → +∞.

Following Reeb and Reveillès [START_REF] Reveillès | Back and forth between continuous and discrete for the working computer scientist[END_REF], the idea is to replace the number h with an infinitely large Ω-integer and to translate all other quantities using the function Ψ ω : R → Z Ω such that Ψ ω (U ) = (⌊ω m × U ⌋) m∈N and where ω is an infinitely large Ω-integer.

The Ω-arithmetization of Euler's scheme at the global scale ω is the following scheme with variables x k , t k ∈ Z Ω (i.e. sequences of elements of Z) :

   t 0 = a; x 0 = b t k+1 = t k + β x k+1 = x k + f (t k , x k ) ÷ β
where β is an infinitely large positive Ω-integer such that β 2 = ω and a = Ψ ω (A), b = Ψ ω (B) and f is the translation of the function F ,

f (t, x) = (⌊ω m × F (t m /ω m , x m /ω m )⌋) m∈N .
This scheme computes a sequence of points (t k , x k ) which is the graph of a discrete function t → x(t) called the Ω-arithmetization at the global scale ω of the function T → X(T ). The problem with this direct translation is that the domain of the function t → x(t) is not connected since t k+1 -t k = β which is infinitely large. To correct this, the arithmetic scaling x → x ÷ β is used. This sends β to 1 and now the points (t k , x k ) are observed at the intermediate scale β. In order to compute the arithmetization directly at the scale β, the following scheme is used

       t 0 = a ÷ β, x 0 = b ÷ β and x 0 = b mod β t k+1 = t k + 1 x k+1 = x k + ( x k + f k ) ÷ β x k+1 = ( x k + f k ) mod β where x = x ÷ β and x = x mod β and f k = f ( t k × β + a mod β, x k × β + x k ) ÷ β.
This scheme computes a sequence of points ( t k , x k ) which is the graph of the discrete function t → x( t ) defined over a connected domain because t k+1 -t k = 1. This discrete function is the Ω-arithmetization of the function T → X(T ) at the intermediate scale β. Properties of Ω-arithmetization are studied in [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF]. The most notable is that Ω-arithmetization is an exact representation of the continuous function T → X(T ). So, this is a good motivation to experiment computations using the formalization of the Harthong-Reeb line with Coq.

The previous scheme is straightforward to implement in Coq using recursive functions: Note that the function hd that returns the head of a list comes with an extra argument in case it receives the empty list as argument.

The computational contents of our formal description of the Ω-integers of Laugwitz and Schmieden, including the function computing the arithmetization is automatically extracted into the functional programming language Ocaml. The main extraction commands required to do that are summarized in Figure 5. The extracted code can then be connected to a visualisation tool which allows us to observe the continuous function we computed with the arithmetisation scheme.

Extraction consists in removing all terms with non computational contents and making all dependent types non-dependent such that they can be accepted by Ocaml's type-checker. The commands Extract Inductive and Extract Constant provide means to explain to the system how Coq inductive definitions and constants should be implemented in Ocaml. There is no formal verification of the relevance of this translation. It is the user's responsability to make sure no mistakes are introduced at this stage. Recent improvements of the Coq computation machinery shall make it possible to compute our continuous functions directly in Coq, thus avoiding this (unsafe) extraction process to Ocaml.

For example, the result of the arithmetization for the function t → t 2 6 is shown in Figure 4. In this example, the function corresponding to F in the above algorithm is F : (T, X) → T 3 . As Ω-integers are infinite sequences of integers they cannot be visualized directly. One must choose different fixed ranks in the involved sequences to see the graphs of the discrete function t → x( t ) at those ranks. Examples of graphs at different ranks for the function t → t 2 6 are drawn on the Figure 4.

Discussion

The actual construction of HR ω based on Laugwitz-Schmieden so-called Ωintegers, proposed in Section 5.2 leads to an alternative constructive continuum which is different from the one characterized by Bridges' axiom system. Formalizing it is another challenge and is currently under way. In addition to shifting the reasoning from the level of the sequences to the level of the elements (of Z), it also requires formalizing several new notions, especially a congruence relation on sequences which allows us to define what regular Ω-integers are. From what we experimented and reported so far, and even if we are confident the proofs of [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF] are correct, it seems very useful to carry out this formalization. It would allow for a better understanding of the definitions, properties and associated proofs and may lead to fixing some imprecisions or shortcomings of the hand-written proofs.

Future work also include linking our formal description of the Harthong-Reeb line with a constructive description of real numbers such as the one developed in Niemejen [START_REF] O'connor | Certified Exact Transcendental Real Number Computation in Coq[END_REF][START_REF] Krebbers | Type Classes for Efficient Exact Real Arithmetic in Coq[END_REF]. This would require to define Ω-rationals and then show formally that the Harthong-Reeb system is equivalent to R in some sense (the exact meaning of this sentence is discussed in [START_REF] Chollet | Insight in discrete geometry and computational content of a discrete model of the continuum[END_REF]). Once this is achieved, we could formally prove that the Euler arithmetization scheme, whose implementation in Coq was presented in this paper, is actually correct.

Conclusion

We proposed a formalization of non standard arithmetic on top of which we built the Harthong-Reeb line. We also implemented non standard arithmetic using Laugwitz-Schmieden Ω-numbers.

This includes proving that our formal description of the Harthong-Reeb line verifies Bridges' axioms, and therefore is a constructive real line. In addition, we verify that the Ω-numbers are a suitable implementation of non standard arithmetic, with which all these properties can be proved correct, with the exceptions of R2.2. and R2.3. and the least upper bound property. We also managed to extract the Coq definitions into an Ocaml program which performs exact computations of continuous functions using only Laugwitz-Schmieden (sequences of) integers.

As shown in [START_REF] Chollet | Foundational Aspects of Multiscale Digitization[END_REF], the axiom system for the Harthong-Reeb line can be adapted to make Laugwitz-Schmieden an adequate model of this theory. This still needs Extraction Language Ocaml.

Extract Inductive prod => "(*)" [ "(,)" ]. Extract Inductive bool => "bool" ["true" "false"]. Extract Inductive sumbool => "bool" ["true" "false"].

Extract Inductive Z => "int" ["0" "(fun x -> x)" "(fun x -> -x)"]. Extract Inductive positive => "int" ["(fun x -> 2*x+1)" "(fun x -> 2*x)" "1"]. Extract Inductive list => "list" ["([])" "(::)"]. Extract Constant Z_of_nat => "(fun x -> let rec n2b x = match x with O -> 0 | S n -> (n2b n)+1 in n2b x)".

Extract Constant Zcompare => "(fun x y -> if (x=y) then Eq else if (x<y) then Lt else Gt)". Extract Constant Psucc => "(fun x -> x+1)". Extract Constant Pplus => "(fun x y -> x+y)". Extract Constant Pmult => "(fun x y -> x*y)". Extract Constant Pminus => "(fun x y -> x-y)". Extract Constant Pdouble_minus_one => "(fun x -> 2*x+1)". Extract Constant Zdiv_eucl_POS => "(fun x y -> (x/y, x mod y))". Extract Constant Zdiv_eucl => "(fun x y -> (x/y, x mod y))".

Extract Constant Zplus => "(fun x y -> x+y)". Extract Constant Zmult => "(fun x y -> x*y)". Extract Constant Zopp => "(fun x -> -x)". Extract Constant Zge_bool => "(fun x y -> x >= y)". Extract Constant Zgt_bool => "(fun x y -> x > y)".

Extract Constant A0_dec_weak_gen => "(fun x n -> if (x n<0) then (Inleft true) else if (x n=0) then (Inleft false) else (Inright))".

Extract Constant Zabs => "(fun x -> if x < 0 then -x else x)".

  Parameter A:Type. Parameter a0 a1 : A. Parameter plusA multA divA modA : A -> A -> A. Parameter oppA absA : A -> A.

  Parameter plus_neutral : forall x,0 + x = x. Parameter plus_comm : forall x y, x + y = y + x. Parameter plus_assoc : forall x y z, x + (y + z) = (x + y) + z. Parameter plus_opp : forall x, x + (-x) = 0. Parameter abs_pos : forall x, 0 <=|x|. Parameter abs_pos_val : forall x, 0 <=x -> |x|=x. Parameter abs_neg_val : forall x, x <=0 -> |x|=-x. [...]

  Parameter ANS4 : forall x, (exists y, lim y /\ | x | <= | y |)-> lim x.

  Parameter ANS5 : forall P :A -> Prop, (forall u : forall n:A, lim n /\ 0 <= n -> A, P (u 0 H0) -> (forall n:A, forall Hn : lim n /\ 0 <= n, (forall k:A, forall Hk:0 <= k /\ k <= n, forall Hn1 : lim (n+1)/\0 <=(n+1), P (u k (ANS4_special n k Hn Hk)) -> P(u (plusA n 1) Hn1))) -> {v:A->A | forall n:A, forall Hn:lim n /\ 0 <= n, forall k:A, forall Hk:0 <= k /\ k <= n, P (v k) /\ v k = u k (ANS4_special n k Hn Hk)}).

Fig. 1 .

 1 Fig. 1. An intuitive representation of HRω.

  Lemma Padd : forall x y, P x -> P y -> P (x + y).DefinitionHRwplus (x y: HRw) : HRw := match x with exist xx Hxx => match y with exist yy Hyy => exist P (xx + yy) (Padd xx yy Hxx Hyy) end end. Lemma Popp : forall x, P x -> P (-x). Definition HRwopp (x: HRw) : HRw := match x with exist xx Hxx => exist P (-xx) (Popp xx Hxx) end. Definition HRwminus (x y : HRw) : HRw := HRwplus x (HRwopp y). Lemma Pprod : forall x y, P x -> P y -> P (( x * y) / w). Definition HRwmult (x y: HRw) : HRw := match x with exist xx Hxx => match y with exist yy Hyy => exist P ((xx * yy) / w) (Pprod xx yy Hxx Hyy) end end. Definition HRwequal (x y : HRw) : Prop := match x with exist xx Hxx => match y with exist yy Hyy => (forall n, lim n ->0 < n -> ( (n*|xx + (-yy)|) <= w)) end end. Definition HRwgt (y x : HRw) : Prop := match y with exist yy Hyy => match x with exist xx Hxx => (exists n, lim n /\ 0 < n /\ (w <= (n*(yy+ (-xx))))) end end. Definition HRwge (y x:HRw) : Prop := match y with exist yy Hyy => match x with exist xx Hxx => forall n, lim n /\ 0 < n -> n * (xx + -yy) <= w end end. Definition HRwdiff (x y : HRw) : Prop := HRwgt x y \/ HRwgt y x. Lemma Pdiv : forall x , HRwdiff x HRw0 -> P ((w * w ) /(proj1_sig x)). Definition HRwinv (x : HRw) (H: HRwdiff x HRw0) : HRw := exist P ((w * w ) / (proj1_sig x)) (Pdiv x H).

Fig. 2 .

 2 Fig. 2. Definitions of HRω operations in Coq

A

  least upper bound is unique: if b and c are two least upper bounds of S, then we have ¬(b > ω c) and ¬(c > ω b); thus, according to the properties 8 of the relations > ω , ⩾ ω and = ω, we get c ⩾ ω b and b ⩾ ω c and then b = ω c.

  Definition subset := HRw->Prop. Definition least_upper_bound (S:subset) (b:HRw) : Prop := (forall s:HRw, (S s -> b >=w s)) /\ (forall b':HRw, (b >w b') -> exists o:HRw, S o/\ o >w b').

  Definition A := nat->Z. Definition a0 : A := fun (n:nat) => 0%Z. Definition a1: A := fun (n:nat) => 1%Z. Definition w :A := fun (n:nat) => (Z_of_nat n).

Definition 4 .

 4 Let a = (a n ) n∈N and b = (b n ) n∈N be two Ω-numbers, a and b are equal if there exists N ∈ N such that for all n > N , a n = b n .

Theorem 1 .

 1 The system HRω 10 has the following properties: (a) All the axioms of a BH-ordered field except BH2.(2), BH2.(3) and BH3.(2). (b) BH2.

  (c) BH2.(3)' If x, y ∈ HRω are such that x △ y and ¬(x ̸ =ω y), then x =ω y. (d) BH3.(2)' If S is a nonempty subset of HRω that is bounded above relative to the relation ⩾ω and such that for all (α, β) ∈ HR 2 ω where β is an upper bound of S and α ∈ S and for (a, b) ∈ HR 2 ω such that α ⩽ω a ⩽ω b ⩽ω β, either b is an upper bound of S or else there exists s ∈ S with s >ω a. Then there exists an element τ ∈ HRω which is a least upper bound of S in the following weak meaning: (I') ∀µ <ω τ, ∃s ∈ S such that µ <ω s (identical to (I)) (II') (∀ν ∈ HRω such that τ <ω ν)(∃b upper bound of S) τ ⩽ω b <ω ν

Fig. 3 .

 3 Fig. 3. The properties of HRω based on Laugwitz-Schmieden Ω-numbers (from [7])

Fixpoint

  LS_Euler_stepA beta a b (f:A * A -> A) m : list (A * A * A) := match m with | O => (a / beta, b / beta, b mod% beta)::nil | (S k) => let r := (LS_Euler_stepA beta a b f k) in let '(ttk, xtk, xhk) := hd (a0, a0, a0) r in let ftk := (f ((ttk * beta) + (a mod% beta) , (xtk * beta) + xhk)) / beta in ( ttk + a1, xtk + (xhk + ftk) / beta, (xhk + ftk) mod% beta ) :: r end.

Fig. 4 .

 4 Fig. 4. The arithmetization of the function t → t 2 6 . Graphs of the function t → x( t ) are drawn at different ranks of the given infinite integer sequences.

  Figure 6 provides an insight of the size of the development. All proofs are available online : http://dpt-info.u-strasbg.fr/~magaud/Harthong-Reeb/

Fig. 5 .

 5 Fig. 5. A simplified version of the extraction commands

Roughly speaking it says that if for a theory with infinitely many axioms, each finite subset of axioms has a model then the theory has a model.

Most statements in Coq are self-explanatory, when it becomes more technical, detailed explanations will be given.

An infinitely large number is the same as a non-limited number.

To do that, we use the definitions and axioms from the library Coq.Logic.ProofIrrelevance

These properties are not completely trivial in intuitionistic logic.

It requires copy-pasting the whole goal and using the change tactic to replace one term by the other, eventually making the system aware both terms are actually the same. Indeed, it actually agrees the 2 terms are convertible but can not perform any reductions leading from the first one to the expected one.