如何使用Coq.Lists.List库替换列表指定索引的元素？

你可以通过递归定义一个更新函数，遍历列表时定位到目标索引，将该位置的元素应用函数后替换回去，其他位置保持不变。以下是具体实现：

在你已有的代码基础上，添加更新逻辑：

Definition bv (n : nat) := list bool. 
Definition get_bv {n : nat} (i : nat) (v : bv n) := nth i v false.
Notation "v [ i ]" := (get_bv i v) (at level 0).

(* 定义更新函数：对索引i处的元素应用函数f后替换回原列表 *)
Definition update_bv {n : nat} (i : nat) (f : bool -> bool) (v : bv n) : bv n :=
  let rec aux current_idx remaining :=
    match remaining with
    | [] => []  (* 索引超出列表长度时，不修改原列表 *)
    | head :: tail =>
        if current_idx =? i then  (* 匹配到目标索引，应用函数f *)
          f head :: aux (S current_idx) tail
        else  (* 未匹配到，保留原元素 *)
          head :: aux (S current_idx) tail
    end
  in aux 0 v.

(* 定义便捷符号，贴近数组修改的直观语法 *)
Notation "v [ i ] <- f" := (update_bv i f v) (at level 0).

函数说明 #

• aux 是辅助递归函数，current_idx 记录当前遍历的索引，remaining 是剩余未处理的列表部分。
• 遍历到目标索引 i 时，对当前元素应用函数 f 后加入新列表；其余位置直接保留原元素。
• 如果索引 i 超出列表长度，遍历到空列表后直接返回原列表结构，这和你定义的 get_bv 在索引超出时返回默认值的逻辑保持一致。

使用示例 #

你可以这样调用更新函数：

(* 示例：将索引1处的bool值取反 *)
Example test_update : [true; false; true] [1] <- negb = [true; true; true].
Proof. reflexivity. Qed.

(* 直接调用update_bv的写法 *)
Example test_update_direct : update_bv 2 negb [true; false; true] = [true; false; false].
Proof. reflexivity. Qed.

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