## Stream: Coq users

### Topic: same output

#### pianke (May 14 2023 at 06:31):

I am finding index of a provided natural number in the list nat.Problem is that when list is empty then it gives 0 and when there is only one element in the list then it also gives 0 because index start from 0. How i can keep both cases different?

#### Pierre Castéran (May 14 2023 at 09:12):

You may use an `option` type:

``````Require Import List Arith.
Import ListNotations.

Fixpoint index_aux {A:Type}(A_eqdec :forall x y :A, {x=y}+{x<>y})
(a:A)(l:list A)(start:nat) : option nat :=
match l with
nil => None
| b::l' => if A_eqdec a b
then Some start
else index_aux A_eqdec a l' (S start)
end.

Definition index_opt {A:Type} A_eqdec (a:A) l :=  index_aux A_eqdec a l 0.
Compute index_opt Nat.eq_dec 3 [3].
Compute index_opt Nat.eq_dec 3 [].
Compute index_opt Nat.eq_dec 3 [1;2;3;4].
Compute index_opt Nat.eq_dec 33 [1;2;3;4].
``````

Another possibility is to consider that a list may contain several occurrences of the searched element.
In which case, you may define a function which returns a list of all the positions of this element in the list.
Then the result is not ambiguous anymore (since `[]` is different from `[0]`in your example).

Last updated: Jun 16 2024 at 01:42 UTC