如何在 Idris 1.3.2 中使用归纳？

Question

我正在学习 Idris，特别是我想学习如何证明陈述。

当然，所有练习中最愚蠢的是自然数和的结合律，我对理论和我将使用的证明方式感到满意（对第一个参数的归纳和重写），但由于教程中使用的 Idris 版本和我的版本 (1.3.2) 之间可能不兼容，我被卡住了。

这是我的代码：

module SumAssoc

plusAssoc : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc Z c r = Refl
plusAssoc (S k) c r = rewrite plusAssoc k c r in Refl

-- ↑
-- this proof works well.
-- now for an inductive proof with tactics...

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' l c r = ?hole

当我尝试使用策略

证明它时

intros
induction l
...

我卡住了并收到以下错误消息：

Prover error:
  |
  | induction l
  | ^
unexpected "induction l":
expected tactic

当然，这与 :prove 环境现已弃用这一事实有关。但我不知道如何解决这个问题，因为我所有的尝试都失败了：

:elab hole好像也好不到哪里去（主要是我无处学习库的语法和逻辑）
使用 pruviloj 也会失败。

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' Z c r = Refl
plusAssoc' (S k) c r = ?hole_2

---------- Proofs ----------

SumAssoc.hole_2 = proof
  intros
  rewrite plusAssoc' k c r
  trivial

EDIT：这有效，但也已弃用。而且，可以理解，我想管理如何通过归纳法证明事物。

编辑 2： 我设法在 :elab hole 中继续使用这一系列命令：

plusAssoc'' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc'' l c r = ?hole_3

不要问我为了了解 this 是正确的语法必须查阅哪个黑暗魔法书：

:elab hole_3
intro `{{l}}
induction (Var `{{l}})
compute

此时，这是我在终端看到的结果

{S_147}
----------              Assumptions:              ----------
 l : Nat
----------                 Goal:                  ----------
{Z_146} : (c : Nat) -> (r : Nat) -> plus c r = plus c r

使用 reflexivity 来总结归纳的基础会非常好，但是...

The goal is not an equality, so Pruviloj.Core.reflexivity is not applicable.

引入剩余的变量会很好，但是...

INTERNAL ERROR: Can't introduce here.
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

Answer 1

在引入新变量之前你需要 compute 和 attack，虽然我不太确定为什么 :) 这是有效的完整战术脚本：

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' = %runElab tac 
  where 
  tac : Elab ()
  tac = do [l,c,r] <- intros
           [z,s] <- induction (Var l)

           focus z
           compute
           reflexivity

           focus s 
           compute
           attack
           [n, prf] <- intros
           rewriteWith (Var prf)
           reflexivity
           solve

如何在 Idris 1.3.2 中使用归纳？

How to use induction in Idris 1.3.2?

idris