Заменить элемент в списке Coq
Я пишу код Coq, который должен изменять списки, в частности, путем доступа к индексу i, применения функции к этому элементу и замены его обратно. Я знаю, что могу получить доступ к элементу списка, используя nth, как определено в Coq.Lists.List. Затем я мог бы применить функцию к этому элементу, но как лучше всего вставить элемент обратно в исходный список с помощью библиотеки 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).
Итак, учитывая функцию, которую я хочу применить f : bool -> bool, я мог бы сделать f(v[i]), но я не уверен, как заменить ее обратно.
Ответы 2
Coq использует парадигму функционального программирования, поэтому вы не можете «заменять» элемент, как в императивном языке программирования. Но вы можете создать новый список, в котором элемент в позиции i будет f (v[i]) вместо (старого) v[i], а все остальные элементы будут такими же, как и в исходном списке.
Обратите внимание, что библиотека mathcomp seq.v уже предоставляет set_nth функцию, которая делает именно это.
Если вы хотите применить одну и ту же функцию к каждому элементу списка,
вы можете использовать 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.