M Kanj

E Le Rouzic

D Amar

J L Auge

B Cousin

N Brochier

Optical Power Control to Efficiently Handle Flex-Grid Spectrum Gain over Existing Fixed-Grid Network Infrastructures

Keywords: GMPLS, Link Design, Flex-Grid, Power Control, Path Computation Algorithm

The exponential traffic growth in optical networks has triggered the evolution from Fixed-Grid to Flex-Grid technology. This evolution allows better spectral efficiency and spectrum usage over current networks in order to facilitate dynamic and huge traffic demands. The integration of Flex-Grid technology increases the number of optical channels established over optical links, leading, however, to an increase in amplification power and possibly saturating optical amplifiers.

In this work, we propose a power adaptation process that takes advantage of link optical signal to noise ratio (OSNR) margins to allow network operators to support this power increase while maintaining the use of legacy amplifiers. Results show that controlling channel optical power benefits from the Flex-Grid in terms of spectrum and capacity gain using in-place amplifier infrastructure.

I. INTRODUCTION

Internet services (video conferencing, cloud services and video streaming) and consequently traffic demands are increasing continually, leading to huge traffic growth in the core optical network. There is a need for network operators to increase their optical network capacity to follow this traffic growth. Since the deployment of new optical fibers is still very expensive, network operators are pushing to exploit the totality of their network capacity by optimizing their optical resources, and thus postponing the deployment of new infrastructures. This exploitation requires new technologies and flexible equipment that are able to handle different types of optical channels, from small to extremely high data rates [START_REF] Gerstel | Elastic optical networking: A new dawn for the optical layer?[END_REF].

Fixed-Grid technology is no longer qualified to handle the increasing data rates of optical channels. At the same time, the 50 GHz ITU grid, due to its fixed-spectrum spacing, produces losses of spectrum resources when the bandwidth occupancy of the established demands is smaller than (or is not an exact multiple of) the size of the allocated spectrum slots [START_REF] Wright | The network capacity benefits of Flexgrid[END_REF].

The ITU recommendation G.694.1 [START_REF]Spectral grids for WDM applications: DWDM frequency grid[END_REF] for a Flex-Grid optical network has defined a new flexible spectral grid standard for wavelength division multiplexing (WDM) applications. This flexible spectral grid has a smaller slot granularity of 12.5 GHz, with nominal central frequency on a grid of 6.25 GHz spacing compared to the currently 50 GHz Fixed-Grid. This recommendation has made the Flex-Grid a promising technology that is capable of following traffic growth and various traffic demands. Flex-Grid efficiently uses available spectrum resources, especially when associated with novel coherent transmission technologies and advanced modulation formats.

Switching from Fixed-Grid to Flex-Grid technology has an impact on the optical amplifiers of an already deployed optical network. Indeed, the optical amplifiers present at the end of each successive span constituting an optical link and in switching nodes are designed and engineered for a Fixed-Grid WDM network. Since Flex-Grid technology allows the reduction of channel spacing, it allows the possibility to create new optical channels over the saved spectrum. However, this increase in the number of optical channels increases the optical power injected in optical links and may cause unwanted impairments due to the saturation of some amplifiers in the already deployed network.

In the literature, several studies have focused on developing accurate physical impairment estimators over uncompensated links. They have demonstrated the existence of an optimal optical power channel that leads to minimum impairment generation and thus achieves better transmission performance (maximum reach) [START_REF] Poggiolini | The GN Model of Non-Linear Propagation in Uncompensated Coherent Optical Systems[END_REF] [5] [6] [START_REF] Bosco | Performance prediction for WDM PM-QPSK transmission over uncompensated links[END_REF]. Others have focused on improving link performances (achieving SNR margin gain) and thus increasing network throughput by adapting channel launch power and optimizing spectral resources and modulation formats without taking into account power resource limits over optical links [START_REF] Ives | Transmitter optimized optical networks[END_REF] [START_REF] Ives | Adapting Transmitter Power and Modulation Format to Improve Optical Network Performance Utilizing the Gaussian Noise Model of Nonlinear Impairments[END_REF].

In this paper, unlike the current paradigm that aims to optimize channel power to their optimum values regardless their reaches, we propose to control and adapt the power of these channels to their minimum required performances (adaptation to the real physical reach). This enables optical power margins to be used for overcoming the power limitation of amplifiers when increasing the number of channels over network links. For this purpose, we propose a distributed generalized multi-protocol label switching (GMPLS)-based control plane with resource reservation protocol-traffic engineering (RSVP-TE) and open shortest path first-traffic engineering (OSFP-TE) protocol modification that implements this power control process. Performance of the novel scheme is demonstrated with simulations.

This paper is organized as follows. Section II presents an overview of optical network design issues. Section III introduces the link power margin and our design method. Section IV presents the power control process. Section V presents GMPLS protocol modifications made to implement the power control process and its associated path computation algorithm. Section VI presents simulated scenarios and results. Conclusion and future works are presented in Section VII.

II. OPTICAL LINK DESIGN AND POWER LIMITATIONS

We consider a set of successive optical spans constituting an optical link between two optical nodes (e.g., reconfigurable optical add-drop multiplexers; ROADMs) as shown in Fig. 1. The optical link design consists of choosing the set of optical amplifiers that can compensate for span losses and simultaneously support the optical power of the total number of channels planned for that link, while seeking maximum optical performance. The link design has the objective of maximizing OSNR, minimizing linear and non-linear effects. Complexity of the process arises in particular because of the contradictory objectives of amplifiers; they must compensate for link span losses, satisfy the aggregate optical power for all optical channels sharing the fiber, and simultaneously minimize the amount of generated noise.

Pdesign,l

Gn-1 As explained in the previous section, links in current Fixed-Grid WDM networks are designed to support a given number of channels (N channel max ). In general, every link (l) has its own N channel max,l ; however, to ease our study, without any loss of generality, we assume that these numbers are identical all over the network. The use of Flex-Grid technology in these infrastructures may increase the number of channels in some links and thus their optical power level.

In fact, if the number of channels is not controlled and limited, there may be some risks of power saturation in the amplifiers that are already close to their maximum output power (power saturation limit) with the initial N channel max , leading to strong performance degradation on these links. Inversely, if the number of channels is limited to N channel max , the spectrum gain enabled by Flex-Grid technology cannot be exploited. Replacing optical amplifiers with new ones having bigger output power is a potential solution, but costly since it requires buying new amplifiers, interruption of the link, and full redesign. In this paper, we propose to make the information of optical power available to the control plane to benefit from Flex-Grid spectrum gain promises, while keeping the in-place amplifiers.

It is noteworthy that, at the end of design step, amplifiers are used in a fixed gain mode, which means that once the design step is finished, adjusted amplifier gains are never changed.

III. LINK POWER MARGIN DEFINITION AND NOVEL DESIGN

METHOD

As a first step, we propose to control the optical power to benefit from the unused power left in each amplifier once the network is designed and deployed, which we call link power margin.

A. Link Power Margin

Let N channel max be the maximum number of channels per each link. Let P design,l (P 1 ) be the input optical power designed for the link l having N channel max . The difference between all span characteristics (losses, non-linearity coefficient, and length) leads to the use of different types of amplifiers with different characteristics in terms of maximum gain (G OA max ), maximum power (P OA max ), or noise figure (N F ) for each span. This variation results in having over every link l, different P design,l and thus P channel,l (individual channel power over link l). This P design,l when applied at link l input, results in different span input powers depending on span attenuation and amplifier configured gains when going through the link. Therefore, there is a power margin (P OA margin,n ) over the n th amplifier such that P OA margin,n = P OA max,n -P n+1 , where P n+1 is the power at the input of the n + 1 th span.

We define as link power margin P margin,l , the minimum power margin that exists over the amplifiers of link l. Therefore, the maximum optical power that can be applied at the input of link l without saturation of any amplifier is P max,l = P design,l + P margin,l . Our utilization of power margin complements recent works on design margins and system margins, as in [START_REF] Auge | Can we use flexible transponders to reduce margins?[END_REF] [11] [12]. In these works, the power control aspect was neglected. Here, we specifically focus on the control of the optical power. However, this requires fine knowledge of the maximum power allowed in each link, which in turn requires understanding of the link design step and the limitations of optical links.

B. Design Method

In order to evaluate our power control process, we have to precisely model the link design step. To this end, we have developed a link design method, which we briefly presented in [START_REF] Amar | On legacy amplifier limitation in flexgrid optical networks[END_REF], taking advantage of the optimization strategy presented in [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF]. Note that our proposed power control can work with any other design method. The LOGON strategy proposed in [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF] consists of performing a local optimization of the optical signal to noise ratio (OSNR) and non-linear impairments at span level, leading to a global OSNR optimization over all the links of the network. Therefore, it proposes to apply an optimal power spectral density at the input of every span, calculated using span and amplifier characteristics by applying formula [START_REF] Carena | Modeling of the Impact of Nonlinear Propagation Effects in Uncompensated Optical Coherent Transmission Links[END_REF] in [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF].

