To create a slicing function that has the lower and upper index and the size of the list as parameters so that when slicing the list given those parameters, it behaves like a gather function.
I've tried to define it using the filter concept and provide it with the testing function. Please see my code below
Require Import PeanoNat.
Require Import Coq.Init.Datatypes.
Require Import Notations.
Import Basics.
Fixpoint filter_index {X: Type} (currInd : nat) (test: nat -> bool) (l: list X ): list X :=
match l with
| [] => []
| h::t => if test currInd then h :: filter_index (S currInd) test t else filter_index (S currInd) test t
end.
Definition slicing_ring (tail head sz: nat) : nat -> bool :=
fun n => if sz <=? head then orb ( n <=? head mod sz) ( tail <=? n) else andb ( tail <=? n) (n <=? head).
Example test1 : filter_index 0 (slicing_ring 3 5 4) [6;9;3;4] = [4;6;9].
So in the above example, I expect to have the result list. However, if I do Compute filter_index 0 (slicing_ring 2 3 4) [6;9;3;4]. it gave me [6;9;4].
Your filter_index function is never going to change the order of the elements of the list. The elements are tested in order and then conditionally inserted into the output in order.
A better approach might be based on indexed access.
Fixpoint get_index {X: Type} (ls: list X) (index: nat): option X :=
match ls, index with
| [], _ => None
| x :: _, 0 => Some x
| x :: tl, S index' => get_index tl index'
end.
(this is essentially nth_error from the standard library — there are variants for other kinds of access).
If you can enumerate the indices for your ring buffer slice in the desired order, this should work fine.