如何在Coq中定义arg max以实现递归函数c(k)

核心思路 #

你需要的argmax无需返回option类型，因为取值范围0≤i≤T是非空的（T是自然数，至少包含i=0），因此可以直接构造返回nat的argmax实现，无需处理空集情况。

分步实现 #

1. 定义argmax辅助函数 #

先实现一个遍历0到T的辅助函数，维护当前h值最大的索引（若有多个最大值，默认保留第一个遇到的；若需取最后一个，可调整比较逻辑）：

(* 辅助函数：遍历候选索引，返回最优索引
   参数说明：
   - current_i: 当前遍历到的索引
   - current_best_i: 目前h值最大的索引
   - current_max_h: 目前最大的h值
   - ck': c(k')的值，用于计算a(k+1,i) = g(i, ck')
*)
Fixpoint argmax_aux (current_i current_best_i : nat) (current_max_h : nat) (ck' : nat) : nat :=
  match current_i with
  | S T => current_best_i  (* 遍历完所有i（0到T），返回最优索引 *)
  | _ => let current_a := g current_i ck' in
         let current_h := h current_a in
         if current_h > current_max_h then
           argmax_aux (S current_i) current_i current_h ck'
         else
           argmax_aux (S current_i) current_best_i current_max_h ck'
  end.

2. 封装argmax入口函数 #

初始化遍历过程，从i=0开始，初始最优索引为0，初始最大h值为h(g 0 ck')：

(* 计算0≤i≤T范围内h(g(i, ck'))的argmax，返回nat类型 *)
Definition argmax_over_range (ck' : nat) : nat :=
  let initial_a := g 0 ck' in
  argmax_aux 0 0 (h initial_a) ck'.

3. 修正递归函数定义 #

原代码中a(k,i)的递归可以简化，且c和a属于互递归，需要用Coq的互递归定义机制（如Function命令，需导入FunInd库）：

Require Import FunInd.

Parameter T : nat.
Parameter g : nat -> nat -> nat.
Parameter h : nat -> nat.

(* 互递归定义c和a *)
Function c (k : nat) : nat :=
  match k with
  | 0 => 0
  | S k' => let j := argmax_over_range (c k') in
            g j (c k')  (* 直接用g(j, c(k'))替代a(S k', j)，等价且更简洁 *)
  end
with a (k i : nat) : nat :=
  match k with
  | 0 => 0
  | S k' => g i (c k')
  end.
Proof.
  (* 证明递归终止：每次递归调用的k值严格递减 *)
  intros. apply lt_wf.
Qed.

4. 调整多最大值的处理逻辑 #

如果需要在多个i取到相同h最大值时选择最大的索引，只需修改argmax_aux中的比较条件：
将if current_h > current_max_h改为if current_h >= current_max_h即可。

关键注意点 #

• 避免option类型：因为范围0≤i≤T非空，argmax必然存在，直接返回nat是安全的。
• 互递归合法性：用Function命令配合终止性证明，解决Coq对互递归函数的守卫检查问题。

内容的提问来源于stack exchange，提问作者Kaiwen