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

Using Coq
1

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. :slight_smile:

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 :frowning: so it was lost and this time I have no success).
If anyone has any hints, I will be very grateful.

2

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
3

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

4

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
5

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.
Proof. Admitted.

Theorem T2 n x x0 x1 (H: is_perm n x) (H0: is_perm n x0) (H1: is_perm n x1):
  map (fun i : nat => nth i (map (fun i0 : nat => nth i0 x 0) x0) 0) x1 =
  map (fun i : nat => nth (nth i x0 0) x 0) x1.
Proof. Admitted.

T1 corresponds to multiplication of inverse permutation with original permutation (which gives identity permutation), and T2 corresponds to associativity of permutation multiplication.
[Edit:] I have proven T1 now.

I believe that in this case direct approach is impossible (for T2 and for me) and it is necessary to prove correspondence with differently defined notion of permutation, prove its properties and transfer back to this definition. That is, permutations as bijections.
[Edit:] I have proven T2 too, even if it feels like a bit of black magic. :slight_smile: