syntax-error - 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.

这是错误:

Syntax error: 'in' expected after [constr:operconstr level 200] (in [constr:binder_constr]).

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

Answer 1

确实，您需要在第一个标识符之后in。根据引用手册(§1.2.12):

let ident := term1 in term2 denotes the local binding of term1 to the variable ident in 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).

<小时/>

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

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。