## Stream: Coq users

### Topic: list free of zeros

#### sara lee (Nov 06 2021 at 16:00):

I have two different functions whose input argument is natural number list. Before providing the list I want to remove all zeros from it .How I can do it? remove_all function from library may be use for this purpose? Output list of remove_all (lets call it l_f_0) when use by both functions it means it has no zero?

#### Laurent Théry (Nov 06 2021 at 21:08):

a solution is to use `filter`that keeps elements that verifies some given property.

``````Require Import List PeanoNat.

Compute filter (fun x => negb (x =? 0)) (0 :: 1 :: 0 :: 2 :: nil).
``````

#### sara lee (Nov 07 2021 at 17:24):

I want to ask if I remove zeros by creating a non-zero list, then use the output list of this function in Coq script. It means list is free of zero? Instead of l I use (remove_zero l) ?

#### Laurent Théry (Nov 07 2021 at 22:06):

Yes, if you want to call `f ` on `l` without the zeros in `l` you can write `(f (remove Nat.eq_dec 0 l)).`

``````Require Import List PeanoNat.

Definition l := 0 :: 1 :: 0 :: 2 :: nil.
Definition f (l : list nat) := rev l.

Check f (remove Nat.eq_dec 0 l).
Compute f (remove Nat.eq_dec 0 l).
``````
``````
``````

Last updated: Jan 29 2023 at 06:02 UTC