# Idea to add "index" function to Standard Library (or maybe not)

I defined it in such way:

``````Definition eq_dec A := forall (x y: A), { x = y } + { x <> y }.

Definition index_error A (dec: eq_dec A) (x: A) (L: list A): option nat.
Proof.
induction L.
+ exact None.
+ destruct (dec x a).
- exact (Some 0).
- exact (match IHL with Some n => Some (S n) | None => None end).
Defined.

Definition index A (dec: eq_dec A) (default: nat) (x: A) (L: list A): nat :=
match (index_error dec x L) with
| Some n => n
| None => default
end.
``````

Why do I think it would be nice to have? It is kind of inverse function of â€śnthâ€ť and seems useful for me anyway.
So, Iâ€™m collecting interesting/useful lemmas to prove about it. If you have any suggestions, feel free to post them.

Also, Iâ€™m trying to prove that

`````` Theorem index_of_list_elements A (dec: eq_dec A) (d: nat) (L: list A) (H: NoDup L): map (fun i => index dec d i L) L = seq 0 (length L).
``````

I know itâ€™s possible, because I have done it once already (but then the .v file become gibberish a day later - maybe electricity was lost in a bad moment or smth - and I hadnâ€™t saved it with version control software so it was lost and this time I have no success).
If anyone has any hints, I will be very grateful.

Hello,

I would attack the problem as follows:

1. For any list `L : list A` and any `f : A -> B`, show that

``````map f L = map (fun n => f (nth n L d)) (seq 0 (length L))
``````
2. For any `L : list A` and any `f g : A -> B`, show that

``````(forall x, In x L -> f x = g x) -> map f L = map g L.
``````
3. Let `f i = index dec d i L`. Then prove that `f (nth n L d) = n` for `n < length L` (use `H : NoDup L`) and deduce from (1) and (2) that

``````map f L = map id (seq 0 L) = seq 0 L.
``````

Cheers,
NicolĂˇs

3 Likes

Note that @nojb point 1 here moves us back to @nojb point 2 there.

Concerning the original question about `index`, it looks indeed natural in a context of lists on types with decidable equality.
As first key statements, I would start with your argument of being an inverse for `nth`: `index (nth ...) = ...` and `nth (index ...) = ...`.
By the way, I would recommend to keep consistency with respect to `nth` on the order of arguments by putting the default element as the last one for `index`.
A possibly interesting and related function would collect the list of indices:

``````Fixpoint indices A (dec: eq_dec A) x l :=
match l with
| nil => nil
| y :: tl => if dec x y then 0 :: map S (indices A dec x tl)
else map S (indices A dec x tl)
end.
``````
1 Like

I proved both

``````Theorem index_nth_id A (dec: eq_dec A) (L: list A) d d' (H: NoDup L) n (H0: n < length L): index dec (nth n L d') L d = n.
``````

and

``````Theorem nth_index_id A (dec: eq_dec A) (L: list A) d d' x (H: In x L): nth (index dec x L d) L d' = x.
``````

And few other theorems at https://github.com/LessnessRandomness/Linear-Algebra/blob/master/index_facts.v

In case if someone wants to have fun, there are two other (unproven, but tested to be true) theorems:

``````Definition is_perm n L := Permutation L (seq 0 n).

Theorem T1 n x (H: is_perm n x):
map (fun i => nth i (map (fun i0 => index Nat.eq_dec i0 x 0) (seq 0 n)) 0) x = seq 0 n.