Stream: Coq users

Topic: list free of zeros

view this post on Zulip 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?

view this post on Zulip Laurent Théry (Nov 06 2021 at 21:08):

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

Require Import List PeanoNat.

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

view this post on Zulip 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) ?

view this post on Zulip 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