sara lee (Nov 06 2021 at 16:00): 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 filterthat keeps elements that verifies some given property.
Require Import List PeanoNat.
Compute filter (fun x => negb (x =? 0)) (0 :: 1 :: 0 :: 2 :: nil).
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: Apr 19 2024 at 04:02 UTC