#4. 二分搜索极小点证明

题目描述

我们考虑一个自然数的数组，满足数组中任何两个相邻的元素不相等 (neighbor_nonequal)。

一个索引是数组中的极小点，如果这个索引上的值小于两边的值（如果这个索引在边界上，则对应边的条件自动满足）。is_local_min 定义索引 $i$ 是数组 $xs$ 的极小点。

可以证明总是存在一个极小点。实际上，二分搜索方法 local_min 可以保证返回一个极小点。

证明步骤

1. 扩展定义

首先，将 is_local_min 的定义扩展到区间的情况 is_local_min_part。

2. local_min_correct_induct (160 分)

函数 local_min 的归纳性质如下：假设 $a$ 和 $b$ 分别小于左侧/右侧的值，则 local_min xs a b 返回一个满足 is_local_min_part 条件的索引。

该证明首先根据 local_min 的定义做归纳，对 local_min 的几种情况分类讨论。

theorem local_min_correct_induct (xs : List Nat) (a b i : Nat) :
    neighbor_nonequal xs → 0 ≤ a → a ≤ b → b < xs.length →
    (a = 0 ∨ (a < xs.length ∧ (a - 1) < xs.length ∧ xs.getD a 0 < xs.getD (a - 1) 0)) →
    (b = xs.length - 1 ∨ (b < xs.length ∧ (b + 1) < xs.length ∧ xs.getD b 0 < xs.getD (b + 1) 0)) →
    local_min xs a b i → is_local_min_part xs a b i

3. local_min_correct (40 分)

使用 local_min_correct_induct 验证正确性结论：

theorem local_min_correct (xs : List Nat) (i : Nat) :
    neighbor_nonequal xs → xs.length > 0 →
    local_min xs 0 (xs.length - 1) i → is_local_min xs i

分值

• local_min_correct_induct: 160 分
• local_min_correct: 40 分

总计: 200 分