CODEWITHSUNDEEP
computer-sciencecoqproof-general
epelaez
epelaez

Reputation: 162

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 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.

Upvotes: 0

Views: 319

Answers (2)

Lolo
Lolo

Reputation: 649

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.

Upvotes: 3

Pierre Jouvelot
Pierre Jouvelot

Reputation: 923

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.

Upvotes: 1

Related Questions