Longest Increasing Subsequence / 最长严格递增子序列

English

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

The input satisfies the following constraints:

• 1 <= n <= 100000, and nums has exactly n elements.
• For every 0 <= i < n, -10000 <= nums[i] <= 10000.
• The caller provides a writable dp workspace of exactly n integers. Its initial contents are unspecified and need not be initialized.
• The two arrays occupy disjoint memory, as expressed by separating ownership in the contract.

The implementation uses O(n^2) dynamic programming. It initializes dp[i] to 1, then scans every earlier index j. When nums[j] < nums[i], it takes the larger of dp[i] and dp[j] + 1. Thus each completed dp[i] describes the longest strictly increasing subsequence ending at index i. The function returns the largest completed value, leaves nums unchanged, and initializes all n workspace entries. It uses O(n) caller-provided workspace and constant additional runtime space. The C* version uses equivalent while loops and local variables that cache individual array reads. The full bound of 100000 is part of the specification even though this quadratic version can be slow on large inputs.

The fixed header defines the result through subsequences:

• 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.
• LISPrefix(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 list as the prefix.

The contract records nums as the ghost list input. Its postcondition requires LISLength(input, result), 1 <= result <= n, ownership of the unchanged input, and ownership of a fully initialized workspace of length n. It does not require the caller to provide initial workspace values. lis_undef(dp, i, n) owns the uninitialized suffix [i, n).

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_dp(nums, n, dp) 返回最长严格递增子序列的长度。子序列保留原数组中的下标顺序，但元素不必连续；相等的值不能延长严格递增子序列。

输入满足以下约束：

• 1 <= n <= 100000，nums 的长度恰好为 n。
• 对所有 0 <= i < n，有 -10000 <= nums[i] <= 10000。
• 调用者提供长度恰好为 n 的可写整数工作数组 dp，其初始内容任意，无须预先初始化。
• 两个数组占用的内存不重叠，契约中的分离所有权表达了这一要求。

给定实现采用 O(n^2) 动态规划。先将 dp[i] 初始化为 1，再扫描所有先前下标 j。当 nums[j] < nums[i] 时，用 dp[i] 与 dp[j] + 1 的较大值更新 dp[i]。因此，每个已完成的 dp[i] 表示以位置 i 结尾的最长严格递增子序列长度。函数返回所有已完成值中的最大值，保持 nums 不变，并初始化全部 n 个工作区元素。算法使用调用者提供的 O(n) 工作区，其余运行时额外空间为常数。C* 版本将 for 循环改写为等价的 while 循环，并使用局部变量缓存单次数组读取。规约仍保留 100000 的完整上界；该二次复杂度版本在大输入上可能运行较慢。

给定头文件通过子序列定义结果：

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

契约使用幽灵列表 input 记录 nums 的内容。后置条件要求 LISLength(input, result)、1 <= result <= n，保留未改变的输入数组所有权，并得到长度为 n、已完全初始化的工作数组所有权。调用者无须提供工作区初值。请在 starter.c 中自行定义不变式所需的辅助谓词并证明所需引理；头文件仅提供规约模型及其依赖定义。 lis_undef(dp, i, n) 表示未初始化后缀 [i, n) 的内存所有权。

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

Examples / 示例