Eq.( 1) represents the aggregated optical power that corresponds to this power spectral density at the n th span input for N channel max channels having R s spectrum width each, where h, µ, F n , and ρ N LI,n stand for Planck's constant, the electromagnetic wave frequency, the NF of the n th amplifier, and non-linear effect contribution respectively.

P n = hµF n 2ρ N LI,n 1 3
(1)

F n = F 1,n + F 2,n D n G OA max,n G 2 n ( 2
)
G n = a n P n+1 P n (3)
Our link design method consists of choosing the optical amplifier that satisfies the link design constraints (maximize OSNR, minimize non-linear effect, satisfy N channel max power, and compensate for span loss). Each amplifier NF is calculated using Eq. ( 2), and varies according to the adjusted gain G n . We use variable gain dual-stage amplifiers without mid-stage access where F 1,n and F 2,n are the NF for the first and the second stage, respectively, and D n denotes the power ratio for both stages to account for the difference between preamp and booster performance. Eq. ( 3) calculates the desired amplifier gain (G n ) to compensate for span loss, where a n is the attenuation of the n th span, P n is the power at the input of the n th span, and P n+1 is the power at the output of the G n optical amplifier as shown in Fig. 1. We replace F n in Eq. ( 2) by its value in Eq. ( 1), and then the P n in Eq. ( 3) by its value of Eq.( 1) to attain a third degree polynomial equation represented by Eq. ( 4), which we solved analytically. The solution of this equation in Eq. ( 5) gives us the value of the gain that should be adjusted in the n th amplifier in order to obtain minimum linear and non-linear impairment generation.

hµF 1,n G 3 n +hµF 2,n D n G OA max,n G n -2ρ N LI,n a 3 n P 3 n+1 = 0 (4)
G n = 4F 2,n D n G OA max,n 3F 1,n × sinh   1 3 asinh   ρ N LI,n (a n P n+1 ) 3 27F1,n (F2,nDnGOA max,n) 3 hµ     (5)
Our link design is performed from the last span to the first one; the amplifier that can satisfy both required gain (G n ) and optimum power (P n+1 ), while achieving the smallest NF is selected. If none of the amplifiers can satisfy these requirements, the one with the closest maximum power (P OA max ) is chosen. The difference of the required power is subsequently recovered by re-tuning the gain(s) of the following (downstream) amplifier(s).

IV. OPTICAL POWER CONTROL Optical networks are made of optical nodes (ROADMs) interconnected with optical links. In order to achieve maximum network performance, every optical link between two ROADMs is usually designed to support optimum performance independently from other links. With this design method, every link has its own set of optimum span powers and amplifier settings. In this configuration, maximum performance is ensured by setting the optimum power for any new optical channel to P channel,l [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF]. This kind of policy does not take into account the fact that channels may require variable reaches; thus some channels may not need the maximum performance (e.g., the channel with the shortest path). As a result some power transmission margins are wasted.

The channel performance and its optical power are tightly linked. Reducing the optical power from its optimum value to a lower value reduces the performance and thus adapts the channel to the required reach. This appears as an interesting method to save some power in a Flex-Grid network and to avoid wasting power transmission margin. More precisely, we expect that this power adaptation will allow the use of the saved margin to increase link capacity in terms of channel number.

To perform the power control, we now propose exploiting the performance estimator of equation ( 5) of the LOGON strategy in [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF]. This equation estimates the OSNR (including non-linear effects in the form of non-linear interference) at the receiver side. If the estimated OSNR (OSN R est ) is bigger than the required one (OSN R req ), then we can adapt channel power. The OSNR value of a lightpath made of successive links is the inverse of the sum of the inverse OSNR of each link [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF]. Because OSNR is proportional to channel power and LOGON is already the worst case in terms of nonlinear effects (OSNR overestimation supposing full spectrum load), approximatively every 1 dB of optical power reduction corresponds to 1 dB of OSNR reduction [START_REF] Vacondio | On nonlinear distortions of highly dispersive optical coherent systems[END_REF]. Therefore, as a simplified first guess, we assume that the OSNR margin in dB (OSN R margin = OSN R est -OSN R req ) corresponds to the amount of power that can be saved for the related optical channel.

Moreover, since amplifiers have a fixed gain (tuned according to the method explained earlier), this OSNR reduction is simply obtained by tuning the power at the transmitter side: a x dB of optical power attenuation at the transmitter side corresponds exactly to x dB of power attenuation at the receiver side when passing though the set of spans and amplifiers constituting the optical links. The estimation of the power that can be saved is a rough but simple assumption that can be easily integrated into a control plane. Other methods relying on more complex computation or monitoring mechanisms can be proposed.

V. GMPLS PROTOCOL AND ROUTING ALGORITHM A. GMPLS Protocol Modifications

Due to the lack of space, the routing and signaling process descriptions of OSPF-TE and RSVP-TE, in addition their extensions that are using new collected physical parameters are briefly presented. A detailed description will be the topic of the next publication.

At the end of the design step, every optical link has its own set of configurations for its optical amplifiers; gain and power settings allow computing performance estimator OSNR (equation ( 5) in [START_REF] Poggiolini | The LOGON strategy for lowcomplexity control plane implementation in new-generation flexible networks[END_REF]). Since no previous work in the domain or any of the IETF RFCs have proposed protocol extensions to include power information for OSPF-TE, we propose modifying it to collect new physical information from the optical plane: P channel,l , P design,l , and P margin,l , link OSNR as defined in the previous section and real time link power (P (t) real,l ). We assume that the first four parameters are configured for each link and recorded in the neighboring nodes upon link commissioning. Then, they are collected from the optical plane and placed in the OSPF-TE link state database. The fifth parameter P (t) real,l is the effective aggregate optical power in the link. It depends on the number of optical channels established at a given t moment. It is updated upon each lightpath setup or release based on optical power computation.

The P ath and Resv messages used in the signaling protocol RSVP-TE are also modified to take into account the optical power recommended setting for the lightpath. This enables optical nodes to perform power verification tests during the light path setup (in addition to the wavelength availability test that is usually done). A path computation algorithm was developed to compute paths according to the TE link parameters that we added in the OSPF-TE database.

B. Routing Algorithm

To find an available and feasible lightpath that satisfies every connection request, we propose the path computation algorithm shown in Fig. 2 and detailed here. For every connection request (i.e., lightpath) between a pair of sources and destination nodes of T Gbit/s rate, it calculates the shortest path using the Dijkstra algorithm. Then, it tries to find a group of S available slots of 12.5 GHz that satisfy the T demand (S slots are calculated with respect to minimum spectrum occupation, supposing one and the same modulation format for all demands), which are continuous and contiguous using the First-Fit algorithm. The demand is blocked when no available slots are found to satisfy the connection request.

Once this set of free successive optical slots over the path is found, three other tests are performed physical feasibility test, power adaptation (PA), power verification (PV). The physical feasibility test checks whether OSN R est is above OSN R req . If the path is physically feasible, then OSN R margin , which is the difference between OSN R est and OSN R req , is computed. If OSN R margin exists, then a channel power adaptation can be made to adapt the optical channel to minimum performances (OSN R req ). In this case, the channel power reduction is equal to the OSN R margin value, and the target optical power for the channel is P adapted channel = P channel -OSN R margin . Regardless of the adapted channel power value, a last power verification test is performed to ensure that this channel, if added, will not cause any saturation problems over the links constituting the optical path. This test consists of comparing the value of the link aggregate power P (t) real,l when adding the new channel (+P adapted channel,l ) with the maximum allowed power (P design,l + P margin,l ) over every l link constituting the path. These values are made available at each node due to the OSPF-TE link state distribution process. Once these tests are done at the ingress node, the signaling is triggered on the chosen path (i.e., a RSVP-TE P ath message is sent downstream in order to set up the optical channel). If any of these tests fails, the connection request is rejected.

Lastly, at each hop, during the signaling process, the aggregate power using the recommended channel power setting is checked in order to verify that it does not exceed the P max,l of each crossed link. Indeed, if the requests are very frequent, some signaling process may simultaneously compete for the same optical resources in terms of optical power (race condition) and the signaling should avoid any overprovisioning due to the not-yet-updated link database.

VI. SIMULATION SCENARIO AND RESULTS

A. Simulation Setup and Scenarios

In order to test and evaluate the potential gain of our proposed power control, we developed a distributed GMPLSbased network simulator over OMNET++. It simulates OSPF-TE and RSVP-TE protocol messages and mechanisms.

We assume that the same initial link design is performed for eighty 100 Gbit/s QPSK channels over a 50 GHz grid (80*50 GHz = 4 THz per link) for all scenarios. However, the full usable bandwidth is set to 4.8 THz (optical amplifiers usable bandwidth).

Simulations are performed over the 32 optical nodes and 42 optical links of the European backbone network shown in Fig. 3. Single mode fiber spans are used (chromatic dispersion = 17 ps.nm -1 .km -1 , fiber attenuation = 0.22 dB/km, non-linearity coefficient = 1 W -1 .km -1 ). Links are designed using the three amplifier types presented in Tab. I, and assuming non identical span lengths that are randomly drawn according to a realistic distribution. Filtering penalties induced by transit across one optical node are 0.05 dB for the 50 GHz channel spacing and 0.64 dB for the 37.5 GHz [START_REF] Amar | How problematic is Spectrum Fragmentation in operator's Gridless network?[END_REF]. Tab. I shows the amplifier portfolio comprising several variable gain dual-stage amplifiers without mid-stage access with fixed parameters (P OA max , G OA max , F 1 , F 2 , D). In order to simplify the results analysis, just 100 Gbit/s optical channels are established in all scenarios. The minimum accepted OSNR at the receiver side, using 0.1 nm noise reference bandwidth, including operational margins, is set to 15 dB for 100 Gbit/s QPSK modulation format with coherent detection and soft decision forward error correction (FEC), whatever the channel bandwidth (three or four slots of 12.5 GHz). Five scenarios are studied:

• Fixed-Grid (FG): This scenario represents today's core optical networks where no power information is communicated in the control plane. The power control block is not activated in the path computation algorithm or in the protocol. The number of channels that can be set up on a given link is thus limited to 80, as no other information has been made available, and each channel occupies four contiguous slots.

• Fixed-Grid with power margins (FG4S PV): In this scenario, the control plane is power aware and thus benefits from the extra power margin of every link (P margin,l ) to set up channels in the limit of the 4.8 THz bandwidth. The power adaptation block is off, but the power verification is on. Each channel occupies four contiguous slots.

• Fixed-Grid with power control and power margins (FG4S PA+PV): In this scenario both power adaptation and power verification are allowed. Each individual channel power is tuned to the power satisfying the minimum accepted OSNR value (OSN R req ). Each channel occupies four contiguous slots.

• Flex-Grid with power control and power margins (FX3S PA+PV): This scenario is the same as FG4S PA+PV but each channel occupies three contiguous slots.

• Flex-Grid with power control and power margins (FX3-4S PA+PV): Same as previous scenario, but with the possibility to choose three or four slots of 12.5 GHz for the 100 Gbit/s channels. The path computation algorithm first assumes three slots of 12.5 GHz for the channel setup. In case the path is not physically feasible (filtering penalty is much higher for three slots than for four slots), the algorithm tries to establish the optical channel using four slots. Note that in all scenarios, paths that exceed maximum reach (i.e., with OSNR below OSNRreq) are rejected, and we have not implemented regeneration (left for further work).

Fifty simulation runs (with different random seed numbers) were performed for each of the five scenarios with an incremental channel setup (no channel is released). The results depicted in Fig. 4 and 5 are given by averaging the 50 simulation runs with a confidence interval of 95% (too small to be displayed on the figures). The demand request inter-arrival time in each node follows an exponential law with λ = 0.4. Demand source-destinations are randomly chosen among all source-destination pairs according to a uniform distribution.

B. Simulation Results

We consider the cumulative blocking probability (CBR) as a first evaluation criterion, which is the ratio of the total number of blocked requests to the total number of generated requests until a time t. Figure 4, shows the CBR of the five scenarios as a function of the normalized spectrum occupation of the network, which is the ratio of the total occupied spectrum over all the links of the optical network until a time t to the total spectrum of all the links. Note that on each link, the spectrum occupation corresponds to the number of reserved slots of all channels, each one having three or four slot occupations depending on the scenario.

For all scenarios, CBR at low occupation is not zero because of the rejected demands due to physical feasibility (paths longer than maximum reach). Not surprisingly, since FX3S PA+PM has a larger filtering penalty, it blocks more demands at low occupation than the other scenarios.

Moreover, FG and FG4S PV have the same CBR until approximatively 65% of spectrum occupation. Over 65% occupation, the CBR of FG4S PV is smaller because the network benefits from power awareness; it can accept more than 80 channels relying on the remaining power margins over the links. Further, FG4S PA+PV has a smaller CBR than FG and FG4S PV because it can not only benefit from the power margin, but it can also generate some power reduction with channel power adaptation. The CBR of FG4S PA+PV stays below the CBR of FG and FG4S PV starting from approximatively 26% of spectrum occupation. This means that even at low load, the power reduction enabled by the proposed power control mechanism can be useful. We also noticed that blocking for FG4S PA+PV is only due to physical feasibility and bandwidth availability reasons even at high load, and upon closer investigation of the optical power levels, we noticed that this scenario is not limited by the optical power availability. As explained earlier, the FX3S PA+PV scenario has bigger CBR at a low occupation ratio because it uses only 37.5 GHz spacing for establishing the 100 Gbit/s channels; the filtering penalty (0.64 dB) then reduces the number of feasible paths in the whole network. However, when network load increases, the FX3S PA+PV CBR is lower than the CBR of FG and FG4S PV CBR. This is explained first because with three slots per channel, the network can accept more channels than with four slots, and second because the power required for these additional channels has been made available by the control process (PA + PV).

This analysis is confirmed with the FX3-4S PA+PV scenario. It has a CBR smaller than FX3S PA+PV for spectrum occupation lower than 65% because paths rejected due to their non-physical feasibility with 37.5 GHz are established here with 50 GHz. Nonetheless, this is paid with lower spectrum efficiency; the spectrum fragmentation caused by the mixing of 37.5 GHz and 50 GHz channels (no spectrum fragmentation aware spectrum assignment) prevents using the whole spectrum bandwidth unlike FG4S PA+PV and FX3S PA+PV. This is also confirmed in Fig. 5.

It is important to note that the spectrum efficiency of the FX3S PA+PV is slightly smaller than FG4S PA+PV since some links still have spectrum resources but their power resources are completely used at high loads. This is because setting up only three slot channels not only increases the number of channels but also decreases the potential for power saving over links: power adaptation performs less power margins because of the high filtering penalty (0.64 dB).

We notice that with this network design the amount of P margin,l of the links is too small to satisfy more than 80 channels (link power margins represent approximately 2.5% of the available power over the network). In this situation, the power adaptation process is able to save enough power to cancel the blocking for power reasons; scenarios using PA FG4S PA+PV, FX3S PA+PV, and FX3-4S PA+PV have approximately 52%, 25%, and 35%, respectively, of remaining power over the entire network (sum of the remaining power over network links).

Figure 5 shows the network capacity (amount of 100 Gbit/s demand accepted and established) as a function of the normalized spectrum occupancy. Note that a four-slot 100 Gbit/s demand going through three optical links (three hop path) for example, will count as 100 Gbit/s on the y-axis and 3*4 slots (3*50 GHz) on the x-axis. This explains why the FG4S PV and FG4S PA+PV curve is below the FG one, in addition to the fact that accepted demands in FG4S PV and FG4S PA+PV have longer reaches (number of hops) at high load where power blocking appear in FG. This explanation also holds for FG4S PV versus the FG curve, and it is particularly visible in the FX3S PA+PV scenario, which has much shorter paths on average than all the other scenarios. The FG, FG4S PV, and FG4S PA+PV reach 137.8 Tbit/s, 158.2 Tbit/s, and 173.3 Tbit/s, respectively, of carried traffic. Therefore, the power control has increased the capacity of the Fixed-Grid network of approximately 25%. As expected, the power control coupled with the use of the Flex-Grid with FX3S PA+PV greatly increases the network capacity to 248 Tbit/s. This represents 80% of the capacity increase compared to FG (i.e., accounting for the 0.8 THz more total spectrum resource) and 45% when compared to FG4S PA+PV. We also note that the Flex-Grid scenario mixing three and four slot channels has a larger capacity than FG4S PA+PV despite the fact that it can occupy less spectrum. These results mean that power control with power adaptation is an efficient mechanism to benefit from the link total spectrum bandwidth, without the need to re-design the existing optical network.

VII. CONCLUSION

In this paper, we have addressed the optical amplifier power limitation issue that an operator network planner will face when migrating networks from Fixed-Grid to Flex-Grid networks. Using a developed link design method that we detail in this paper, we have proposed a channel power control process with power information distribution, power verification, and power adaptation. We also describe a path computation algorithm that includes power control and show how the whole process can be integrated into a distributed GMPLS-based control plane. We suggest several modifications for the existing OSPF-TE and RSVP-TE protocols to include power information.

It is important to emphasize that our power control process is completely independent from link design, OSNR estimator, or control plane protocol. Any other link design method associated with any OSNR estimator could be used to perform the power control.

Simulation results revealed that the power control process is an efficient way to benefit from Flex-Grid capacity promises while maintaining the use of legacy amplifiers without the need to re-design any links in the network. Future work will include other network topologies, in addition to a detailed description of control plane protocol extensions and mechanisms for OSPF-TE and RSVP-TE protocols to be able to apply the power control over a distributed-GMPLS based network. The power control process will also be evaluated in the dynamic case where connections are established and released.

Fig. 1 .

 1 Fig. 1. Simplified representation of an amplified link (succession of a fiber span and optical amplifier) between two ROADMs.

Fig. 2 .

 2 Fig. 2. Path Computation Algorithm.

Fig. 3 .

 3 Fig. 3. European Backbone Network Topology.

Fig. 4 .

 4 Fig. 4. Cumulative Blocking Ratio vs. Normalized Spectrum Occupation.

Fig. 5 .

 5 Fig. 5. Network Throughput vs. Normalized Spectrum Occupation.

