coq - 如何在 Coq 中创建子列表？

Question

我正在 Coq 中工作并试图弄清楚如何做下一件事:如果我有一个自然数列表和一个给定的数字 n ，我想在每个 n 之前和之后列出我的 list 。的。为了更清楚，如果我有列表 [1; 2; 0; 3; 4; 0; 9]和号码n = 0 ，然后我想输出三个列表:[1;2] , [3;4]和 [9] .我的主要问题是我不知道如何在 Fixpoint 上输出几个元素.我想我需要嵌套 Fixpoint s 但我只是不明白如何。作为一个有太多问题的非常原始的想法，我有:

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 ，而不是 []在它的第一个分支上(尝试更改它以查看会发生什么!)。