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: Oct 13 2024 at 01:02 UTC