时间戳

首页 > 解决方案 > 对列表进行切片，就好像它具有环形缓冲区的行为一样

function - 对列表进行切片，就好像它具有环形缓冲区的行为一样

问题描述

创建一个切片函数，该函数将列表的上下索引和大小作为参数，以便在给定这些参数的情况下对列表进行切片时，它的行为就像一个收集函数。

我尝试使用过滤器概念定义它并为其提供测试功能。请在下面查看我的代码

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].

所以在上面的例子中，我希望有结果列表。但是，如果我这样做Compute filter_index 0 (slicing_ring 2 3 4) [6;9;3;4].，它给了我[6;9;4].

标签： functionfiltercoq

解决方案

您的filter_index函数永远不会更改列表元素的顺序。元素按顺序测试，然后有条件地按顺序插入到输出中。

更好的方法可能是基于索引访问。

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.

（这本质上nth_error来自标准库——有其他类型的访问的变体）。

如果您可以按所需顺序枚举环形缓冲区切片的索引，则应该可以正常工作。

推荐阅读