Coq let子句中的多个分配

Question

我是Coq的新手，只是想弄清楚基本语法。如何添加多个子句let？这是我要编写的函数：

Definition split {A:Set} (lst:list A) :=
  let
    fst := take (length lst / 2) lst
    snd := drop (length lst / 2) lst
  in (fst, snd) end.

这是错误：

语法错误：在[constr：operconstr级别200]之后（在[constr：binder_constr]中）应为'in'。

我猜想它in的定义是fst？

Answer 1

确实，您需要in在第一个标识符之后。根据参考手册（第1.2.12节）：

let ident := term1 in term2表示的本地绑定term1到变量ident在term2。

您需要多个（嵌套）let ... in表达式：

Definition split {A:Set} (lst:list A) :=
  let fst := take (length lst / 2) lst in
  let snd := drop (length lst / 2) lst in
    (fst, snd).

顺便说一句，您可以使用标准库（模块）中的firstn和skipn函数来代替和：Listtakedrop

Require Import Coq.Lists.List.
Import ListNotations.
Compute firstn 3 [1;2;3;4;5].    (* Result: [1;2;3] *)
Compute skipn 3 [1;2;3;4;5].     (* Result: [4;5]   *)

这（和一点重构）导致以下定义split（我将其重命名以避免split标准函数的出现）：

Definition split_in_half {A:Set} (lst:list A) :=
  let l2 := Nat.div2 (length lst) in
    (firstn l2 lst, skipn l2 lst).

Compute split_in_half [1;2;3;4;5].    (* Result: ([1; 2], [3; 4; 5])  *)

顺便说一句，如果您担心输入列表中的多次传递，它仍然有很大的改进空间。如果您打算进行提取（例如，提取到OCaml中），则可能是这样。