Coq中nat->nat类型命题相等性判断及列表索引查询方案

你遇到的核心矛盾是Coq中函数类型的外延相等性确实不存在通用可判定过程，所以直接用=比较无法写出可计算的递归实现，以下是三种常用的替代方案：

• 方案1：使用命题式谓词定义，不要求可计算
  如果你不需要这个索引函数可以直接执行计算，仅需要用它做逻辑推导，可以直接定义归纳谓词描述「f是列表l的第n个元素」的性质，示例实现：

  Inductive fn_index {A} (f : A) : list A -> nat -> Prop :=
  | fn_index_hd l : fn_index f (f :: l) 0
  | fn_index_tl g l n : fn_index f l n -> fn_index f (g :: l) (S n).
  

  该定义不需要判定相等性，使用时只需提供两个函数相等的证明即可完成逻辑推理。
• 方案2：传入对应场景下的函数相等判定器
  如果你确实需要可计算的索引查找逻辑，可以将目标函数子类的相等判定器作为入参传入。虽然通用的nat -> nat相等判定不存在，但如果你的列表中函数都是特定结构（比如有限定义域、固定阶多项式等），可以针对该子类实现专用判定：

  Fixpoint find_fn_index {A} (eq_dec : forall x y : A, {x = y} + {x <> y}) (l : list A) (f : A) : option nat :=
    match l with
    | [] => None
    | g :: l' => if eq_dec g f then Some 0 else option_map S (find_fn_index eq_dec l' f)
    end.
  

  比如针对所有「仅在小于k的自然数上有非零输出，其余输入都返回0」的函数，只需要验证两个函数在0到k-1上的输出完全一致即可判定相等。
• 方案3：用带可判定相等的结构化类型替代原生函数类型
  你可以将业务中用到的nat -> nat函数封装为语法归纳类型，直接比较语法结构相等：

  Inductive arith_expr : Type :=
  | Const : nat -> arith_expr
  | Var : arith_expr
  | Add : arith_expr -> arith_expr -> arith_expr
  | Mul : arith_expr -> arith_expr -> arith_expr.
  
  (* 实现解释器将结构化表达式转换为nat->nat函数 *)
  Fixpoint interp (e : arith_expr) : nat -> nat :=
    match e with
    | Const n => fun _ => n
    | Var => fun x => x
    | Add e1 e2 => fun x => interp e1 x + interp e2 x
    | Mul e1 e2 => fun x => interp e1 x * interp e2 x
    end.
  

  该场景下arith_expr的语法相等是可判定的，列表直接存储arith_expr类型即可实现常规的可计算索引查找。

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