Сжатие списка переписывания в Coq - PullRequest
Новая
       11

Сжатие списка переписывания в Coq

2 голосов
/ 15 июня 2019

У меня есть следующая функция Haskell, которая выводит все возможные способы разделения списка: 

split :: [a] -> [([a], [a])]
split []     = [([], [])]
split (c:cs) = ([], c : cs) : [(c : s1, s2) | (s1, s2) <- split cs]

Некоторые примеры ввода: 

*Main> split [1]
[([],[1]),([1],[])]
*Main> split [1,2]
[([],[1,2]),([1],[2]),([1,2],[])]
*Main> split [1,2,3]
[([],[1,2,3]),([1],[2,3]),([1,2],[3]),([1,2,3],[])]

Я пытаюсь написать ту же функциюв Coq, учитывая, что по умолчанию нет сопоставления с образцом, и я не хочу определять нотацию для него , поэтому я решил вместо этого написать рекурсивную функцию: 

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint split {X : Type} (l : list X) : list (list X * list X) :=
  match l with
    | [] => [([], [])]
    | c::cs =>
      let fix split' c cs :=
          match cs with
            | [] => []
            | s1::s2 => (c++[s1], s2) :: split' (c++[s1]) s2
          end
      in
      ([], c :: cs) :: ([c], cs) :: split' [c] cs
  end.

который дает те же результаты: 

     = [([], [1]); ([1], [])]
     : list (list nat * list nat)
     = [([], [1; 2]); ([1], [2]); ([1; 2], [])]
     : list (list nat * list nat)
     = [([], [1; 2; 3]); ([1], [2; 3]); ([1; 2], [3]); ([1; 2; 3], [])]
     : list (list nat * list nat)

Однако это слишком многословно, есть какие-либо намеки на то, как преобразовать это в более читаемую функцию, используя HOFs в Coq?

1 Ответ

5 голосов
/ 15 июня 2019

понимание в версии на Haskell является синтаксическим сахаром для map (или, в более общем случае, flat_map). 

Fixpoint split {X : Type} (l : list X) : list (list X * list X) :=
  match l with
  | [] => [([], [])]
  | c::cs =>
      ([], c :: cs) :: map (fun '(s1, s2) => (c :: s1, s2)) (split cs)
  end.
...