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?

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: Oct 04 2023 at 22:01 UTC