Stream: Coq users

Topic: Ideas on how to create custom list map


view this post on Zulip walker (Apr 24 2023 at 14:42):

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 ?

view this post on Zulip Laurent Théry (Apr 24 2023 at 15:17):

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.

view this post on Zulip Meven Lennon-Bertrand (Apr 24 2023 at 16:46):

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

view this post on Zulip walker (Apr 24 2023 at 18:18):

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

view this post on Zulip walker (Apr 24 2023 at 18:22):

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.

view this post on Zulip walker (Apr 24 2023 at 18:23):

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