以交互方式生成的证据：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模式中处理implicits的方式似乎存在问题。

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)