如何在 Coq 中创建子列表？

Question

我正在 Coq 中工作，并试图弄清楚如何做下一步：如果我有一个自然数列表和一个给定的 number n，我想在每个 之前和之后打破我的列表n。为了更清楚地说明，如果我有列表[1; 2; 0; 3; 4; 0; 9]和数字n = 0，那么我希望输出三个列表：[1;2]、[3;4]和[9]。我遇到的主要问题是我不知道如何在Fixpoint. 我想我需要嵌套Fixpoints 但我只是不知道如何做。作为一个非常原始的想法，我有太多问题：

Fixpoint SubLists (A : list nat)(m : nat) :=
 match A with
 |[] => []
 |n::A0 => if n =? m then (SubLists L) else n :: (SubLists L)
end.

我非常感谢您对如何执行此操作以及如何导航具有多个元素的输出的意见。

Answer 1

您可以通过组合几个固定点来做到这一点：

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint prefix n l :=
  match l with
  | [] => []
  | m :: l' => if beq_nat n m then []
               else m :: prefix n l'
  end.

Fixpoint suffix n l :=
  match l with
  | [] => l
  | m :: l' => if beq_nat n m then l'
               else suffix n l'
  end.

Fixpoint split_at n l :=
  match l with
  | [] => []
  | m :: l' => prefix n (m :: l') :: split_at n (suffix n (m :: l'))
  end.

请注意，Coq 的终止检查器接受对 的递归调用split_at，即使它在语法上不是 的子术语l。原因是它能够检测到该后缀仅输出其参数的子项。但为了让它起作用，我们必须返回l, 而不是[]它的第一个分支（尝试更改它看看会发生什么！）。