This is basically some creativity question I have this custom map function:

```
Section MapIndexRev.
Variable T U: Type.
Variable f: nat -> T -> U.
Fixpoint map_index_rev (s: seq T) : seq U :=
match s with
| [::] => [::]
| t::s' => let l := size s' in
(f l t)::map_index_rev s'
end.
End MapIndexRev.
```

The general intuition is that if I have list `a::b::c::d::e::[::]`

I want to to have a map that knows that `a`

has reverse index 4, `b`

has index `3`

... etc

The need for this function appeared during implementing stuff related to inductive families in debruijn notation.

There are two things I hate about this function:-

A- I have to calculate size ever time, the alternative is using subtraction, but I am afraid of having to deal with saturation (forall x, 0-x = 0)

B- I don't like the idea that I will have to prove many facts from scratch while it might be possible to deduce them from the properties of normal map with less effort.

So my question is how can I do better that this implementation ?

Trying to reuse existing functions, I get this

```
From mathcomp Require Import all_ssreflect.
Section MapIndexRev.
Variable T U: Type.
Variable f: nat -> T -> U.
Definition map_index_rev s :=
[seq f p.1 p.2 | p <- zip (rev (iota 0 (length s))) s].
End MapIndexRev.
```

Have you tried using the following `mapi`

function?

```
Require Import List.
Import ListNotations.
Fixpoint mapi {A B : Type} (f : nat -> A -> B) (i : nat) (l : list A) : list B :=
match l with
| [] => []
| h :: t => (f i h) :: (mapi f (S i) t)
end.
```

It is incrementing in the wrong direction compared to the one you want, and the following might be annoying to use because of the sutraction:

```
Definition map_index_rev {A B : Type} (f : nat -> A -> B) (l : list A) : list B :=
mapi (fun n => f (length l - n)) 0 l.
```

Such functions that take an extra natural number index to be incremented at each recursion step are heavily used in MetaCoq, exactly for handling de Bruijn stuff

well, it is funny because I need it for the exact same purpose, but I am always scared of subtraction.

also @Laurent Théry 's solution almost worked, but it failed because f itself is actually a very very complex recursive function with nested cases, in particular I had questions about this particular `f`

here https://coq.zulipchat.com/#narrow/stream/237659-Equations-devs-.26-users/topic/cannot.20guess.20decreasing.20argument/near/349406228

once I used this this `map_index_rev`

implementation, the other function `f`

became not happy and failed to identify decreasing argument.

I am **not** going to add more details at this point because I will just keep the old implementation which is recursive and maybe come back to it later when it becomes the main problem.

Last updated: Jun 16 2024 at 01:42 UTC