ACKNOWLEDGMENTS

This work was partly supported by the DGCIS, in the frame of the CELTIC-Plus project SASER-SIEGFRIED.


Pierre Boutry
email: boutry@unistra.fr

Julien Narboux
email: narboux@unistra.fr

Pascal Schreck
email: schreck@unistra.fr

A reflexive tactic for automated generation of proofs of incidence to an affine variety

Keywords: Automation, computational reflection, geometry, incidence, formalization, Coq

This paper describes the formalization and implementation of a reflexive tactic for automated generation of proofs of incidence to an affine variety. Incidence proofs occur frequently in formal proofs of geometric statements. Nevertheless they are most of the time omitted in pen-and-paper proofs since they do not contribute to the understanding of the proof in which they appear. Our tactic allows us to automate proofs about incidence to an affine variety. Being based on a type class capturing the minimal set of properties needed to deal with incidence, the tactic is applicable to any theory verifying these properties. This type class is defined using dependent types to formalize predicates of parameterizable arity which represent the incidence to an affine variety.

Introduction

The following research was conducted as part of a larger project which focuses on the use of proof assistants in an educational framework to teach reasoning principles. We believe that geometry is a good subject to study in order to understand the proof process. Our long term goal consists in the development of an interactive software based on Coq in which students can write their own proofs. In the context of education, Hilbert's and Tarski's axiomatic developments possess the advantageous quality of not being based on set-theoretical notions. As a basis for these tools and libraries, Tarski's system of geometry was chosen for its well-known metamathematical properties. Yet the absence of set-theoretical notions has its drawback.

For instance, it induces incidence proofs to become particularly tedious. This issue also arises in Hilbert's axiomatic development while straight lines are nevertheless considered. To illustrate how often incidence proofs occur we made some statistics. We studied our formal development (GeoCoq) of Tarski's geometry which is mainly a formalization of [START_REF] Schwabhauser | Metamathematische Methoden in der Geometrie[END_REF]. Approximately one seventh of the lines of the proof script contains applications of lemmas about collinearity of points. And almost a third of the lemmas of our development have as hypothesis the collinearity of some given points. One should point out two facts which allowed us to lower the ratio of incidence proofs present in our development. Firstly most of the incidence proofs are produced using some automatic tactics, therefore their length is greatly reduced. Secondly we restricted ourselves to the formalization of two-dimensional euclidean geometry. Thus the greater part of the incidence proofs corresponds to proofs about collinearity.

The particularity of incidence proofs is that they are omitted in pen-and-paper proofs while they are subject to combinatorial explosion. These proofs are omitted as they do not contribute to the understanding of the proof in which they appear. This particularity calls for a procedure to automate these proofs. In this paper we describe the reflexive tactic we developed to deal with this issue. Our early version of the tactic was specifically conceived to handle the case of collinearity. We then realized that our approach could be generalized in order to deal with incidence to an affine variety. As well as automating the incidence proofs our tactic allowed us to achieve a higher readability of our proof scripts.

Geometry is a successful area of the field of automated theorem proving. Several efficient methods have been developed. The most popular ones are the Gröbner basis method [8], Wu's method [START_REF] Chou | Mechanical Geometry Theorem Proving[END_REF][START_REF] Wang | Elimination Methods[END_REF][START_REF] Wu | On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry[END_REF], the area method of Chou, Gao and Zhang [START_REF] Chou | Machine Proofs in Geometry[END_REF], geometric algebra [START_REF] Li | Automated Geometric Theorem Proving, Clifford Bracket Algebra and Clifford Expansions[END_REF]. It is to be noticed that a decision procedure for the theory we are using was given by Tarski [START_REF] Tarski | What is Elementary Geometry[END_REF]. Some of these methods have been formalized in Coq: the second author formalized the area method [START_REF] Janicic | The Area Method : a Recapitulation[END_REF][START_REF] Narboux | A Decision Procedure for Geometry in Coq[END_REF], Pottier and Théry formalized the Gröbner basis method [START_REF] Grégoire | Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving[END_REF][START_REF] Pottier | Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics[END_REF][START_REF] Théry | A Machine-Checked Implementation of Buchberger's Algorithm[END_REF], Genevaux et al. extended this work to Wu's method [START_REF] Genevaux | Formalization of Wu's simple method in Coq[END_REF], Fuchs and Théry formalized a procedure based on geometric algebra [START_REF] Fuchs | A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry[END_REF]. But in this paper, as we aim at applications in the education, we are not interested in obtaining the most powerful prover which automates the whole proof. On the contrary we want to automate only the proof steps which are usually implicit in a pen-and-paper proof. The basis for this work is the mechanization in Coq of Tarski's axiomatic development about geometry. This library called GeoCoq has already been described in our previous work [START_REF] Boutry | Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski's system of geometry[END_REF][START_REF] Braun | From Tarski to Hilbert[END_REF][START_REF] Braun | A synthetic proof of Pappus' theorem in Tarski's geometry[END_REF][START_REF] Narboux | Mechanical Theorem Proving in Tarski's geometry[END_REF]. But for the sake of modularity we defined a type class capturing the minimal set of properties needed to apply our tactic. Our tactic is then applicable to any theory verifying these properties and is thus not restricted to Tarski's system of geometry.

Our work share some motivations with the work of Phil Scott and Jacques Fleuriot [START_REF] Scott | Mechanising Hilberts foundations of geometry in Isabelle[END_REF][START_REF] Scott | A Combinator Language for Theorem Discovery[END_REF]. They propose a framework to add domain-specific automation and apply it to the case study of Hilbert's geometry. Their approach consists in using the idle computation time to generate new facts using a given set of lemmas in a forward manner. Our method is different, it is specific for incidence problems. Hence it is more efficient because as we know the kind of data we manipulate, we can use a suitable data structure.

Automating the proof steps that are implicit in Euclid's proofs is done by Avigad et al. [START_REF] Avigad | A formal system for euclids elements[END_REF].

The rest of the paper is organized as follows. Section 2 describes the issue in the context of a simple example in elementary geometry. Section 3 presents a reflexive tactic to deal with the pseudotransitivity of the collinearity predicate. In section 4, we generalize our approach to other predicates.

Illustration of the issue through a simple example

For the sake of clarity, we present the simple example of the midpoints theorem. We will present a proof which contains an incidence proof. This will allow us to illustrate the issue that arises while doing an incidence proof. The statement of this theorem is the following.

THEOREM 1. In a non-degenerate triangle ABC where P is the midpoint of segment BC and Q the midpoint of segment AC, the lines AB and P Q are strictly parallel1 .

First we give the (slightly incorrect) informal proof which is often given in class. PROOF 1. We first construct point X as the symmetric point of P with respect to Q. Point Q is therefore the midpoint of segment P X.

From the assumptions we know that Q is also the midpoint of AC. Thus, the diagonals of the quadrilateral AP CX bisect in their midpoint and hence AP CX is a parallelogram. Now according to the fact that the opposite sides of a parallelogram are parallel and have the same length, we have that AX and CP (or BP ) are parallel and AX ≡ CP . As we know that P is the midpoint of BC we also have AX ≡ P B. The quadrilateral AXP B has two opposite sides which are parallel and of the same length, hence it is a parallelogram. Finally the opposite sides of a parallelogram are parallel, thus AB and P Q are parallel.

Formalizing this simple proof is not as trivial as it seems.

Firstly, for a good reason: actually, this proof is not correct because from the fact that the opposite sides of a quadrilateral ABCD are parallel and of the same length we can only conclude that either ABCD or ABDC is a parallelogram. Proving that one is a parallelogram rather than the other is not trivial and should not be omitted. The possibility of overlooking the fact that in order to prove that ABCD is a parallelogram we also need to prove that ABDC cannot be a parallelogram motivates the use of a proof assistant.

Secondly, for some bad reasons: this proof contains proof steps which are implicit in a pen-and-paper proof that a proof assistant forces us to detail. Degenerate cases appear extremely often in geometry and correspond to cases of incidence of two geometric objects. These cases generally do not appear in pen-and-paper and contribute greatly to the difficulty of generating a proof of a geometric statement. Either the statement that we wish to prove holds in the degenerate case. Then one usually needs to prove the incidence of other pairs of geometric objects in order to prove the statement in the degenerate case. Or it does not and then an extra hypothesis is needed. This hypothesis is often referred to as a non-degeneracy condition and corresponds to the negation of the incidence of two geometric objects. This extra hypothesis will generate a proof obligation which will often be proven by proof of negation2 . The contradiction will then be shown through an incidence proof.

Therefore handling degenerate cases will most of the time result in incidence proofs. The proof of midpoints theorem features such handling of degenerate cases. Indeed one cannot directly deduce that lines AB and P Q are parallel from the fact that ABP X is a parallelogram. In fact this statement is only true when the parallelogram is non-flat. Thus one needs to prove that three of the four points defining the parallelogram are non-collinear. So let us prove A, P and X are non-collinear by proof of negation. Assuming that A, P and X are collinear one can obtain a contradiction by proving that A, B and C are collinear with following proof script. In this script there are six occurrences of lemmas dealing with permutation properties of the predicate Col designating the collinearity of an ordered triple of points. These lemmas correspond to

