Свернуть и доказательства - PullRequest
Новая
       46

Свернуть и доказательства

2 голосов
/ 23 апреля 2019

Я часто использую тип данных Vect в своем коде. Часто мне приходится доказывать что-то, связанное с библиотечными функциями, а не Vects, которые используют foldr. Так как foldr реализован поверх foldrImpl, если я попытаюсь осмотреть контекст доказательства, вставив дыру, то, что проявляется в цели. Моя проблема в том, что, похоже, idris не может оценить foldrImpl в типе цели (поведение, аналогичное тому, когда функция проверки целостности неизвестна), что заставляет меня застрять в доказательствах.

Обычно мое решение этой проблемы - определить собственную версию библиотечной функции, которая выполняет свертывание с нуля. Но это явно неудобно, поскольку: (i) мне приходится кодировать функции, которые уже существуют в библиотеке; (ii) это заставляет меня не использовать сгиб в любых определениях, о которых я собираюсь позже доказать.

Для конкретного примера рассмотрим, что я хочу доказать следующее 

lemma_take_head : {x : a} -> 
                  {xs : List a} -> 
                  {ls : Vect len (List a)} ->  
                   concat ((x :: xs) :: ls) = x :: (concat (xs :: ls))
lemma_take_head {ls = []} = Refl
lemma_take_head {ls = l :: ls} = ?h2

С моей версией concat это так же просто, как просто вернуть Refl. Но с библиотечной версией, которая сворачивается, мы получаем следующий контекст для случая, когда Vect является главным недостатком: 

  a : Type
  l : List a
  x : a
  xs : List a
  len : Nat
  ls : Vect len (List a)
--------------------------------------
h2 : foldrImpl (\meth, meth => meth ++ meth) [] (\x1 => x :: xs ++ l ++ x1) ls = x :: foldrImpl (\meth, meth => meth ++ meth) [] (\x1 => xs ++ l ++ x1) ls

Есть ли способ продолжить доказательства после того, как они достигнут такой точки, или это единственное решение для повторной реализации функций таким образом, чтобы они не использовали сгибы?

...