Multiple assignments in a Coq let clause

Question

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?

Anton Trunov Anton Trunov · Accepted Answer · 2016-10-26T07:35:11

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.

Multiple assignments in a Coq let clause

1 Answers