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 level 200] 之后应为“in”（在 [constr:binder_constr] 中）。

我想它在fst 的定义之后需要一个in？

Answer 1

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

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

您需要多个（嵌套的）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).

---

顺便说一句，您可以使用标准库 (List module) 中的 firstn 和 skipn 函数来代替 take 和 drop：

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。