∀ABCσ, σ ∈ S {A,B,C} ⇒ Col A B C ⇒ Col σ(A) σ(B) σ(C)
where SX denotes the symmetric group on a finite set X. To avoid the definition of the symmetric group we proved one lemma for each element of the group but the identity element.

Moreover there are three occurrences of lemmas handling the pseudo-transitivity of this same predicate. These lemmas correspond to

∀P QABC, P = Q ⇒ Col P Q A ⇒ Col P Q B ⇒ Col P Q C ⇒ Col A B C
where A was chosen so that the first collinearity is trivially satisfied from

∀AB, Col A A B
which expresses that two points are always collinear. The lemma of pseudo-transitivity can be understood as the possibility of proving that three points are collinear if they all belong to the same line. The extra hypothesis is needed to ensure that the points really belong to a well-defined line.

Even if we believe that in the context of education it is important to mention that the parallelogram should be non-flat we would like the incidence proof corresponding to the proof of negation to be done automatically. Indeed besides corresponding to proof steps that should be implicit as they do not bring any understanding of the proof, its proof script is tedious to produce because of the combinatorics underlying the pseudo-transitivity of collinearity. In the next section we expose the reflexive tactic we developed to automatically prove collinearity properties.

A reflexive tactic for dealing with permutation properties and pseudo-transitivity of collinearity

In order to simplify the proving process and to improve readability, we defined a tactic which can prove automatically collinearity properties which are consequences of this pseudo-transitivity.

Our first approaches to deal with this problem were to use the built-in automation of Coq (by creating a base of hints for the Coq tactic eauto) and then to write an ad hoc tactic in the tactic language of Coq. However this approach was not fulfilling our needs as it could not cope with difficult problems in a reasonable time. We therefore opted for a different approach. We chose to implement a reflexive tactic to handle this problem. First introduced in Coq by Samuel Boutin [START_REF] Boutin | Using reflection to build efficient and certified decision procedures[END_REF], reflexivity consists in replacing a tactic by an algorithm written in the Coq language and proving that the algorithm is sound. The reader interested in learning more about this now standard approach can also read the last chapter of the Coq'Art [START_REF] Bertot | Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions[END_REF]. Using a reflective tactic allows us not only to save the user from doing the tedious work about the pseudo-transitivity of collinearity but also it hides these steps from the proof term. The algorithm used by this tactic is described in the following paragraph.

Algorithm

The algorithm is divided into three parts. The first one consists in the initialization phase: it computes the set of all the sets of points known collinear and the sets of pairs of points known distinct. The second part consists in updating our internal data structure to compute the sets of points on each line. Finally we check if three given points are collinear by testing if they belong to a single line. For our algorithm we need a set of sets of points L to represent the sets of points known to be collinear and a set of pairs of points D to represent the points known to be different.

The algorithm is as follows: INPUT: 3 points A B C and the current hypotheses.

1. Initialize L so that it contains all sets of three points that are assumed to be collinear by the hypotheses in the context and D so that it contains all the pairs of points that are assumed to be different by the hypotheses in the context.

2. For every l1 and l2 in L such that there exists a pair (p1, p2) in D such that p1 ∈ l1 ∩ l2 and p2 ∈ l1 ∩ l2, replace L with ((L\l1)\l2) ∪ {l1 ∪ l2} 3 until there are no such l1 and l2.

3. If there is a set l in L such that A ∈ l, B ∈ l and C ∈ l then A, B and C are collinear.

Remark. Our tactic only captures basic properties of incidence, and is complete for only a small theory described below. Indeed, it can happen that some points A, B and C are collinear (if this fact follows from other geometric theorems) and our tactic fails in yielding a set l ∈ L such that A ∈ l, B ∈ l and C ∈ l.

Implementation

We now give some technical details about the implementation in Coq of our algorithm.

Data-structures

We need to represent sets of sets of points. To represent points we need a decidable ordered type, hence we use the type of positive numbers as key. To represent finite sets we use the module Msets of the standard library. We could have used the library Containers [START_REF] Lescuyer | First-class containers in coq[END_REF] which is easier to use than Msets because it in- 3 One should remember that we are manipulating sets of sets here. fers automatically the structures needed to build the finite sets but we have chosen to keep the standard Msets to make our development easier to install as it is included in the standard distribution. We selected the implementation using ordered lists. Notice that using AVLs is not interesting here since we rarely have more than thirty points.

The tactic

First, our tactic follows the first step of our previous algorithm in order to build the sets L and D by using an associative list so that the positives in our structures identify points. This initialization phase is implemented using the tactic language of Coq.

The second step is implemented as a Coq function defined using the Function package of Coq [START_REF] Barthe | Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant[END_REF]. To convince Coq that the algorithm terminates we proved the fact that the cardinality of L decreases at each recursive call.

The third step is also implemented as a Coq function which searches for a triple of points in a same set contained in L.

Proof of the soundness of our tactic

For the sake of modularity, we created a type class with the minimal set of properties that a theory needs to verify and we did all the proofs within the context of this type class. The type class mechanism allows us to state axiom systems and to use implicitly the proof that some theory is a model of this axiom system. Type classes are dependent records with some automation: Coq infers some implicit instances [START_REF] Sozeau | First-Class Type Classes[END_REF]. Our tactic is then applicable to any theory verifying these following four properties (our own development about Tarski's geometry but also, for example, the developments of Frédérique Guilhot [START_REF] Guilhot | Formalisation en coq et visualisation d'un cours de géométrie pour le lycée[END_REF], or Jean Duprat [START_REF] Duprat | Fondements de géométrie euclidienne[END_REF]

: forall X Y A B C : CTpoint, X<>Y -> CTCol X Y A -> CTCol X Y B -> CTCol X Y C -> CTCol A B C }.
We want to prove that the tactic produces a L that verifies the property "any triple of points belonging to a set of L are provably collinear". To do so we prove that the L produced by the first step of our algorithm verifies this property and that the second step of the algorithm preserves this property. The original L trivially verifies this property by construction. We denote by x the point represented by the positive integer x. Now assuming that we have l1, l2, p1 and p2 verifying p1 ∈ l1 ∩ l2, p2 ∈ l1 ∩ l2 and (p1, p2) ∈ D. Assuming that the interpretation of any triple of points in l1 are provably collinear and assuming the same for l2 then for any p3 in l1, Col p1 p2 p3 holds and for any p4 in l2, Col p1 p2 p4 holds. By the lemma stated previously (CTcol3) the interpretation of any triple of points in l1 ∪l2 are provably collinear. This proves that the second step of our algorithm preserves the property stated above and at the end of the second step we will obtain a set L verifying this property.

In Coq, the function x → x is called interp. The functions to manipulate sets of sets of positives are prefixed by SS, the functions

∀X1X2 . . . Xn+2, wd X1 X2 X3 . . . Xn+2 ⇒ wd X2 X1 X3 . . . Xn+2 (2) ∀X1X2 . . . Xn+3, coinc X1 X2 . . . Xn+3 ⇒ coinc X2 . . . Xn+3 X1 (3) ∀X1X2 . . . Xn+3, coinc X1 X2 X3 . . . Xn+3 ⇒ coinc X2 X1 X3 . . . Xn+3. (4)
Moreover, we admit that the coinc predicates trivially holds when two points are equal:

∀AX1X2 . . . Xn+1, coinc A A X1 . . . Xn+1. (5)
Finally we need that the pseudo-transitivity property holds:

∀X1X2 . . . Xn+2P1P2 . . . Pn+3, wd X1 . . . Xn+2 ∧ n+3 i=1 coinc X1 . . . Xn+2 Pi ⇒ coinc P1 . . . Pn+3. (6)
In Coq's syntax, we can express this axiom system, the dots are replaced by dependent types:

We define a class Arity which contains two fields:

• the type of the points we will consider,

• the natural number n such that n + 2 is the arity of the wd (then n + 3 will be the arity of coinc):

Class Arity := { COINCpoint : Type; n : nat }.

