与 :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 ..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 有点要求我们在 (a : Type) 上做 intro，但是在编译模块时类型变量是隐式的，我们不必引入它。

这里的解决方法是删除有问题的 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)

与 :elab 交互生成的证明不起作用

Proof generated interactively with :elab doesn't work

theorem-proving

idris

elaboration