Подтверждение генерируется в интерактивном режиме с помощью: elab не работает

Question

Я пытаюсь доказать следующее утверждение с помощью интерактивного помощника:

total
concatAssoc : (x : List a) -> (y : List a) -> (z : List a) -> (x ++ y) ++ z = x ++ (y ++ z)
concatAssoc = ?h

Я понимаю, как это можно доказать без размышлений разработчика:

concatAssoc [] _ _ = Refl
concatAssoc (_ :: x) y z = cong $ concatAssoc x y z

Однако мне просто любопытно, почему у меня возникает проблема с интерактивным доказательством этого утверждения в REPL. Вот что я сделал:

:elab h
x <- gensym "x"
_base <- gensym "_base"
intro'
intro x
repeatUntilFail intro'
induction (Var x)
search
compute
attack
intro'
intro'
intro _base
rewriteWith (Var _base)
reflexivity
solve
:qed

Вот что я получил:

...
-Main.h> solve
h: No more goals.
-Main.h> :qed
Proof completed!
Main.h = %runElab (do x <- gensym "x"
                      _base <- gensym "_base"
                      intro'
                      intro x
                      repeatUntilFail intro'
                      induction (Var x)
                      search
                      compute
                      attack
                      intro'
                      intro'
                      intro _base
                      rewriteWith (Var _base)
                      reflexivity
                      solve)

После этого я заменил тело функции следующим доказательством:

import Pruviloj.Core
import Pruviloj.Induction
import Language.Reflection.Elab

total
concatAssoc : (x : List a) -> (y : List a) -> (z : List a) -> (x ++ y) ++ z = x ++ (y ++ z)
concatAssoc = %runElab (do x <- gensym "x"
                           _base <- gensym "_base"
                           intro'
                           intro x
                           repeatUntilFail intro'
                           induction (Var x)
                           search
                           compute
                           attack
                           intro'
                           intro'
                           intro _base
                           rewriteWith (Var _base)
                           reflexivity
                           solve)

Однако, когда я попытался скомпилировать его, я получил следующую ошибку:

>idris 1.idr -p contrib -p pruviloj -X ElabReflection
Type checking .\1.idr
1.idr:9:16-23:34:
  |
9 | concatAssoc =  %runElab (do x <- gensym "x"
  |                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of concatAssoc with expected type
        (x : List a) -> (y : List a) -> (z : List a) -> (x ++ y) ++ z = x ++ y ++ z

Can't find a value of type
        (x ++ []) ++ z = x ++ z

Holes: Main.concatAssoc

Итак, мой вопрос: почему такое же доказательство работает в REPL, но не работает, если записано в файл?

Answer 1

Кажется, есть проблема с тем, как REPL обрабатывает последствия в режиме :elab.

Idris> :l ElabDoesNotWork.idr
Holes: Main.h
*ElabDoesNotWork> :elab h


----------                 Goal:                  ----------
{hole_0} : (a : Type) -> (x : List a) -> (y : List a) -> (z : List a) -> (x ++ y) ++ z = x ++ y ++ z
-Main.h>

Здесь REPL вроде просит нас сделать intro на (a : Type), но при компиляции модуля переменная типа неявная, и нам не нужно ее вводить.

Обходной путь здесь заключается в удалении оскорбительного intro:

import Pruviloj.Core
import Pruviloj.Induction

concatAssoc : (xs, ys, zs : List a) -> (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
concatAssoc = %runElab (do intro `{{xs}}
                           intro `{{ys}}
                           intro `{{zs}}
                           induction (Var `{{xs}})
                           compute
                           reflexivity
                           compute
                           attack
                           intro `{{x}}
                           intro `{{xs'}}
                           intro `{{IH}}
                           rewriteWith (Var `{{IH}})
                           reflexivity
                           solve)