Shu-Ming Sun
email: sun@math.vt.edu

Emmanuel Trélat
email: emmanuel.trelat@upmc.fr

Bing-Yu Zhang
email: zhangb@ucmail.uc.edu

Ning Zhong
email: zhongn@ucmail.uc.edu

A Note on Sharpness of the Local Kato-Smoothing Property for Dispersive Wave Equations

It is well known that solutions of the Cauchy problem for general dispersive equations wt + iP (D)w = 0, w(x, 0) = q(x), x ∈ R n , t ∈ R, enjoy the local smoothing property

where m is the order of the pseudo-differential operator P (D). This property, called local Kato smoothing, was first discovered by Kato for the KdV equation and implicitly shown later for linear Schrödinger equations. In this paper, we show that the local Kato smoothing property possessed by solutions general dispersive equations in the 1D case is sharp, meaning that there exist initial data q ∈ H s (R) such that the corresponding solution w does not belong to the space L 2 -T, T ; H s+ m-1 2 +ǫ loc (R) for any ǫ > 0.

Introduction

Consider the Cauchy problems for the one-dimensional Korteweg-de Vries (KdV) equation

u t + uu x + u xxx = 0, u(x, 0) = φ(x), x ∈ R, t ∈ R,
and for the one-dimensional linear Schrödinger equation

iv t + v xx = 0, v(x, 0) = ψ(x), x ∈ R, t ∈ R. (1.1)
While their solutions are known to be as smooth as their initial values in the sense that u(•, t) ∈ H s (R) if and only if φ ∈ H s (R) for any t ∈ R, This local smoothing property was first discovered by Kato [START_REF] Kato | On the Cauchy problem for the (generalized) Korteweg-de Vries equations, Advances in Mathematics Supplementary Studies[END_REF] for the KdV equation and implicitly shown later by Sjölin [START_REF] Sjölin | Regularity of solutions to the Schrödinger equation[END_REF] for the linear Schrödinger equation. It is now referred to as the local Kato-smoothing property and has been proved by Constantin and Saut [START_REF] Constantin | Local smoothing properties of dispersive equations[END_REF] to be a common feature of dispersive-wave systems. Indeed, Constantin and Saut studied the following general dispersive-wave equation

w t + iP (D)w = 0, w(x, 0) = q(x), x ∈ R n , t ∈ R, (1.2)
where D = 1 i (∂/∂x 1 , • • • , ∂/∂x n ), P (D)w is the pseudo-differential operator

P (D)w =
R n e ix•ξ p(ξ) ŵ(ξ)dξ defined with a real symbol p(ξ), and ŵ is the Fourier transformation of w with respect the spatial variable x. The symbol p(ξ) is assumed to satisfy (i) p ∈ L ∞ loc (R n , R) and is continuously differentiable for |ξ| > R with some R ≥ 0,

(ii) there exist m > 1, C 1 > 0, C 2 > 0 such that |p(ξ)| ≤ C 1 (1 + |ξ|) m for all ξ ∈ R n , and |∂p(ξ)/∂ξ j | ≥ C 2 (1 + |ξ|) m-1 |ξ j |/|ξ|,
for all ξ ∈ R n and |ξ| > R, j = 0, 1, 2, . . . , n.

Theorem A (Constantin and Saut [START_REF] Constantin | Local smoothing properties of dispersive equations[END_REF]) Let s ≥ -m-1 2 be given. Then for any q ∈ H s (R n ), the corresponding solution w of (1.2) belongs to the space C(R; H

s+ m-1 2 loc (R n ))
and moreover, for any given T > 0 and R > 0, there exists a constant C depending only on s, T and R such that

T -T |x|≤R (I -∆) (m-1+2s)/4 w(x, t) 2 dxdt ≤ C q 2 H s (R n ) . (1.3)
This local smoothing effect, as pointed out by Constantin and Saut in [START_REF] Constantin | Local smoothing properties of dispersive equations[END_REF], is due to the dispersive nature of the linear part of the equation and the gain of the regularity, (m -1)/2, depends only on the order m of the equation and has nothing to do, in particular, with the dimension of the spatial domain R n . The discovery of the local Kato-smoothing property has stimulated enthusiasm in seeking various smoothing properties of dispersive-wave equations which, in turn, has greatly enhanced the study of mathematical theory of nonlinear dispersive-wave equations, in particular, the well-posedness of their Cauchy problems in low regularity spaces (see [START_REF] Bourgain | Fourier transform restriction phenomena for certain lattice subsets and applications to nonlinear evolution equations, part I: Shrödinger equations[END_REF][START_REF] Bourgain | Fourier transform restriction phenomena for certain lattice subsets and applications to nonlinear evolution equations, part II: the KdV-equation[END_REF][START_REF] Christ | Asymptotics, frequency modulation, and low regularity ill-posedness for canonical defocusing equations[END_REF][START_REF] Kenig | On the (generalized) Korteweg-de Vries equation[END_REF][START_REF] Kenig | Oscillatory integrals and regularity of dispersive equations[END_REF][START_REF] Kenig | Well-posedness of the initial value problem for the Korteweg-de VrieseEquation[END_REF][START_REF] Kenig | Well-Posedness and scattering results for the generalized Korteweg-de Vries equations via the contraction principle[END_REF][START_REF] Kenig | A bilinear estimate with applications to the KdV equation[END_REF] and see the references therein).

A question arises naturally: Does the solution w of (1.2) gain more regularity than m-1 2 by comparing it to its initial value q? More precisely, one may wonder if the estimate (1.3) is sharp in the following sense:

Is it possible to find ǫ > 0 such that, for any given T > 0 and R > 0, there exists a constant C depending only on s, T and R such that

T -T |x|≤R (I -∆) (m-1+2s+ǫ)/4 w(x, t) 2 dxdt ≤ C q 2 H s (R n ) ? (1.4)
In particular, applying Theorem A to the linear KdV equation (Airy equation)

u t + u xxx = 0, u(x, 0) = φ(x), x ∈ R, t ∈ R, (1.5)
and to the linear Schrödinger equation (1.1) leads to the following estimates for their solutions:

given s ∈ R and R, T > 0, there exists a constant C > 0 such that for any φ, ψ ∈ H s (R), the corresponding solutions u of (1.5) and v of (1.1) satisfy

T -T |x|≤R Λ s+1 u(x, t) 2 dxdt ≤ C φ 2 H s (R) , (1.6)
and

T -T |x|≤R Λ s+1/2 v(x, t) 2 dxdt ≤ C ψ 2 H s (R) , (1.7)
respectively, where Λ = (I -

∂ 2 x ) 1 2
.

Is it possible to find an ǫ > 0 such that

