如何在 Coq 中定义 arg max

Question

我是 Coq 新手。我对定义递归函数感兴趣

c(k)

。基本情况

c(0)

是常数 0。给定

c(k)

，有

a(k+1, i) = g(i, c(k))

，其中

g

是一个函数，以及

c(k+1) = a(k+1, j)

，其中

j = arg max h(a(k+1, i))

在所有

0 <= i <= T

上，

h

是另一个函数，并且

T

是

i

的上限。

c(k)

和

a(k)

都是自然数。索引是自然数。我一直在定义

arg max

运算符。

这是我的草图：

(* The upper bound of i *)
Parameter T : nat.
Parameter g : nat -> nat -> nat.
Parameter h : nat -> nat.

Fixpoint c (k : nat) : nat :=
  match k with
  | 0 => 0
  | S k' => a k j  (* ?? *)
  with
Fixpoint a (k i : nat) : nat :=
  match k with
  | 0 => 0
  | S k' => g i (c k')
  end.

我向 GPT 询问了这个问题，它建议我首先找到

h(a(k+1, i))

超过

i

的最大值，然后搜索产生该最大值的特定

i

。显然这不起作用，因为搜索产生了 nat 选项，但我知道

arg max

不是一个选项。

非常感谢！

Answer 1

ChatGPT 在这里并不遥远。 搜索会返回

option nat

，因为您可能正在搜索不存在的值。 但您知道该值存在，因此您知道搜索将始终返回

Some x

形式的值。 根据这些知识，您可以通过以下形式的函数运行搜索结果来安全地摆脱异常情况。

Definition discard_option (x : option nat) : nat :=
  match x with Some x => x | _ => 0 end.

在证明代码的属性时，您必须证明

find

（可用于搜索正确值的函数）当然永远不会返回

None

。