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 和 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。

Coq let 子句中的多项赋值

Multiple assignments in a Coq let clause

syntax-error

coq

let