在IDRIS 1中应用已知证据

Question

我试图通过练习来熟悉 Idris1 中的定理证明，但遇到了麻烦。

假设我有以下自然数的定义和我想要证明的以下定理：

data Natural = Z | S Natural

plus : Natural -> Natural -> Natural
plus x Z = x
plus x (S y) = S (plus x y)

succBoth : {a : Natural} -> {b : Natural} -> (a = b) -> (S a = S b)
succBoth = ?succBothProof

plusZero : (y : Natural) -> plus Z y = y
plusZero = ?plusZeroProof

plusSwitch : (x : Natural) -> (y : Natural) -> plus (S x) y = S (plus x y)
plusSwitch = ?plusSwitchProof

plusComm : (x : Natural) -> (y : Natural) -> plus x y = plus y x
plusComm = ?plusCommProof

我已经写好了前三个的证明。现在，当我想证明最后一个定理时，我遇到了应用早期证明的必要性。

Idris> :l Peano.idr
Holes: Peano.plusCommProof
*Peano> :elab plusCommProof
-Peano.plusCommProof> intro `{{x}}
...
-Peano.plusCommProof> intro `{{y}}
...
-Peano.plusCommProof> induction (Var `{{y}})
...
-Peano.plusCommProof> compute
...
-Peano.plusCommProof> attack
----------              Other goals:              ----------
{Z_103},{S_104}
----------              Assumptions:              ----------
 x : Natural
 y : Natural
----------                 Goal:                  ----------
{hole_7} : x = plus Z x

在这个阶段应用 plusZero 是很自然的事情，但我在尝试这样做时遇到了问题。我尝试通过 rewriteWith 应用它，请记住 plusZero 采用 Natural 类型参数。我尝试为其提供 x 变量，认为它能够从假设中推断出其 Natural 类型，但运气不佳：

-Peano.plusCommProof> rewriteWith `(plusZero (Var `{{x}}))
(input):1:15-35:When checking argument y to function Peano.plusZero:
        Type mismatch between
                Raw (Type of Var _)
        and
                Natural (Expected type)

How does one "cast" the < code>Raw 变量转换为上下文中的类型？

Answer 1

我无法让IDRIS 1版本使用，但是我确实安装了IDRIS 2，并以其样式编写了证明。

module Peano

data Natural = Zero | Succ Natural

plus : Natural -> Natural -> Natural
plus x Zero = x
plus x (Succ y) = Succ (plus x y)

succBoth : {a : Natural} -> {b : Natural} -> (a = b) -> (Succ a = Succ b)
succBoth rfl = cong (\ a => Succ a) rfl

plusZero : (y : Natural) -> plus Zero y = y
plusZero Zero = Refl
plusZero (Succ y)
  = let assumption = plusZero y in
        rewrite assumption in Refl

plusSwitch : (x : Natural) -> (y : Natural) ->
             plus (Succ x) y = Succ (plus x y)
plusSwitch x Zero = Refl
plusSwitch x (Succ y)
  = let assumption = plusSwitch x y in
        rewrite assumption in Refl

plusComm : (x : Natural) -> (y : Natural) -> plus x y = plus y x
plusComm x Zero = rewrite plusZero x in Refl
plusComm x (Succ y)
  = let assumption = plusComm x y in
        rewrite plusSwitch y x in
        rewrite assumption in Refl

诚然，更紧凑，但我更喜欢IDRIS 1：ELAB风格而不是可读性