u ∈ L 2 (-T, T ; H s+1+ǫ loc (R)), v ∈ L 2 (-T, T ; H s+/12+ǫ loc (R))
and moreover, for any given T > 0 and R > 0,

T -T |x|≤R Λ s+1+ǫ u(x, t) 2 dxdt ≤ C φ 2 H s (R) , (1.8)
and

T -T |x|≤R Λ s+1/2+ǫ v(x, t) 2 dxdt ≤ C ψ 2 H s (R) ? (1.9)
Here the constant C is assumed to depend only on s, R, and T .

As far as we know, this question has not been addressed in the literature. On the other hand, it has been proved by Kenig, Ponce and Vega [START_REF] Kenig | Oscillatory integrals and regularity of dispersive equations[END_REF][START_REF] Kenig | Well-posedness of the initial value problem for the Korteweg-de VrieseEquation[END_REF] that solutions of (1.5) and (1.1) possess the following smoothing property.

Theorem B (Kenig, Ponce and Vega [START_REF] Kenig | Oscillatory integrals and regularity of dispersive equations[END_REF][START_REF] Kenig | Well-posedness of the initial value problem for the Korteweg-de VrieseEquation[END_REF]) For any s ∈ R, there exists a constant C s > 0 depending only on s such that for any φ, ψ ∈ H s (R), the corresponding solutions u of (1.5) and the solution v of (1.1) satisfy

sup x∈R ∂ s+1 x u(x, •) L 2 t (R) ≤ C s φ H s (R) , (1.10)
and

sup x∈R ∂ s+1/2 x v(x, •) L 2 t (R) ≤ C s ψ H s (R) . (1.11)
This property is referred to as sharp Kato-smoothing. It has become an important tool in studying the non-homogeneous boundary value problems [START_REF] Bona | A nonhomogeneous boundary-value problem for the Korteweg-de Vries equation in a quarter plane[END_REF][START_REF] Bona | A nonhomogeneous boundary-value problem for the Korteweg-de Vries Equation on a finite domain[END_REF][START_REF] Holmer | The initial-boundary value problem for the Korteweg-de Vries equation[END_REF][START_REF] Holmer | The initial-boundary-value problem for the 1D nonlinear Schrödinger equation on the half-line[END_REF] and control theory of the KdV equation and the Schrödinger equation (see [START_REF] Cerpa | Boundary controllability of the Korteweg-de Vries equation on a bounded domain[END_REF][START_REF] Jia | Boundary stabilization of the Korteweg-de Vries equation and the Kortweg-de Vries-Burgers equation[END_REF][START_REF] Rosier | Control and stabilization of the Korteweg-de Vries equation: recent progresses[END_REF][START_REF] Russell | Smoothing and decay properties of solutions of the Kortewegde Vries equation on a periodic domain with point dissipation[END_REF] and see the references therein).

Since the estimates (1.6) and (1.7) follow easily from (1.10) and (1.11), it remains a doubt if estimates (1.6) and (1.7) are sharp: Does there exist ǫ > 0 such that (1.8) and (1.9) hold for all solutions of (1.5) and (1.1), respectively?

In this paper, we will first consider the Cauchy problem for general one-dimensional evolutionary partial differential equations

u t = Q(∂ x )u, u(x, 0) = φ(x), x ∈ R, t > 0 (1.12)
where

Q(D) = Q 1 (∂ x ) + Q 2 (∂ x )
is a (2N + 1)-order differential operator, with

Q 1 (∂ x ) = N j=0 a j ∂ 2j+1 x , and Q 2 (∂ x ) = N k=1 b k ∂ 2k x ,
where a j , j = 0, 1, • • • , N are real constants and

b k = α k + iβ k , k = 1, 2, • • • , N,
are complex constants. Assume that there exists an integer 0 ≤ ν ≤ N such that either

(-1) N a N > 0, α k = 0, k = ν + 1, • • • , N, (-1) ν α ν < 0, (1.13)
or

a N = 0, (-1) N α N < 0. (1.14)
Note that, if (-1) N a N < 0, then we can make a change of variable x → -x to change the equation so that (-1) N a N > 0. Then it can be verified that the solution u of (1.12) possesses the local Kato-smoothing property:

Given s ∈ R and R, T > 0, there exists C > 0 such that for any φ ∈ H s (R), the corresponding solution u of (1.12) satisfies

T 0 |x|≤R Λ s+N u(x, t) 2 dxdt ≤ C φ 2 H s (R) . (1.15)
We show that the local Kato smoothing property for (1.12) given by the estimate (1.15) is sharp.

Theorem 1.1. For any ǫ > 0, the estimate

T 0 |x|≤R Λ s+N +ǫ u(x, t) 2 dxdt ≤ C φ 2 H s (R) (1.16)
fails to be true for all solutions of the Cauchy problem (1.12).

This result applies not only to the Airy equation, but also to the linear KdV-Burgers equation

u t + u x + u xxx -u xx = 0.
which is not cannot be written in the form of the dispersive equation (1.2). Moreover, the parabolic equation

u t = (-1) m+1 ∂ 2m x u, u(x, 0) = φ(x), x ∈ R, t ≥ 0,
and the (linear) Ginzburg-Landau type equation

u t = (α + iβ)(-1) m+1 ∂ 2m x u, u(x, 0) = φ(x), x ∈ R, t ≥ 0,
with α > 0 are special cases of (1.12). Their solutions possess the following global dissipative smoothing property:

φ ∈ H s (R) =⇒ u ∈ C([0, T ]; H s (R)) ∩ L 2 (0, T ; H s+m (R))
and there exists a constant C depending only on T and s such that

u L 2 (0,T ;H s+m (R)) ≤ C φ H s (R) .
(1.17)

Similarly, one may wonder if this type of dissipative smoothing property is sharp: does the solution u belong to L 2 (0, T ; H s+m+ǫ loc (R)) for some ǫ > 0 in general when φ ∈ H s (R), in general? Theorem 1.1 provides a negative answer to this question and shows that the dissipative smoothing property (1.17) is sharp.

We next consider the Cauchy problem (1.2) in the 1D case

w t + iP (D)w = 0, w(x, 0) = q(x), x ∈ R, t ∈ R, (1.18)
and we show that the estimate (1.3) is sharp.

Theorem 1.2. The local Kato-smoothing property of the Cauchy problem (1.2) posed in R as described by (1.3) is sharp in the sense that, for any ǫ > 0, the estimate

T 0 |x|≤R Λ s+(m-1)/2+ǫ w(x, t) 2 dxdt ≤ C q 2 H s (R) (1.19)
fails to be true for all solutions of (1.2).

