Несколько заданий в разделе 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]).

Я полагаю, что ожидает in после определения fst?

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

---

Кстати, вы можете использовать firstn и skipn функции от стандарта библиотека (List module) вместо 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.