Multiple assignments in a Coq let clause

coq, let, syntax-error

Solution

Indeed, you need `in` after the first identifier. According to the reference manual (§1.2.12):

`let ident := term1 in term2` denotes the local binding of `term1` to the variable `ident` in `term2`.

You need multiple (nested) `let ... in` expressions:

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).

By the way, you can use the `firstn` and `skipn` functions from the standard library (`List` module) instead of `take` and `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]   *)

This (and a little bit of refactoring) results in the following definition of `split` (I renamed it to avoid shadowing of the `split` standard function):

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])  *)

Incidentally, it still leaves plenty of room for improvement, if you are concerned about multiple passes over the input list. Which you could be, if you're planning to do extraction, e.g. into OCaml.

Problem

I'm brand new to Coq and just trying to figure out the basic syntax. How can I add multiple clauses to `let`? Here's the function I'm trying to write: ``` Definition split {A:Set} (lst:list A) := let fst := take (length lst / 2) lst snd := drop (length lst / 2) lst in (fst, snd) end. ``` and here is the error: Syntax error: 'in' expected after [constr:operconstr level 200] (in [constr:binder_constr]). I suppose it expects a `in` after the definition of `fst`?

Original source