Coinc_predicates inherits from Arity and contains one field for each predicate: One can then define the type class corresponding to axioms ( The type T n is denoted by cartesianPower T n. The functions app 1 n P X Xn, allow the application of a predicate P of arity n + 1 to be applied to an X of some type T and an Xn of type T n . The functions app n 1 and app 2 n are similar. We denote the n-ary conjunction by pred conj.

The rest of the implementation is similar to the one presented in the previous section. The set of pairs of distinct points is generalized by a set of tuples ordered using lexicographic order. The proofs are more technical because we replace proof in a particular case by inductive proofs for an arbitrary arity. We have shown that the two generators of the group of permutations induce all permutation properties. Some lemmas are needed to deal with the dependent types, we omit the details.

Deriving instances in Tarski's geometry

In the context of Tarski's geometry, we derived three instances of the Coinc theory.

Collinearity

It is straightforward to instantiate our theory to obtain a tactic for collinearity as in Sec. 3. The proofs can be performed within Tarski's neutral dimensionless geometry (without assuming any upper-dimension axiom nor parallel postulate).

Coplanarity

The definition of coplanarity we adopt corresponds to the lemma 9.33 in [START_REF] Schwabhauser | Metamathematische Methoden in der Geometrie[END_REF]. It states that four points are coplanar if (at least) two out of these four points form a line which intersect the line formed by the remaining two points (see Fig. 2):

Definition Coplanar A B C D := exists X, (Col A B X /\ Col C D X) \/ (Col A C X /\ Col B D X) \/ (Col A D X /\ Col B C X).
The permutation properties (3-4) and trivial cases (5) of the predicate Coplanar are easy to obtain but the pseudo-transitivity (6) requires the axiom of Pasch (both the inner and outer forms) and many case distinctions. The inner form of Pasch's axiom that we assume is a variant of the axiom Moritz Pasch introduced in [START_REF] Pasch | Vorlesungen ber neuere Geometrie[END_REF] to repair the defects of Euclid. It intuitively says that if a line meets one side of a triangle and does not pass through the endpoints of that side, then it must meet one of the other sides of the triangle.

Concyclic

Our last instance allows to prove that points belong to the same circle. To define the concyclic predicate the first idea is to ask for the points to be coplanar and that there is a point (the center of the circle) which is at the same distance of the four points :

Definition Concyclic A B C D := Coplanar A B C D /\ exists O, Cong O A O B /\ Cong O A O C /\ Cong O A O D.
But in order to prove axiom (5), we need a more general definition because three points do not belong to a circle in case they are collinear. We will say that four points are concyclic-gen if either they are concyclic or if they all belong to the same line. Note that we do not assume the points to be distinct, so we need four collinearity assumptions to express this fact: This generalized predicate allows us to instantiate the type class.

Other instances

It would be of interest to study the generalization of these instances to other cases such as conics, cubics or linear subspaces. It is well-known that five points in general linear position define a plane conic. Pascal's hexagon theorem (see Fig. 3) is a good mean to define conics geometrically. Assuming Pappus' theorem we have proved in [START_REF] Magaud | A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem[END_REF] that the permutation properties of the predicate expressing that six points are coincident to a conic. It remains to show the pseudo-transitivity property.

Conclusions and Future Work

In this paper we described a generic reflexive tactic for solving some specific incidence properties which appear in high-school geometry. During this formalization we appreciated the versatility of the Calculus of Inductive Constructions (CIC) which allows to express easily functions of parameterizable arity.

Our tactic is generic in some sense, but also very specialized: it can solve a small class of goals. Yet, it would have been tedious to manually prove the goals which are solved automatically. Moreover, these sub-proofs are often hidden in an informal text since they are "obvious" and make the whole proof more difficult to read.

We believe that in order to obtain simple proofs, not only general progress about proof languages and automated deduction should be made but also some ad hoc techniques specialized in the domain of study should be used. For instance, in analysis, tactics to deal with proof involving epsilons could be used.

The tactic we obtain for dealing with co-planarity open also the path toward an extension of our formalization of geometry to higher dimension geometry.

Figure 1 .

 1 Figure 1. The midpoints theorem.

) 4 :

 4 Class Col_theory (CTpoint:Type) (CTCol:CTpoint->CTpoint->CTpoint->Prop):= { CTcol_trivial : forall A B : CTpoint, CTCol A A B; CTcol_perm_1 : forall A B C : CTpoint, CTCol A B C -> CTCol B C A; CTcol_perm_2 : forall A B C : CTpoint, CTCol A B C -> CTCol A C B; CTcol3

  Class Coinc_predicates (Ar : Arity) := { wd : arity COINCpoint (S (S n)); coinc : arity COINCpoint (S (S (S n))) }. The predicates are elements of the type arity T n representing predicates of type T → ... → T n times → Prop. Its formal definition is the following: Fixpoint arity (T:Type) (n:nat) := match n with | 0 => Prop | S p => T -> arity T p end.

Figure 2 .

 2 Figure 2. Definition of Coplanar.

Figure 3 .

 3 Figure 3. Pascal's hexagon theorem.

Definition

  Concyclic_gen A B C D := Concyclic A B C D \/ (Col A B C /\ Col A B D /\ Col A C D /\ Col B C D).

The common way of defining parallelism is to consider two lines as parallel if they belong to the same plane but do not meet. We distinguish between strict parallelism which corresponds to the previous definition and parallelism which add the possibility for the lines to be equal.

We use the expression 'proof of negation' to describe a proof of ¬A assuming A and obtaining a contradiction. 2 2015/10/15

In order to capture that ∀ABCσ, σ ∈ S {A,B,C} ⇒ Col A B C ⇒ Col σ(A) σ(B) σ(C) it suffices that this proposition holds for the generators of S {A,B,C} , namely (A B) and (A B C).3 2015/10/15

Exactly as for Col theory, to capture the permutation properties of wd and coinc, it suffices that the permutation properties hold for the generators of S {X 1 ,X 2 ,...,X n+2 } and S {X 1 ,X 2 ,...,X n+3 } , respectively. 4 2015/10/15

Availability

The full Coq development can be found at the following url: http: //geocoq.github.io/GeoCoq/

for sets of positives are prefixed by S and the functions for sets of pairs of positives are prefixed by ST.

We define a predicate expressing that our set of lines is correct; for every line, all points on this line are collinear:

Definition ss_ok (ss : SS.t) (interp: positive -> COLTpoint) := forall s, SS.mem s ss = true -> forall p1 p2 p3, S.mem p1 s && S.mem p2 s && S.mem p3 s = true -> CTCol (interp p1) (interp p2) (interp p3).

We also need a predicate expressing that our set of pairs of distinct points is correct; all pairs are distinct: Finally, we prove that our main function test col (which tests if 3 points belong to the same set s ∈ L after applying our algorithm on L and D) is correct assuming that we start in a correct context:

Lemma test_col_ok : forall ss sp interp p1 p2 p3, ss_ok ss interp -> sp_ok sp interp -> test_col ss sp p1 p2 p3 = true -> CTCol (interp p1) (interp p2) (interp p3).

For the reification phase, we repeat the application of the following lemma, which states that if we know that two points A and B are distinct we can add them to the list of pairs of distinct points: We have a similar lemma to reify collinearity assumptions:

Relation with equality of lines and rank functions

If we allow ourself the concept of line (either by defining it with Tarski's language as we have done in [START_REF] Braun | From Tarski to Hilbert[END_REF] or by using another language for geometry which includes lines such as Hilbert's axioms), then we can rewrite the pseudo-transitivity property of Col as an equality properties about lines:

At first sight this property looks nicer than our properties about Col, but the problem with this formulation is that lines are always defined by pairs of distinct points. In practice using this kind of formulation would imply numerous case distinctions about equality of points.

There is a close link between the concept of rank that we formalized previously [START_REF] Magaud | Formalizing Desargues' theorem in Coq using ranks in Coq[END_REF] and the properties studied in this section. The rank r of a subset S of elements of the matroid of points is the maximum size of an independent subset of S. Notice that the sub-modularity property of the rank function is a generalization of the pseudo-transitivity of Col:

Indeed, if l and m are lines then their rank are of 2, and if their intersection contains two distinct points then the rank of the intersection is at least of 2, hence all points in the union are collinear:

Generalization

The algorithm presented in the previous section may seem to be very specific. In fact, it can be generalized to deal with other properties than pseudo-transitivity of collinearity. For example, the lemma to express the pseudo-transitivity of the coplanar predicate has the same form:

And the lemma to express the pseudo-transitivity of the concyclic predicate has the same form:

In fact, our tactic is generalizable to any incidence relationship with algebraic curves or affine varieties.

The tactic

We use an axiomatic approach to define the generalized tactic.

The generalization holds for any predicate wd of arity n + 2 and coinc of arity n+3 for some n which verify the following axioms. Intuitively, wd predicate express the non degeneracy condition, and coinc the incidence relation.

We assume that the wd and coinc predicates are invariant by permutation 5 : ∀X1X2 . . . Xn+2, wd X1 X2 . . . Xn+2 ⇒ wd X2 . . . Xn+2 X1 (1)


Henri Gouin
email: henri.gouin@univ-amu.fr

Tommaso Ruggeri
email: tommaso.ruggeri@unibo.it

Dynamical pressure for fluid mixtures with several temperatures

Keywords: Fluid mixtures, Multi-temperatures, Dynamical pressure, Hamilton's principle Mélanges de fluides, multi-temperatures, pression dynamique, principe d'Hamilton. 1 Introduction

Dynamical pressure for fluid mixtures with several temperatures

The theory of mixtures generally considers two different kinds of continua : homogeneous mixtures (each component occupies the whole mixture volume) and heterogeneous ones (each component occupies only a part of the mixture volume). At least four approaches to the construction of two-fluids models are known. The first one for studying the heterogeneous two-phase flows is an averaging method [START_REF] Ishii | Thermo-fluid dynamic theory of two-phase flows[END_REF]. A second approach was used for the construction of a quantum liquid model and was purposed for the homogeneous mixtures of fluids [START_REF] Putterman | Super fluid hydrodynamics[END_REF]. A third approach is done in the context of rational thermodynamics founded on the postulate that each constituent obeys the same balance laws as a single fluid [START_REF] Müller | Rational Extended Thermodynamics[END_REF][START_REF] Ruggeri | On the hyperbolic system of a mixture of Eulerian fluids : a comparison between single and multi-temperature models[END_REF]. At least, there exists a different approach based on the Hamilton principle which is used for the construction of conservative mathematical models of continua. The variations of the Hamilton action are constructed in terms of virtual motions of continua which may be defined both in Lagrangian and Eulerian coordinates [START_REF] Serrin | Mathematical principles of classical fluid mechanics in Encyclopedia of Physics VIII/1[END_REF]. Here, we use variations in the case of fluid mixtures. The variational approach to the construction of two-fluid models has been used by many authors [START_REF] Berdichevsky | Variational principles of continuum mechanics[END_REF][START_REF] Gouin | Variational theory of mixtures in continuum mechanics[END_REF][START_REF] Gouin | Mixture of fluids involving entropy gradients and acceleration waves in interfacial layers[END_REF]. The method is different from the method proposed is [START_REF] Gouin | Identification of an average temperature and a dynamical pressure in multi-temperature mixture of fluids[END_REF] and is now developed in [START_REF] Gouin | The Hamilton principle for fluid binary mixtures with two temperatures[END_REF].

To study thermodynamical processes by using the Hamilton principle, the entropies of components are added to the field parameters instead of temperatures. The Lagrangian is the difference between the kinetic energy and an internal potential per unit volume depending on the densities, the entropies and the relative velocities of the mixture components. It is not necessary to distinguish molecular mixtures from heterogeneous fluids when each component occupies only a part of the mixture volume [START_REF] Gavrilyuk | Hyperbolic models of homogeneous two-fluid mixtures[END_REF]. The terms including interaction between different components come from the direct knowledge of the internal potential.

The assumption of a common temperature for all the components is open to doubt for the suspensions of particles [START_REF] Lhuillier | From Molecular mixtures to suspensions of particles[END_REF] as well as in the mixtures of gases in the early universe [START_REF] De Groot | Relativistic kinetic theory[END_REF]. By using the Hamilton principle, the existence of several temperatures (one temperature for each component) must be associated with the existence of several entropies (one specific entropy for each component). The internal potential per unit volume is a function of the densities, the entropies and the difference of velocity between components.

2 Governing equations in conservative cases.

In a Galilean system of coordinates, the motion of a two-fluid mixture is represented as

Z α = Φ α (z) , (α = 1, 2)
where z = (t, x) denotes Eulerian coordinates in a four-dimensional domain ω in the time-space and Z α = (λ, X α ) denotes Lagrangian coordinates of the component α in a four-dimensional reference space ω α . The conservation of matter for each component requires

ρ α det F a = ρ α0 (X α ) with F a = ∂x ∂X α , (1)
where index α0 corresponds to the reference density in ω α and det (∂x/∂X α ) is the Jacobian determinant of the motion of the component α of density ρ α . In differentiable cases Eqs (1) are equivalent to the equations of density balances

∂ρ α ∂t + div(ρ α v α ) = 0, (2)
where v α denotes the velocity of each component α. The Lagrangian of the binary system is

L = 2 α=1 1 2 ρ α v 2 α -ρ α Ω α -η(ρ 1 , ρ 2 , s 1 , s 2 , u),
where the summation is taken over the fluid components (α = 1, 2), s α are the specific entropies, u = v 2 -v 1 is the relative velocity of components, Ω α are the external force potentials, η is a potential per unit volume of the mixture. The Lagrangian L is a function of ρ α , v α , s α and we introduce the quantities

R α ≡ ∂L ∂ρ α = 1 2 v 2 α - ∂η ∂ρ α -Ω α , k T α ≡ 1 ρ α ∂L ∂v α = v T α - (-1) α ρ α ∂η ∂u , ρ α T α ≡ - ∂L ∂s α = ∂η ∂s α , (3)
where T denotes the transposition and ∂L/∂v α , ∂η/∂u are linear forms. Relation (3) 3 defines the temperatures T α (α = 1, 2) which are dynamical quantities depending on ρ 1 , ρ 2 , s 1 , s 2 and u.

To obtain the equations of component motions by means of the Hamilton principle, we consider variations of particle motions in the form of surjective mappings X α = Ξ α (t, x;κ α ), where scalars κ α are defined in a neighborhood of zero ; they are associated with a two-parameter family of virtual motions. The real motions correspond to κ α = 0 such that Ξ α (t, x;0) = φ α (t, x) and virtual Lagrange displacements are

δ α X α = ∂Ξ α (t, x;κ α ) ∂κ α | κα=0 , (α = 1, 2). (4)
The Hamilton action is a = ω L dv dt. We first consider the Hamilton principle in the form

δ α a ≡ da dκ α |κ α=0 = δ α ω L dv dt = 0,
under constraints [START_REF] Ishii | Thermo-fluid dynamic theory of two-phase flows[END_REF], where δ α a are the variations of a associated with Rel. [START_REF] Ruggeri | On the hyperbolic system of a mixture of Eulerian fluids : a comparison between single and multi-temperature models[END_REF].

From the definition of virtual motions, we obtain the values of δ α v α (x, t), δ α ρ α (x, t) and δ α s α (x, t) where the notation δ α b(t, x) represents the variation of function b at (t, x) fixed. The functions are assumed to be smooth enough in the domain ω α and δ α X α = 0 on its boundary. It follows [START_REF] Gouin | The Hamilton principle for fluid binary mixtures with two temperatures[END_REF],

δ α a = ωα ρ α0 - ∂R α ∂X α + ∂ ∂λ (k T α F α ) -T α ∂s α0 ∂X α δ α X α dv α dt,
and we get the component motion equations in Lagrangian coordinates, ∂ ∂λ

(k T α F α ) - ∂R α ∂X α -T α ∂s α0 ∂X α = 0.
By taking into account the identity d α F α dt -∂v α ∂x F α = 0 and for λ = t, we rewrite the equations in Eulerian coordinates,

d α k T α dt + k T α ∂v α ∂x = ∂R α ∂x + T α ∂s α ∂x .

DOI: 10.1051/meca/2009052

To obtain the equation of energy, we need a second variation of motions associated with the time parameter.

The variation corresponds to a virtual motion in the form λ = ϕ(t; κ), where scalar κ is defined in a neighborhood of zero. The real motion of the mixture corresponds to κ = 0 such that ϕ(t, 0) = t ; the associated virtual displacement is

δλ = ∂ϕ(t; κ) ∂κ | κ=0 .
In multi-component fluids, due to exchanges of energy between the components, the entropies cannot be conserved along component paths ; in the reference spaces ω α , the specific entropies s α depend also on λ

s α = s α0 (λ, X α ) .
The variation of Hamilton's action associated with the second family of virtual motions yields

δa ≡ δ ω L dv dt = ω ∂L ∂λ δλ dv dt = 0. From ∂L ∂λ = 2 α=1 ∂L ∂s α ∂s α0 ∂λ , we deduce when λ = t, ∂L ∂λ = - 2 α=1 ρ α T α d α s α dt , where d α s α dt = ∂s α ∂t + ∂s α ∂x v α
is the material derivative with respect to velocity v α . We obtain for the total mixture

2 α=1 ρ α T α d α s α dt = 0. (5)
Due to Eqs. ( 2) we obtain the equivalent form

2 α=1 Q α = 0 with Q α = ∂ρ α s α ∂t + div(ρ α s α v α ) T α . (6)
Equation ( 6) expresses that the exchange of energy between components has a null total amount. In case of mixtures with two entropies, the Hamilton principle is not able to close the system of motion equations ; we need additional arguments to obtain the evolution equations for each entropy s α by considering the behaviors of Q α . A possibility to close the system of equations is to consider that the momenta and heat exchanges between the components are rapid enough to have a common temperature. Another possibility, used by Landau for quantum fluids [START_REF] Putterman | Super fluid hydrodynamics[END_REF], is to assume that the total specific entropy s is convected along the first component trajectory. These assumptions are not valid for heterogeneous mixtures where each phase has different pressures and temperatures [START_REF] Lhuillier | From Molecular mixtures to suspensions of particles[END_REF][START_REF] De Groot | Relativistic kinetic theory[END_REF].

3 Mixtures weakly out of equilibrium.

We consider the case when the mixture is weakly out of equilibrium such that the difference of velocities u and the difference of temperatures T 2 -T 1 are small enough with respect to the main field variables.

In the following,

ρ v = 2 α=1 ρ α k α = 2 α=1 ρ α v α is the total momentum and ρ = 2 α=1
ρ α is the mixture density.

For the sake of simplicity, we neglect the external forces. Generally, the volume potential η is developed in the

form 1 η(ρ 1 , ρ 2 , s 1 , s 2 , u) = e(ρ 1 , ρ 2 , s 1 , s 2 ) -b(ρ 1 , ρ 2 , s 1 , s 2 ) u 2 ,
where b is a positive function of ρ 1 , ρ 2 , s 1 , s 2 . We consider the linear approximation when |u| is small with respect to |v 1 | and |v 2 |. In linear approximation the volume potential is equal to the volume internal energy e [START_REF] Gavrilyuk | Hyperbolic models of homogeneous two-fluid mixtures[END_REF],

η(ρ 1 , ρ 2 , s 1 , s 2 , u) ≈ e(ρ 1 , ρ 2 , s 1 , s 2 ) = ρ ε(ρ 1 , ρ 2 , s 1 , s 2 ),
where ε denotes the internal energy per unit mass. Let us note that the diffusion vector

j = ρ 1 (v 1 -v) ≡ ρ 2 (v -v 2
) is a small momentum vector deduced both from velocities and densities of the components. The equations of density balances (1) can be written in the form

dρ dt + ρ div v = 0 and ρ dc dt + div j = 0, (7)
where c = ρ 1 /ρ denotes the concentration of component 1 and d/dt = ∂/∂t + ∂/∂x . v is the material derivative with respect to the average velocity of the mixture. The divergence of a linear operator A is the covector divA such that, for any constant vector a, (div A) a = div (A a) and we write v α v T α ≡ v α ⊗ v α . Let us denote by h α ≡ ∂e/∂ρ α the specific enthalpy of the component α. For processes with weak diffusion, the equations of component motions get the form,

ρ α Γ α ≡ ∂ρ α v α ∂t + div(ρ α v α ⊗ v α ) T = ρ α T α grad s α -ρ α grad h α .
The equation of total momentum is [START_REF] Gouin | The Hamilton principle for fluid binary mixtures with two temperatures[END_REF] :

∂ρv ∂t + div 2 α=1 (ρ α v α ⊗ v α ) -t T = 0,
where t = 2 α=1 t α is the total stress tensor such that t ανγ = -p α δ νγ , p α = ρρ α ε ,ρα = ρ α e ,ρα - ρ α e/ρ , p = 2 α=1 p α . The internal energy is a natural function of densities and entropies. Due to Def. (3) 3 ,

ρ 1 T 1 = ρ ∂ε ∂s 1 (ρ 1 , ρ 2 , s 1 , s 2 ) and ρ 2 T 2 = ρ ∂ε ∂s 2 (ρ 1 , ρ 2 , s 1 , s 2 ). (8)
Let us denote by ε the expression of the specific internal energy as a function of ρ, c, s 1 , s 2 such that ε(ρ, c, s 1 , s 2 ) = ε(ρ 1 , ρ 2 , s 1 , s 2 ) ; we get :

ρ dε dt = ρ ∂ε ∂ρ dρ dt + ρ ∂ε ∂c dc dt + ρ ∂ε ∂s 1 ds 1 dt + ρ ∂ε ∂s 2 ds 2 dt .
Due to the fact that ρ 2 ∂ε ∂ρ = p and ∂ε ∂c = h 1 -h 2 , we obtain

ρ dε dt = p ρ dρ dt + ρ (h 1 -h 2 ) dc dt + ρ 1 T 1 ds 1 dt + ρ 2 T 2 ds 2 dt . (9)
By taking into account that v) and by using Eqs. ( 5), [START_REF] Gouin | Variational theory of mixtures in continuum mechanics[END_REF], Eq. ( 9) yields

