LIS with Binary Search / LIS + 二分优化

English

Given an integer array nums of length n, prove that the supplied function length_of_lis_binary_search(nums, n, tails) returns the length of its longest strictly increasing subsequence. A subsequence retains the original index order, but its elements need not be adjacent. Equal values cannot extend it.

The input satisfies the following constraints:

• 0 <= n <= 100000, and nums has exactly n elements.
• Elements may be any signed 32-bit integers, including -2147483648 and 2147483647; there is no smaller element-value bound.
• The caller provides a writable tails array of exactly n integers. Its initial integer values are arbitrary, as recorded by the ghost list tails_l.
• The two arrays occupy disjoint memory, as expressed by separating ownership in the contract. For n = 0, either pointer may be null; no element is accessed.

The implementation maintains an active prefix tails[0..len). For each input value x, binary search finds the first position whose tail is >= x, or position len if all active tails are smaller. The function writes x at that position and increments len only when extending the active prefix. It returns 0 for the empty input, preserves nums, and returns ownership of the entire workspace, still of length n. Workspace values outside the active prefix are not part of the result specification.

The algorithm takes O(n log n) time and uses O(n) caller-provided workspace, with constant additional runtime space. The C* version expresses the supplied for loop as an equivalent while loop and caches tails[mid] in a local variable. It performs no arithmetic on input values. The active tail values need not themselves form a subsequence of nums: for [3, 5, 6, 2, 4], the final active tails are [2, 4, 6], while an actual longest subsequence is [3, 5, 6].

The fixed header uses the same subsequence model as the quadratic LIS problem:

• ValidIncreasingSubsequence(l, limit, idxs) requires indices in [0, limit), strictly increasing indices, and strictly increasing selected values. PAIRWISE expresses the relation for every earlier/later pair. The empty subsequence is allowed.
• LISLengthPrefix(l, limit, ans) requires a valid subsequence of length ans and requires every valid subsequence to have length at most ans.
• LISLength(l, ans) uses the entire input list as the prefix.

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.

The implementation and contract are fixed. Add loop invariants and proof code only inside starter.c; changing the implementation or specification is rejected by the judge and consumes an attempt. Keep the supplied header and contract annotations. Submit the completed starter.c; no main function or standard input/output handling is needed.

中文

给定长度为 n 的整数数组 nums，请证明给定函数 length_of_lis_binary_search(nums, n, tails) 返回最长严格递增子序列的长度。子序列保留原数组中的下标顺序，但元素不必连续；相等的值不能延长严格递增子序列。

输入满足以下约束：

• 0 <= n <= 100000，nums 的长度恰好为 n。
• 元素可以是任意有符号 32 位整数，包括 -2147483648 和 2147483647，不附加更小的元素值范围限制。
• 调用者提供长度恰好为 n 的可写整数数组 tails。其初始整数值任意，由幽灵列表 tails_l 记录。
• 两个数组占用的内存不重叠，契约中的分离所有权表达了这一要求。n = 0 时，两个指针均可以为空指针，函数不会访问任何数组元素。

实现维护有效前缀 tails[0..len)。对于每个输入值 x，二分查找定位第一个尾值 >= x 的位置；若所有有效尾值均小于 x，则定位到 len。将 x 写入该位置，只有扩展有效前缀时才增加 len。空输入返回 0，函数保持 nums 不变，并保留整个长度为 n 的工作数组所有权。有效前缀以外的工作区内容不属于结果规约的一部分。

算法时间复杂度为 O(n log n)，使用调用者提供的 O(n) 工作区，其余运行时额外空间为常数。C* 版本将给定 for 循环改写为等价的 while 循环，并使用局部变量缓存 tails[mid]。算法不对输入值做算术运算。有效尾值本身未必构成 nums 的子序列：输入 [3, 5, 6, 2, 4] 的最终有效尾值为 [2, 4, 6]，而一个实际的最长子序列为 [3, 5, 6]。

头文件沿用二次复杂度 LIS 题目的子序列模型：

• ValidIncreasingSubsequence(l, limit, idxs) 要求所有下标位于 [0, limit)，下标严格递增，选中元素的值也严格递增。PAIRWISE 表示每一对先后元素均满足对应关系。允许空子序列。
• LISLengthPrefix(l, limit, ans) 要求存在长度为 ans 的合法子序列，且每个合法子序列的长度均不超过 ans。
• LISLength(l, ans) 将前缀范围设为整个输入列表。

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

实现和契约均为固定内容。你只能在 starter.c 中添加循环不变式和证明代码；修改实现或规约将被判定为失败，并消耗一次提交机会。请保留给定头文件以及契约标注。提交完成后的 starter.c 即可，不需要编写 main 函数或标准输入输出代码。

Examples / 示例