英文:
Replace element in Coq list
问题
I am writing Coq code that needs to modify lists, particularly by accessing an index i, applying a function to that element, and replacing it back. I know I can access the element of a list by using nth as defined in Coq.Lists.List. Then, I could apply the function to this element, but what would be the best way to insert the element back into the original list using the Coq.Lists.List library?
I currently have the following code:
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).
So given the function that I want to apply f : bool -> bool, I could do f(v[i]), but I'm not sure how to replace it back.
英文:
I am writing Coq code that needs to modify lists, particularly by accessing an index i, applying a function to that element, and replacing it back. I know I can acces the elemenent of a list by using nth as defined in Coq.Lists.List. Then, I could apply the function to this element, but what would be the best way to insert the element back into the original list using the Coq.Lists.List library?
I currently have the following code:
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).
So given the function that I want to apply f : bool -> bool, I could do f(v[i]), but I'm not sure how to replace it back.
答案1
得分: 2
Sure, here's the translated text:
如果您想对列表的每个元素应用相同的函数，可以使用 map。相反，如果您只想替换列表中的一个单独元素，您可能需要编写自己的替换函数。例如：
Require Import List.
Import ListNotations.
Fixpoint replace {A : Type} (l : list A) (i : nat) (v : A) :=
match l with
| [] => []
| a :: l1 => match i with
| 0 => v :: l1
| S i1 => a :: replace l1 i1 v
end
end.
Compute replace [true; false; true] 2 false.
英文:
If you want to apply the same function to every element of a list,
you can use map. Instead, if you want to only replace one
single element of a list, you may need to write your own replace function. For example:
Require Import List.
Import ListNotations.
Fixpoint replace {A : Type} (l : list A) (i : nat) (v : A) :=
match l with
| [] => []
| a :: l1 => match i with
| 0 => v :: l1
| S i1 => a :: replace l1 i1 v
end
end.
Compute replace [true; false; true] 2 false.
答案2
得分: 1
Coq使用函数式编程范式，所以你不能像在命令式编程语言中那样“替换”一个元素。但你可以创建一个新列表，其中位置i的元素为f(v[i])，而不是（旧的）v[i]，其他元素与原始列表相同。
请注意，mathcomp的seq.v库已经提供了一个set_nth函数，可以做到这一点。
英文:
Coq uses a functional programming paradigm, so you cannot "replace" an element as you would in an imperative programming language. But you can create a new list with the element at position i being f (v[i]) instead of the (old) v[i], all the other elements being the same as in the original list.
Note that the mathcomp seq.v library already provides a set_nth function that does exactly that.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论