d α s α dt = ds α dt + ∂s α ∂x (v α -
ρ dε dt + p div v + (h 1 -h 2 ) div j + (T 1 grad s 1 -T 2 grad s 2 ) T j = 0. (10)
Due to Eqs. ( 8), the internal energy can be expressed as a function of densities and temperatures of components

ε(ρ 1 , ρ 2 , T 1 , T 2 ) = ε(ρ 1 , ρ 2 , s 1 , s 2 ).
As we wrote in [START_REF] Gouin | Identification of an average temperature and a dynamical pressure in multi-temperature mixture of fluids[END_REF], we define the average temperature T associated with T 1 and T 2 through the implicit solution of the equation

ε(ρ 1 , ρ 2 , T, T ) = ε(ρ 1 , ρ 2 , T 1 , T 2 ). (11)
We denote by Θ α = T α -T the difference between component and average temperatures, which are nonequilibrium thermodynamical variables. Near equilibrium, Eq. ( 11) can be expanded to the first order ; then

2 α=1 c α v Θ α = 0 with c α v = ∂ ε ∂T α (ρ 1 , ρ 2 , T, T ). (12)
Due to the fact that ρ dε =

2 α=1 ρ α T α ds α + p α ρ α dρ α , then ρ c 1 v = T 2 α=1 ρ α ∂s α ∂T 1 (ρ 1 , ρ 2 , T, T ) and ρ c 2 v = T 2 α=1 ρ α ∂s α ∂T 2 (ρ 1 , ρ 2 , T, T ). (13)
The definition of the total entropy s of the mixture is The exchange of energy between components must obey the second law of thermodynamics : the total entropy rate is an increasing function of time and we consider the second law of thermodynamics in the form

ρ s = 2 α=1 ρ α s α (ρ 1 , ρ 2 , T 1 , T 2 ). (14
2 α=1 ∂ρ α s α ∂t + div(ρ α s α v α ) ≥ 0 (18)
Due to Rels. (2) the Clausius-Duhem inequality (18) is equivalent to

2 α=1 ρ α d α s α dt ≥ 0 .
This implies that the second member of Rel. (17) must be positive. Therefore, as usual in thermodynamics of irreversible processes, the entropy inequality requires

π ≡ p -p o = -Λ div v . (19)
This expression defines the Lagrange multiplier Λ of proportionality such that Λ ≥ 0. The dynamical pressure π is the difference between the pressure in the process out of equilibrium with different temperatures for the components and the pressure of the mixture assumed in local thermodynamical equilibrium with the common average temperature T . Let us notice that Eqs. [START_REF] Berdichevsky | Variational principles of continuum mechanics[END_REF]19) allow to obtain Q α values. In fact,

ρ 1 T (T 2 -T 1 ) d 1 s 1 dt = Λ T 2 (div v) 2 and ρ 2 T (T 1 -T 2 ) d 2 s 2 dt = Λ T 1 (div v) 2
and the system of field equations is now closed.

Conclusion.

The Hamilton principle points out that a dynamical pressure can be obtained by neglecting viscosity, friction or external heat fluxes. This is a main property of mixtures with multi-temperatures and this fact may have some applications in plasma of gases and in the evolution of the early universe [START_REF] Weinberg | Entropy generation and the survival of protogalaxies in an expanding universe[END_REF].

The results are in complete accordance with the ones by Gouin & Ruggeri [START_REF] Gouin | Identification of an average temperature and a dynamical pressure in multi-temperature mixture of fluids[END_REF] and developed in [START_REF] Gouin | The Hamilton principle for fluid binary mixtures with two temperatures[END_REF]. This is an important verification of the fact that the Hamilton principle can be extended to nonconservative mixture motions when components have different temperature. A difference with classical thermodynamics methods is that the volume internal energy is not necessary the sum of the volume internal energies of the components. In [START_REF] Gouin | The Hamilton principle for fluid binary mixtures with two temperatures[END_REF], the volume internal energy is a nonseparate function of densities and entropies (or temperatures) and is consequently more general than in [START_REF] Gouin | Identification of an average temperature and a dynamical pressure in multi-temperature mixture of fluids[END_REF].

)

  DOI: 10.1051/meca/2009052

