P063 · Inconvenient Pairs / 不方便的居民对

English

A city occupies the square [0, 1000000] × [0, 1000000]. The strictly increasing arrays xs and ys give the coordinates of its vertical and horizontal streets. Each street crosses the whole city and can be travelled in either direction. The four boundaries are streets.

Person i stands at (px[i], py[i]), on at least one street. All people occupy distinct points. A pair is inconvenient if its shortest route along streets is strictly longer than its Manhattan distance. Count unordered pairs, counting each pair once.

Prove the supplied function, which handles one test case:

long long solver(const int *xs, int n, const int *ys, int m,
                        const int *px, const int *py, int k,
                        int *va_grp, int *va_key,
                        int *ha_grp, int *ha_key);

The constraints are:

• 2 <= n, m <= 200000, 2 <= k <= 300000.
• Each street array is strictly increasing, starts at 0, ends at 1000000, and has every coordinate in [0, 1000000].
• Every resident coordinate is in [0, 1000000]; each resident is on at least one street, and resident positions are distinct.
• All eight arrays occupy disjoint memory.
• The four work arrays contain initialized integers with arbitrary values. Their contents may change; their full array ownership is returned.

The function returns a signed 64-bit count and preserves all four input arrays. The caller supplies the arrays and invokes this function directly.

Fixed implementation

All six executable functions are supplied:

1. strip uses binary search to find the last street coordinate <= v. It returns -1 on a street, otherwise the index of the gap containing v.
2. item_less compares (group, key) records lexicographically.
3. sift_items restores a max heap by selecting its larger child and swapping both the group and key cells together.
4. sort_items builds the heap and repeatedly extracts the maximum, sorting the parallel arrays in lexicographic order.
5. count_pairs sorts its records. For each strip it adds g * (g - 1) / 2, then subtracts same * (same - 1) / 2 for each equal-coordinate run.
6. solver classifies residents into the two active prefixes, omits crossings, and adds the counts from the two orientations.

The implementation uses four work arrays. Variables are declared before for loops, and some array reads and Boolean branches are made explicit. The cap used in helper contracts is a mathematical ghost parameter; it is not an executable argument.

Time complexity is O(k * (log n + log m + log k)), with O(k) caller-provided workspace. The maximum possible pair count is k * (k - 1) / 2, which can exceed a signed 32-bit integer.

Specification

The ghost list people : (int#int)list records coordinate pairs; person_x and person_y record the input arrays and must agree with its projections. The header supplies these mathematical definitions:

• Pre states street membership, strict street ordering, boundary coordinates, and distinct resident positions. Size and coordinate bounds also appear in the function precondition.
• StreetWalk is a nonempty list of vertices joining the endpoints, with each step lying on a street. WalkLength sums the Manhattan lengths of its edges.
• StreetDistance requires an attained minimum over those walks.
• Inconvenient requires that minimum to be strictly greater than Manhattan distance. Spec counts the finite set of inconvenient index pairs i < j.
• FullShape(p, n) is existential ownership of an initialized integer array of length n.
• ParallelPermutation compares the multiplicities of complete (group, key) records, preserving their association. CombinePoints truncates to the shorter list, as Coq combine does.
• The header supplies the heap and pair-count predicates required by the executable helper contracts. sift_items and sort_items additionally ensure preservation of PairCount, a proved consequence of their parallel permutation guarantee.

Define any auxiliary predicates and prove the lemmas needed for your invariants in starter.c; the header supplies only the contract model and its dependencies.

All contract arithmetic is mathematical integer arithmetic. Header definitions introduce no unproved correctness assumptions. The implementation and contracts are fixed; add invariants and proof code in starter.c. Submit that file once its proof is complete.

中文

城市是正方形 [0, 1000000] × [0, 1000000]。严格递增的数组 xs、ys 分别给出竖直街道的横坐标和水平街道的纵坐标。每条街道贯穿整座城市，可以双向通行，城市四条边界也属于街道。

第 i 个居民位于 (px[i], py[i])，至少在一条街道上，且所有居民的位置互不相同。如果两人之间沿街道行走的最短距离严格大于其曼哈顿距离，则称他们构成一对不方便的居民对。计算这样的无序居民对数量，每对只计一次。

函数一次处理一个测试用例，签名及八个数组的长度见上表。要求：

• 2 <= n, m <= 200000，2 <= k <= 300000。
• 两个街道数组严格递增，首元素为 0，末元素为 1000000，坐标均在 [0, 1000000] 范围内。
• 居民坐标均在该范围内，每人至少处于一条街道上，位置互不相同。
• 八个数组的存储空间互不重叠。四个工作数组均已初始化，初值任意。
• 返回有符号 64 位计数，保持 xs、ys、px、py 不变，并归还四个工作数组的完整所有权。工作数组内容允许改变。

给定实现与规约

给定实现包含六个函数：strip、item_less、sift_items、 sort_items、count_pairs、solver。先二分定位条带，将非交叉点居民分类存入两个有效前缀；随后对 (条带编号, 坐标) 平行数组进行堆排序。对每个条带，先加上该组所有居民对的数量，再减去坐标相同的居民对数量。最后将两个方向的计数相加。

实现使用四个工作数组。变量声明位于 for 循环前，部分数组读取、布尔分支显式展开。辅助函数规约中的 cap 仅为数学幽灵参数，不是运行时参数，也不需要额外桶数组。

时间复杂度为 O(k * (log n + log m + log k))，调用者提供的工作区为 O(k)。答案可能超过有符号 32 位整数范围。无须编写输入解析或 main。

幽灵列表 people 记录坐标对，并通过投影等式与 person_x、 person_y 对齐。Pre 表示合法街道、居民在街道上及位置互异等条件；输入规模与坐标边界写在函数前置条件中。

StreetWalk 表示非空街道路径，WalkLength 表示各段长度之和， StreetDistance 要求存在达到最小值的路径。Inconvenient 要求最短距离严格大于曼哈顿距离，Spec 则对满足条件的 i < j 下标对集合取基数。规约不是算法执行结果的重新定义。

FullShape(p, n) 表示对长度为 n 的已初始化整数数组的存在量化所有权，隐藏工作数组的具体初值。 ParallelPermutation 保持完整 (条带编号, 坐标) 记录的重数，不能独立打乱两列。头文件还提供运行时辅助函数规约所需的堆性质与计数定义。 sift_items 和 sort_items 还保证 PairCount 不变；这是已证明的平行排列性质的推论。

请在 starter.c 中自行定义不变式所需的辅助谓词并证明所需引理；头文件仅提供规约模型及其依赖定义。

契约中的整数均为数学整数。给定定义不引入未经证明的正确性假设。实现与契约固定，只在 starter.c 中添加不变式和证明代码，完成后提交该文件。

Examples / 示例

The original sample contains two test cases; each becomes one function call. 原样例包含两个测试用例，各对应一次函数调用。