To prove Theorems 1.1 and 1.2, given s and ǫ > 0, we will construct bounded sequences {φ n } and {ψ n } in H s (R) such that the corresponding solutions u n of (1.5), and v n of (1.1), satisfy respectively

lim n→+∞ T -T |x|≤R Λ s+1+ǫ u n (x, t) 2 dxdt = +∞, lim n→+∞ T -T |x|≤R Λ s+1/2+ǫ v n (x, t) 2 dxdt = +∞,
for some T > 0 and R > 0.

2 Proof of Theorem 1.1

By contradiction, assume that the estimate (1.16) holds true for some ǫ > 0. Without loss of generality, we assume that s = 0 and 0 < ǫ < 1 2 . Let p be a given C ∞ smooth function with compact support, such that 0 ≤ p(x) ≤ 1 for any x ∈ R, and Applying Λ ǫ to the equation in (1.5) yields

(Λ ǫ u) t + Q(∂ x )[(Λ ǫ u)] = 0, (Λ ǫ u)(x, 0) = (Λ ǫ φ)(x), x ∈ R, t ∈ R. (2.1)
Multiplying the equation in (2.1) by p(x)Λ ǫ u and integrating the resulting equation over R with respect to x gives

∞ -∞ p(x) (Λ ǫ u) 2 2 dx t = N j=0 (-1) j+1 a j j + 1 2 ∞ -∞ p ′ (x)(∂ j x (Λ ǫ u) 2 dx + N j=0 j+1 l=2 l j + 1 ∞ -∞ p (l) (x)∂ j+1-l x (Λ ǫ u)∂ j x (Λ ǫ u)dx + N k=1 (-1) k b k ∞ -∞ ∂ k x (p(x)Λ ǫ u)∂ k x (Λ ǫ u)dx
Integrating both sides of the above equation with respect to t over (0, T ) leads to

∞ -∞ p(x)(Λ ǫ φ) 2 dx- ∞ -∞ p(x) (Λ ǫ u(x, T )) 2 dx = N j=0 (-1) j+1 a j j + 1 2 T 0 ∞ -∞ p ′ (x)(∂ j x (Λ ǫ u) 2 dxdt + N j=0 j+1 l=2 l j + 1 T 0 ∞ -∞ p (l) (x)∂ j+1-l x (Λ ǫ u)∂ j x (Λ ǫ u)dxdt + N k=1 (-1) k b k T 0 ∞ -∞ ∂ k x (p(x)Λ ǫ u)∂ k x (Λ ǫ u)dxdt (2.2)
Since p has a compact support, and since (1.16) holds true, it follows that the right-hand side of (2.2) estimated by C T φ 2 L 2 (R) , and thus

∞ -∞ p(x)(Λ ǫ φ) 2 dx- ∞ -∞ p(x) (Λ ǫ u(x, T )) 2 dx ≤ C T φ 2 L 2 (R) (2.3)
Let us prove that (2.3) cannot hold true, by constructing a sequence

{φ n } ∞ n=1 in L 2 (R) such that sup 0<n<+∞ φ n L 2 (R) < +∞, (2.4) lim n→+∞ ∞ -∞ p(x)(Λ ǫ φ n (x)) 2 dx = +∞, (2.5) and sup 0<n<+∞ ∞ -∞ p(x) (Λ ǫ u n (x, T )) 2 dx < +∞, (2.6)
where u n is the corresponding solution of (1.12) with u n (x, 0) = φ n (x).

Let η be the function whose Fourier transform is

η(ξ) = 1 (1 + ξ 2 ) 1/4 (1 + ln(1 + ξ 2 )) 2 .
The function η belongs to the space L 2 (R) and has the following properties:

(i) Λ ǫ η ∈ L 2 (c, d) for any (c, d) with 0 ∈ (c, d),
(ii) Λ ǫ η is well-defined for any x = 0, (iii) both η(x) and (Λ ǫ η)(x) decay faster than any algebraic order when |x| → +∞.

Let χ n (ξ) be an even C ∞ cut-off function satisfying χ n (ξ) = 1 for ξ ∈ [0, n] and χ n (ξ) = 0 for ξ ∈ [n + 1, +∞). Note that χ n (ξ) is a monotone decreasing function and keeps the same shape

for ξ ∈ [n, n + 1] as n changes. For any n ≥ 1, let φ n ∈ L 2 (R) be the function whose Fourier transform is φn (ξ) = e i50ξ χ n (ξ) (1 + ξ 2 ) 1/4 (1 + ln(1 + ξ 2 )) 2 = e i50ξ χ n (ξ)η(ξ).
Then we have

φ n L 2 (R) = φn L 2 (R) ≤ C η L 2 (R) < +∞ for any n ≥ 1. Since Λ ǫ η(x + 50) ∈ L 2 (c, d) for any (c, d) with -50 ∈ (c, d) and max |x+50|≥10 (|φ n (x)| + |Λ ǫ φ n (x)|) ≤ C(1 + |x|) -2 for n = 1, 2, • • • where C is independent of n, we have that for any n ≥ 1, ∞ -∞ (1 -p(x))(Λ ǫ φ n ) 2 dx ≤ C 0 < +∞, and, henceforth, as n → +∞, ∞ -∞ p(x)(Λ ǫ φ n ) 2 dx = ∞ -∞ (Λ ǫ φ n ) 2 dx - ∞ -∞ (1 -p(x))(Λ ǫ φ n ) 2 dx = ∞ -∞ (1 + ξ 2 ) ǫ/2 χ n (ξ)η(ξ) 2 dξ - ∞ -∞ (1 -p(x))(Λ ǫ φ n ) 2 dx → +∞ It remains to prove (2.6). To this end, note that if α k = 0, k = ν + 1, • • • , N, (-1) ν α ν < 0 for some 1 ≤ ν ≤ N , then for any x ∈ R, |Λ ǫ u n (x, T )| ≤ 1 2π ∞ -∞ e Q(iξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ) dξ ≤ 1 2π ∞ -∞ e Q2(iξ)T (1 + ξ 2 ) ǫ/2 φn (ξ) dξ ≤ 1 2π ∞ -∞ e 2Q2(iξ)T (1 + ξ 2 ) ǫ dξ 1 2 φ n L 2 (R) Then ∞ -∞ p(x) (Λ ǫ u n (x, T )) 2 dx ≤ 1 2π -1 -110 p(x) ∞ -∞ e 2Q2(iξ)T (1 + ξ 2 ) ǫ dξ φ n 2 L 2 (R) dx ≤ 1 2π ∞ -∞ e 2Q2(iξ)T (1 + ξ 2 ) ǫ dξ φ n 2 L 2 (R) -1 -110 p(x)dx < C < +∞
for any n. On the other hand, If

α k = 0, k = 1, 2, • • • , N , then Q(iξ) = i Q(ξ)
where Q(ξ) is a real valued polynomial of order 2N + 1 with the coefficient of highest order term satisfying (-1) N a N > 0. If T > 0 is given, by our assumption, there exist M > 0 and

C 1 > 0 such that Q ′ (ξ)T ≥ C 1 ξ 2N whenever |ξ| > M . Then, for x ≤ -1 and T > 0, Λ ǫ u n (x, T ) = 1 2π ∞ -∞ e i Q(ξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ)dξ = 1 2π |ξ|>M e i Q(ξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ)dξ + 1 2π |ξ|≤M e i Q(ξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ)dξ , where 1 2π |ξ|≤M e i Q(ξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ)dξ ≤ 1 2π (2M ) 1/2 (1 + M 2 ) ǫ/2 φ n L 2 (R) , 1 2π |ξ|>M e i Q(ξ)T -ixξ (1 + ξ 2 ) ǫ/2 φn (ξ)dξ = 1 2π |ξ|>M (1 + ξ 2 ) ǫ/2 φn (ξ) i( Q ′ (ξ)T -x) ξ e i( Q(ξ)T -xξ) dξ = 1 2π |ξ|>M (1 + ξ 2 ) ǫ/2 e i50ξ χ n (ξ) i( Q ′ (ξ)T -x)(1 + ξ 2 ) 1/4 (1 + ln(1 + ξ 2 )) 2 ξ e -i( Q(ξ)T -xξ) dξ
For |ξ| > M , we have

|w n (ξ)| := (1 + ξ 2 ) ǫ/2 e i50ξ χ n (ξ) i( Q ′ (ξ)T -x)(1 + ξ 2 ) 1/4 (1 + ln(1 + ξ 2 )) 2 ξ e -i( Q(ξ)T -xξ) ≤ C (C 1 ξ 2m T + |x|)(1 + ξ 2 ) 1 4 -ǫ 2 (1 + ln(1 + ξ 2 )) 2 ≤ C ξ 2m + 1
,

where 1 4 -ǫ 2 ≥ 0 and C > 0 is independent of n. Hence, ∞ -∞ p(x) (Λ ǫ u n (x, T )) 2 dx ≤ C -1 -110 p(x) |ξ|>M |w n (ξ)|dξ + (2M ) 1/2 2π (1 + M 2 ) ǫ/2 φ n L 2 (R) 2 dx ≤ C -1 -110 p(x)dx < +∞
Therefore, (2.3)-(2.6) yield a contradiction, which implies that there does not exist any ǫ > 0 such that (1.16) holds true. The theorem is proved.

3 Proof of Theorem 1.2

By assumption, there exists a N > 0 such τ = p(ξ) is invertible on (N, +∞) and

π(ξ) ∼ ξ m , ξ = ν(τ ) ∼ τ 1/m , p ′ (ξ) ∼ τ m-1 as τ → +∞.
By contradiction, assume that (1.19) holds true for some ǫ > 0. Without loss of generality, we assume that s = 0 and that 0 < ǫ < 1 2 . Let η be the function as defined in the proof of Theorem 1.1. For any integer n ≥ 1, let µ n (ξ) be a C ∞ cut-off function such that

µ n (ξ) = 1 ξ ∈ [N, n + N ] 0 for ξ ≤ N and ξ ≥ n + N + 1
and ψ n ∈ L 2 (R) be the function whose Fourier transform is

ψn (ξ) = µ n (ξ) (1 + ξ 2 ) 1/4 (1 + ln(1 + ξ 2 )) 2 = µ n (ξ)η(ξ).
Then, for any n ≥ 1,

(i) Λ ǫ ψ n ∈ L 2 (R) and lim n→+∞ Λ ǫ ψ n L 2 (R) = ∞, (ii) there exists C 0 > 0 such that ∞ -∞ |ψ n (x)| 2 dx ≤ C 0 , max |x|≥1 (|ψ n (x)| + |Λ ǫ ψ n (x)|) ≤ C(1 + |x|) -2 .
Let v n be the solution of (1.18) with ψ replaced by ψ n . Since (1.19) holds true, we must have

T -T |x|≤R Λ (m-1)/2+ǫ v n (x, t) 2 dxdt ≤ C ψ n 2 L 2 (R) < +∞. ( 3.1)
The left-hand side of (3.1) can be written as

T -T |x|≤R Λ (m-1)/2+ǫ v n (x, t) 2 dxdt = I n -J n , with I n = R -R ∞ -∞ Λ ǫ+ m-1 2 v n (x, t) 2 dt dx, J n = R -R ∞ T + -T -∞ Λ ǫ+ m-1 2 v n (x, t) 2 dt dx.
Let us prove that (3.1) cannot be true by showing that lim n→+∞ I n = +∞ and sup 1≤n<+∞ J n < +∞.

We first prove that, for any n ≥ 1,

∞ -∞ Λ ǫ+ m-1 2 v n (x, t) 2 dt = C Λ ǫ ψ n 2 L 2 (R) for any x ∈ R. (3.2) Since ∞ -∞ Λ ǫ+ m-1 2 v n (x, t) 2 dt = ∞ -∞ 1 2π ∞ -∞ (1 + ξ 2 ) ǫ 2 + m-1 4 e -i(tp(ξ)-xξ) ψn (ξ)dξ 2 dt = C ∞ -∞ ∞ N (1 + ξ 2 ) ǫ 2 + m-1 4 e -i(tp(ξ)-xξ) µ n (ξ)η(ξ)dξ 2 dt = C ∞ -∞ ∞ M (1 + ν 2 (τ )) ǫ 2 + m-1 4 e -i(tτ -xν(τ )) µ n (ν(τ ))η(ν(τ ))ν ′ (τ )dτ 2 dt = C ∞ -∞ ∞ -∞ e -itτ w n (x, τ )dτ
x ∈ R, ∞ -∞ Λ ǫ+ m-1 2 v n (x, t) 2 dt = C ∞ -∞ |w n (x, τ )| 2 dτ = C ∞ 1 (1 + ν 2 (τ )) ǫ 2 + m-1 4
µ n (ν(τ ))η(ν(τ ))ν ′ (τ ) where C > 0 is independent of n, but may depend on T and R. The theorem is proved.

  and v(•, t) ∈ H s (R) if and only if ψ ∈ H s (R) for any t ∈ R, they possess a local smoothing property:φ ∈ H s (R) =⇒ u ∈ L 2 (-T, T ; H s+1 loc (R)) for any T > 0, and ψ ∈ H s (R) =⇒ v ∈ L 2 (-T, T ; H s+1/2 loc (R)) for any T > 0.

  p(x) = 1 for any x ∈ [-99, -5], 0 for any x / ∈ [-110, -1].

2 + m- 1 4

 21 x, τ ) = ((1 + ν 2 (τ )) ǫ e ixν(τ )) µ n (ν(τ ))η(ν(τ ))ν ′ (τ )for τ ≥ M and w n (τ ) = 0 for τ ≤ M , by the Plancherel theorem, we have, for any

1 ( 1 + ξ 2 ) ǫ 2 + m- 1 4 2 dξ= C Λ ǫ ψ n 2 L 2 (R) , and therefore, I n = 2RC Λ ǫ ψ n 2 L 2 ( 1 4 1 4

 11212222211 µ n (ξ)η(ξ) ν ′ (p(ξ)) R) → +∞ as n → +∞.It remains to show that sup 1≤n<+∞ J n < +∞. We only consider the term J n,T := similar. Using integration by parts, we get that, for |x| ≤ R andT ≥ R + 1 , e -i(tp(ξ)-xξ) µ n (ξ)η(ξ)dξ µ n (ξ)η(ξ) -i(tp ′ (ξ) -x) ξ e -i(tp(ξ)-xξ) dξ 2 dt (3.3)where|tp ′ (ξ) -x| ≥ |t||p ′ (ξ)| -R ≥ |t| + T -R ≥ |t| + 1 or |tp ′ (ξ) -x| ≥ ξ m-1 ,for ξ ≥ N . Therefore, by performing integrations by parts in (3.3) and noticing that each of them produces at least one factor of the order of |ξ| -1 , we see that the integral in (3.3) with respect to ξ is finite and still has a term tp ′ (ξ) -x in the denominator such that

Acknowledgment. S. M. Sun was partially supported by the National Science Foundation under grant No. DMS-1210979. B.-Y. Zhang was supported by a grant from the Simons Foundation (201615), NSF of China (11231007, 11571244).


domain: info math

text:
André Hirschowitz

Marco Maggesi

Nested Abstract Syntax in Coq

Keywords: POPLmark, Abstract Syntax, Semantics, Nested Datatypes, Coq, System F<:

come

Introduction

We present a partial solution to the POPLmark Challenge (Aydemir et al., 2005) in the Coq proof assistant. Our formalization addresses part (1A) of the Challenge, concerning the transitivity property of the subtyping relation of System F <: . The specific feature of our solution is the use of nested datatypes to encode the syntax of System F <: . Accordingly, we propose an original "higher-order" encoding of environments, as functions on the varying set of variables.

Nested datatypes, also called heterogeneous datatypes, have been popularized by the work of Bird and Meertens (Bird and Meertens, 1998). It is a general technique to enforce certain invariants through typing, which allows a high-level and perfectly natural representation of variable binding, as was experienced already ten years ago (Altenkirch and Reus, 1999;Bird and Paterson, 1999). We propose the name "Nested Abstract Syntax" for this (old) approach, which we see as an alternative in particular to Higher Order Abstract Syntax (Pfenning and Elliott, 1988;Lee, Crary and Harper, 2007) and to Weak Higher Order Abstract Syntax (Honsell, Miculan and Scagnetto, 2001).

Here are some advantages of using this technique:

-Typing is refined, taking into account the variation of the set of free variables.

-There is no α-equivalence, which makes life much simpler. It may be considered as a kind of de Bruijn encoding enriched with an enlightening typing discipline (Bird and Paterson, 1999).

-Substitution is perfectly understood in a high-level way, as the main ingredient of the monadic structure (see, e.g., (Altenkirch and Reus, 1999)).

Despite these advantages, nested datatypes seem to have been employed only sparsely in real formalizations of higher-order languages. Besides the first achievements mentioned above, we may quote our earlier (Hirschowitz and Maggesi, 2007) and the contributions of Matthes (Matthes, 2008a;Matthes, 2008b;Matthes, 2009). In particular, we are not aware of other implementations of System F <: based on nested datatypes.

From our point of view, the main conclusions of our experience are -Nested Abstract Syntax is perfectly suited for formalizations of the present kind.

-Coq offers convenient support in order to program statements in this style with a satisfactory level of readability.

-On the other hand, Coq does not yet offer sufficient support for easy proving in this style, due to the systematic use of dependenttypes.

-The formalization of a computer language as designed by the POPLmark Challenge has revealed to be an excellent benchmark for the overall maturity and expressiveness of our favorite theorem prover.

The complete source code of the formalization exposed in this paper can be freely downloaded from the web page of the second autor: http://www.math.unifi.it/~maggesi/ .

The Option

The characteristic feature of the nested approach is best understood through the typing, within the untyped lambda-calculus, of the abstraction operator:

abs : term ^V → term V.
Here, given the type V (V for variables), we consider a new type ^V which denotes V extended with a new distinguished element (the "fresh" variable). This is realized by the option datatype that is defined as follows.1

Inductive option (A:Type) : Type := | Some : A -> option A | None : option A.

The option type comes equipped with a companion operator option_map which gives its functor structure:

Definition option_map (A B:Type) (f:A->B) (x:option A) : option B := match x with | Some a => Some (f a) | None => None end.

The terms option and option_map are heavely used in this work, thus we extend the Coq syntax with a special notation for them given by a prefixed hat.2

Notation "^f" := (option_map f). Notation "^X" := (option X) : type_scope.

Nested Encoding of F <:

Here we describe our encoding of F <: -types.

Nested Syntax for F <:

We recall that type expressions in F <: are constructed according to the following grammar

T ::= types Top maximum type X type variable T → T type of functions ∀X<:T.T universal type
where in the universal type ∀X <: S.T the variable X is bound in T .

We define an inductive type ftype V which represents the set of type expressions over the context V as follows Inductive ftype (V:Type) : Type :

= | Top : ftype V | TVar : V -> ftype V | Arr : ftype V -> ftype V -> ftype V | Uni : ftype V -> ftype ^V -> ftype V.
The occurrence of the option type ^V in the signature reveals the presence of a binding construction, more precisely that a new variable (the "freshest" one) is bound in the second argument of the constructor Uni. For better readability, we introduce the syntactic sugar s --> t and all s, t to denote Arr s t and Uni s t respectively. Let us discuss how far we stand from the specification:

-Our ftype is stratified, hence, for instance, we have one term Top for each context V . We would be happy to read Top V instead of Top V , but this is not (yet?) possible in Coq.

-For a "variable" v ∈ V , TVar v is in ftype V while v itself is not. So here we depart slightly from the specification. From the theoretical point of view, this may be presented as a clarification.

On the other hand, from the pretty-print point of view, it would have been fine to consider TVar as a coercion. Unfortunately, this could not be performed smoothly in Coq.

-In our syntax for Uni, the bound variable does not show up. As far as meta-theory is concerned, this may be considered a good thing.

Recursion and the like

A crucial advantage of our encoding is that Coq provides for free the recursion and induction principles which we need. Furthermore Coq provides us with tactics dedicated to inductive types, notably -injection derives new equalities from old ones by applying the injectivity of the constructions of our inductive type.

-discriminate searches for an absurd assumption, claiming that two structurally different terms (like Top V and Top V → Top V ) are equal.

Note that the fact that Coq handles such nested inductive types is pretty recent (version 8.1). More general forms of inductive types, involving for instance constructions like the explicit substitution:

expl subst : term(term V ) → term V
cannot yet be implemented so smoothly in Coq, and are the object of active research (Matthes, 2008a;Matthes, 2008b;Matthes, 2009).

Renaming

The assignment V → ftype V is endowed with a structure of functor through renaming. This is defined using the recursion principle (Fixpoint) as follows:

Fixpoint ftype_map V W (f:V->W) (t:ftype V) : ftype W := match t with | Top => Top W | TVar X => TVar (f X) | S --> T => %f S --> %f T | all S,
T => all %f S, %(^f) T end where "% f" := (ftype_map f).

Functoriality

The functoriality of our renaming can be easily stated (and proven):

Lemma ftype_map_id : forall V (t:ftype V) (f:V->V), (forall x, f x=x) -> %f t=t.
Lemma ftype_map_comp : forall U t V (f:U->V) W (g:V->W), %g (%f t) = %(g o f) t.

Substitution

The renaming functor can be upgraded into a monad, just in the way it is done for the λ-calculus e.g. in (Altenkirch and Reus, 1999). In fact, this substitution and its main properties could be generated from the signature, just as is the recursion principle.

4. Stratified Environments for F <:

Environments as Functions

As for type expressions, type environments are stratified over contexts. We simply encode them as maps V → ftype V .

Definition env V := V->ftype V.
This is slightly too simple, and we will introduce in the next section an additional well-formedness condition RWF. On the other hand, thanks to this encoding, the judgement TVar x <: t ∈ Γ, which means that the variable x is bound to the value t in the environment Γ, is readily translated into the equation Γ x = t, and thus need no programming.

Adding a Binding

The operation of adding a new binding in the environment is denoted Γ & t and is implemented by the following definition.

3 Definition consenv V (G:env V) (t:ftype V) : env ^V := fun x => match x with | None => %(@Some V) t | Some x => %(@Some V) (G x) end. Notation "G & t" := (consenv G t)
(at level 50, left associativity).

This can be pictorially represented by the following commutative diagram:

ftype V / / ftype ^V V @Some V / / Γ O O ^VΓ&t O O
where the environment Γ is extended to Γ & t by adding a binding for a "fresh" type variable. Note that this commutative diagram has a lifting property: it can be completed with a map h : ^V → ftype V .

Extending Environments

The concatenation of environments is a crucial operation in the proof of the transitivity. The typing of this operation is slightly subtle: what is the nature of ∆ in the concatenation Σ = Γ, ∆? Although this question can, of course, be answered in a satisfactory way, our choice has been to avoid this problem. We take advantage of the fact that the knowledge of Γ and ∆ is equivalent to the knowledge of Γ and Σ, and formalize concatenation through extensions.

Given a commutative diagram

ftype V %f / / ftype W V Γ O O f / / W ∆ O O
we say that ∆ is a raw extension of Γ along f . We reserve the word extension for well-formed extensions. Indeed, for extensions as for environments, we need a well-formedness predicate. As a matter of fact, in the next section, we will define well-formedness of environments in terms of well-formedness of extensions.

The environment expression

Σ = Γ, X <: Q, ∆
is formalized as a sequence of two extensions

ftype V / / ftype ^V / / ftype W V Γ O O / / ^V Γ & Q O O / / W. Σ O O

Well-Formedness

Our very simple notion of environment leaves room for exotic terms. Indeed, in well-formed environments, each variable has to be bound to a type which only depends upon "earlier" variables. For instance, we have to rule out, for a non empty type V , the exotic environment TVar : V → ftype V . We found it convenient to first introduce a relative well-formedness predicate for extensions of environments. Our notion of well-formedness will allow us to merge the permutation lemma and the weakening lemma (see section 7).

Relative Well-Formedness

We introduce a ternary predicate for relative well-formedness (RWF)

Σ extends Γ along f defined inductively through two introduction rules, corresponding to the familiar nil+cons scheme.

The nil rule roughly says that the "empty" extension is well-formed4 :

RWF_refl : forall V (G G':env V) (f:V->V), G==G' -> (forall x, f x = x) -> G' extends G along f
The cons rule says that the composition of two sequential extensions, as pictured in the following diagram, is well-formed as soon as the left hand square is well-formed and the right hand square is commutative:

ftype V % f 1 / / ftype W % f 2 / / ftype X V Γ 1 O O f 1 / / W Γ 2 O O f 2 / / X Γ 3 O O h h h Q Q Q Q Q Q Q Q Q Q Q Q Q Q
This commutativity of the right hand side of the diagram expresses that variables in X are bound to terms in ftype W . Note that, thanks to the nil rule, the right hand square is a well-formed extension too, as we will state formally below.

Altogether, our inductive declaration reads as follows:

Inductive RWF : forall W (D:env W) V (G:env V) (f:W->V), Prop := | RWF_refl : forall V (G G':env V) (f:V->V), G==G' -> (forall x, f x = x) -> G' extends G along f | RWF_append : forall V1 (G1:env V1) V2 (f1:V1->V2) V3 (G3:env V3) (f2:V2->V3) (f:V1->V3) (E:V3->ftype V2), (forall x, G3 x = %f2 (E x)) -> (forall x, f2 (f1 x) = f x) -> E o f2 extends G1 along f1 -> G3 extends G1 along f where "D 'extends' G 'along' f" := (RWF G D f).
Note that we made no injectivity assumption on the function f in the judgment Σ extends Γ along f . In fact, there are basically two classes of extensions that we are interested in.

-The first case is when the reindexing map f is a proper injection. This is the case where the term extension of environments is most appropriate.

-The second case is when f is a bijection. Here we may think of f as a permutation of the bindings of the environment, and the judgement ∆ extends Γ along f may be interpreted as f is an allowed permutation transforming Γ into ∆. Note that the notion of permutation alluded to in the paper version should be a change of order on the fixed set of variables, rather than a permutation of this set in the usual sense.

Reasoning with Well-Formed Extensions

The inductive declaration of the RWF predicate generates the desired induction principle which allows to reason smoothly about it.

For instance, we prove easily that a well-formed extension is actually an extension:

Lemma RWF_commute : forall W (D:env W) V (G:env V) (f:W->V), (G extends D along f) -> forall y, G (f y) = %f (D y).
Similarly we prove that well-formedness is extensional:

Lemma RWF_extens : forall W (D D':env W) (HD : D==D') V (G G':env V) (HG : G==G') (f f':W->V) (Hf : f==f'), G extends D along f -> G' extends D' along f'.

We also prove that the composition of two well-formed extensions is well-formed again:

Lemma RWF_trans : forall V1 (G1:env V1) V2 (G2:env V2) (f1:V1->V2) V3 (G3:env V3) (f2:V2->V3) (f:V1->V3), G2 extends G1 along f1 -> G3 extends G2 along f2 -> (forall x, f2 (f1 x) = f x) -> G3 extends G1 along f. Finally we check that the consenv construction yields well-formed extensions:

Lemma RWF_consenv : forall V (G:env V) (t:ftype V),
G&t extends G along @Some V.

The proof is a direct application of the cons rule (RWF_append) In the required diagram

ftype V / / ftype ^V V Γ O O @Some V / / ^VΓ&t O O h h h Q Q Q Q Q Q Q Q Q Q Q Q Q Q h is given by h (Some v) = Γ v for all v ∈ V h None = %(@Some V ) t

Absolute Well-Formedness

Finally, we recover the absolute notion of well-formedness as follows.

An environment Γ is well-formed, noted WF Γ, if it is well-formed with respect to the empty environment (the obvious environment over the empty context). We denote by empty the empty inductive type and by empty_inc (V:Type), empty -> V the associated initial map.

Definition WF V (G:env V) := G extends @empty_inc _ along @empty_inc V.

As immediate corollaries of lemmas RWF_trans and RWF_consenv we obtain the following two basic properties of WF: Lemma WF_trans : forall W (D:env W) V (G:env V) (f:W->V), WF D -> G extends D along f -> WF G.

Lemma WF_consenv : forall V (G:env V) (t:ftype V), WF G -> WF (G & t).

6. Subtyping

The Subtyping Predicate

We are now ready to define the subtyping judgement Γ s <: t of F <: . This is denoted G |~s << t in the machine syntax and encoded through an inductive predicate as follows:

Inductive sub : forall V (G:env V) (s t:ftype V), Prop := | SA_Top : forall V (G:env V) (s:ftype V), WF G -> G |--s << Top _ | SA_Refl_TVar : forall V (G:env V) (x:V), WF G -> G |--TVar x << TVar x | SA_Trans_TVar : forall V (G:env V) (x:V) t, G |--G x << t -> G |--TVar x << t | SA_Arrow : forall V (G:env V) (s1 s2 t1 t2:ftype V), G |--t1 << s1 -> G |--s2 << t2 -> G |--s1 --> s2 << t1 --> t2 | SA_All : forall V (G:env V) (t1 s1:ftype V) (s2 t2:ftype ^V), G |--t1 << s1 -> G & t1 |--s2 << t2 -> G |--all s1, s2 << all t1, t2
where "G |--s << t" := (sub G s t).

This definition is pretty close to the paper specification, with one constructor for each inference rule. Let us review the differences:

-In the Trans_TVar construction, we have only one premise, thanks to the functional nature of our environments.

-We have two occurrences of the W F predicate. We could easily have been closer to the paper version by defining a type for wellformed environments. We have preferred to make apparent that the well-formedness assumption is useful only in the rules without any premise (namely the first two ones).

Reflexivity and Adequacy

We can state the reflexivity statement as follows

Lemma sub_refl : forall V (G:env V) t, WF G -> G |--t << t.
and its proof is straightforward.

Our adequacy statement for the subtyping, which says that subtyping entails well-formedness reads as follows:

Lemma sub_WF : forall V (G:env V) s t, G |--s << t -> WF G.
and its proof is also straightforward.

Merging Permutation and Weakening

The Paper Version

The F <: -theory contains two lemmas respectively for weakening and permutation. The permutation lemma reads as follows Lemma 1. (Permutation) If ∆ is a well-formed permutation of Γ then Γ S <: T implies ∆ S <: T . with a rather long and low-level definition of what is a well-formed permutation.

On the other hand, the weakening lemma reads Lemma 2. (Weakening) If Γ S <: T and dom(Γ) ∩ dom(∆) = ∅, then Γ, ∆ S <: T . This formulation involves the concatenation operation on environments. As already mentioned, the typing of ∆ in the concatenation Γ, ∆ is not completely evident. For the present weakening lemma, a cautious interpretation would be to understand ∆ simply as an environment, just as Γ. But this would not cover the intended meaning of the lemma, namely the case where values in ∆ are allowed to involve variables in Γ. For this case, a subtler typing of ∆ is in order.

A Merging Interpretation

Our solution avoids this problem: when faced with Σ := Γ, ∆, we type Σ (instead of ∆), and just say that Σ is a well-formed extension of Γ. This approach offers a new perspective where our two lemmas can be merged. The unified formulation is even more general than the conjunction of the two lemmas, since non injective renamings are allowed:

Lemma sub_weakening : forall W (D:env W) (s t:ftype W), D |--s << t -> forall V (G:env V) (f:W->V), G extends D along f -> G |--%f s << %f t.
The case where f is a bijection accounts for the permutation lemma, while the case where f is a (proper) injection accounts for the weakening lemma. The proof of our sub_weakening lemma is straightforward.

Transitivity and Narrowing

We now turn to the main results of part (1A) of the Challenge, that is, the proof of the transitivity property for the subtyping relation. In this proof, the transitivity property is coupled with the so-called narrowing property.

Statements

We begin with the statement of the transitivity lemma which should not give any surprise:

Lemma transitivity : forall V (G:env V) s q t, G |--s << q -> G |--q << t -> G |--s << t.
The statement of the narrowing lemma is slightly more problematic. Let us first recall the paper version:

Lemma 3. (Narrowing) If Γ, X <: Q, ∆ M <: N and Γ P <: Q then Γ, X <: P, ∆ M <: N .
The difficulty comes from the concatenated environments. As explained in section 4.3 we solve this problem by rephrasing the statement in terms of well-formed extensions of environments. We introduce two environments D and D' over the context W, which are meant to correspond to Γ, X <: P, ∆ and Γ, X <: Q, ∆ respectively.

So we have an environment G over V and two extensions D and D' of G&p and G&q respectively, along the same map f:^V->W.

Our next task is to express that D and D come from the same ∆, in other words that they agree outside f (^V ). As a matter of fact, we define agreement outside a value instead of outside a map. Here is our definition:

Definition agrees_outside V (D E:env V) x : Prop := forall y, y = x \/ D y = E y. Notation "D 'agrees' 'with' E 'outside' x" := (agrees_outside D E x) (at level 70).

Now we can state our version of the narrowing lemma.

Proofs

Following a scheme found in the formalization by Chargueraud5 we divide the common inductive proof of transitivity and narrowing in two sub-lemmas, namely, transitivity_lemma and narrowing_lemma.

The results in which we are actually interested, i.e., transitivity and narrowing, are easy consequences of these lemmas.

In view of the transitivity_lemma we introduce a variant of the obvious property "q is transitive". The latter reads:

Definition transitive : forall V (q:ftype V), Prop := forall (G:env V) s t, G |--s << q -> G |--q << t -> G |--s << t.
Our variant is the apparently stronger "q is universally transitive":

Definition univ_trans : forall V (q:ftype V), Prop := forall W (f:V->W) G s t, G |--s << %f q -> G |--%f q << t -> G |--s << t.
Now we can state the transitivity_lemma:

Lemma transitivity_lemma : forall V (q:ftype V), univ_trans q.

In a similar way, we have to somehow recast our narrowing lemma:

Lemma narrowing_lemma : forall V (q:ftype V) (trs:trans_prop q) W ( Note that the assumptions are arranged in a way better suited for our planned induction. Note also that the assumptions are given names: this is for easier proofs. Our proof of this lemma is the most involved one in our code, with around forty tactics. Our proof of our transitivity_lemma is much simpler, with around twenty tactics. Of course, it invokes our narrowing_lemma.

Conclusions

This work aimed at positioning Nested Abstract Syntax (NAS) with respect to the main approaches to the binding representation problem. Here are our thoughts in this matter.

-With respect to first-order approaches, notably de Bruijn nameless encoding, we hope to have demonstrated that NAS avoids α-equivalence and related problems, like de Bruijn encoding, while allowing statements with a high-level of readability.

-With respect to higher-order approaches like HOAS (Pfenning and Elliott, 1988), WHOAS (Honsell, Miculan and Scagnetto, 2001), Nominal Logic (Gabbay and Pitts, 2002), we insist on the fact that NAS need no specific logical apparatus, and offers a high-level point of view, perfectly compatible with our everyday logic.

Since at least we are convinced that NAS is a perfect solution to the binding representation problem, the next question is whether it is ready "for the masses". Here is our answer:

-We have to admit that NAS requires a large amount of dependent typing. This should not be a bad point. Unfortunately, it occurs that dependent types easily bring Coq beyond its current capabilities. This does not appear in our formalization just because each time we were stuck, we have been able to find a better way to avoid the problem. Nevertheless, in our opinion, this is the main obstacle which will prevent the "masses" to use NAS.

-The second obstacle is probably the syntax allowed by Coq, which, although fairly sophisticated, is still far from what is allowed for instance by T E X.

-Finally, the "masses" would certainly appreciate a system generating more material, in particular the monadic and parallel substitutions associated with a given signature and their main properties. It is not yet clear to us how will develop our new approach to environments through functions and extensions, but we anticipate that some material could be generated also concerning these environments.

Let us end with a few more remarks:

-Concerning conciseness, we have elaborated a small test in order to compare the various existing solution to Part 1A of the POPLmark Challenge. We estimate the total amount of the information contained in our code by measuring the size of the compressed sources. Thus we tried to compare the gzipped size of our code with some other available formalizations written in Coq. The results obtained are summarized in the following Some formalizations are built on top of some kind of general purpose library, in which case we tried to evaluate the size of the library (reported in the column Extras) separately from the size of the code specific for the solution of the Challenge.

-When formalizing a theory, possibly pushed by the limitations of the system in use, one is often tempted to explore new definitions and proofs. This is part of a general process: we anticipate that computer proofs will more and more influence paper proofs.

Although the formulation of the POPLmark Challenge did not leave much room for such exploration, we did not fully resist to the temptation. In particular, we have coined a new approach to environments through functions and extensions, allowing a nice merge of the permutation and weakening lemma. We hope that this approach will be fruitful again in the future.

-A word is in order to explain why we solved only part 1A of the POPLmark Challenge. The answer is just a matter of priority, we did not start yet to try the next part.

  env V) W (D D':env W) (f:^V->W) p q m n, D agrees with D' outside f None -> D extends G&p along f -> D' extends G&q along f -> G |--p << q -> D' |--m << n -> D |--m << n.

  D':env W) m n (Hq : D' |--m << n) (G:env V) (D:env W) (f:^V->W) (Hf : D agrees with D' outside f None) p (RWFp : D extends G&p along f) (RWFq : D' extends G&q along f), G |--p << q -> D |--m << n.

  table. 6

	Contribution	Part 1A Extras
	B. Aydemir et al.	2.5 Kb 16.4 Kb
	A. Chlipala	2.3 Kb	2.6 Kb
	A. Hirschowitz & M. Maggesi	4.2 Kb	0 Kb
	X. Leroy	5.0 Kb	1.0 Kb
	J. Vouillon	4.6 Kb	0 Kb

fsubwf.tex; 7/07/2009; 1:28; p.2

The definitions of option and option map that follows are taken from the Coq Standard Library. The option datatype is also known as maybe in other contexts, for instance in the Haskell community.

Coq's extensible syntax uses a type driven scope mechanism which is able to disambiguate the two notations. fsubwf.tex; 7/07/2009; 1:28; p.3

fsubwf.tex; 7/07/2009; 1:28; p.4

fsubwf.tex; 7/07/2009; 1:28; p.5

The prefix "@" disables the implicit arguments mechanism. fsubwf.tex; 7/07/2009; 1:28; p.6

fsubwf.tex; 7/07/2009; 1:28; p.7

The double equality == stands for the extensional equality of functions. fsubwf.tex; 7/07/2009; 1:28; p.8

fsubwf.tex; 7/07/2009; 1:28; p.9

fsubwf.tex; 7/07/2009; 1:28; p.10

fsubwf.tex; 7/07/2009; 1:28; p.11

fsubwf.tex; 7/07/2009; 1:28; p.12

fsubwf.tex; 7/07/2009; 1:28; p.13

http://www.chargueraud.org/arthur/research/2006/poplmark/ fsubwf.tex; 7/07/2009; 1:28; p.14

fsubwf.tex; 7/07/2009; 1:28; p.15

These statistics have been obtained by removing comments and code which does not appear to be necessary for addressing part 1A and by compressing the files with gzip with the option --best. The whole process has been carried on mostly by hand, which means that it can be affected by errors. fsubwf.tex;

7/07/2009; 1:28; p.16