In Ref.[START_REF] Gouin | Identification of an average temperature and a dynamical pressure in multi-temperature mixture of fluids[END_REF], the internal energy is the sum of the internal energies of the components ρ ε = 2 α=1 ραεα(ρα, sα) .

DOI: 10.1051/meca/2009052

The first order expansion of Eq. ( 14) yields

Due to Rels. ( 12), [START_REF] De Groot | Relativistic kinetic theory[END_REF], ρ s = 2 α=1 ρ α s α (ρ 1 , ρ 2 , T, T ) and the specific entropy s does not depend on Θ 1 and Θ 2 but only on ρ 1 , ρ 2 and T . We denote by ε the internal specific energy as a function of ρ, c, T :

which satisfies the Gibbs equation

where p o (ρ, c, T ) is the equilibrium pressure at temperature T and µ 2 -µ 1 , difference of component chemical potentials, is the chemical potential of the whole mixture. By taking into account of equation ( 7), we get

Moreover,

Equation ( 15) yields the relation between the material derivatives of entropy s and entropies s 1 and s 2 . By taking into account this result in Eq. ( 10) and ε(ρ, c, T ) = ε(ρ 1 , ρ 2 , s 1 , s 2 ), we obtain

(16) The differences of temperatures Θ 1 ≡ T 1 -T and Θ 2 ≡ T 2 -T are small with respect to T and j is a small diffusion term with respect to the mixture momentum ρv ; consequently, in an approximation to the first order, the term

In an approximation to the first order, the term (Θ 1 s 1 + Θ 2 s 2 ) div j is negligible.

Due to the fact that µ α (ρ 1 , ρ 2 , T 1 , T 2 ) = h α -T α s α is the chemical potential of the component α, when j is a small diffusion velocity with respect to average velocity v, the term

is vanishing in an approximation to the first order. Consequently, in an approximation to the first order, Eq. ( 16) reduces to