在 Idris 中与重写策略作斗争

Question

我正在翻阅 Terry Tao 的真实分析教科书，它从自然数开始构建基础数学。通过尽可能多地形式化证明，我希望自己熟悉 Idris 和依赖类型。

我定义了以下数据类型：

data GE: Nat -> Nat -> Type where
    Ge : (n: Nat) -> (m: Nat) -> GE n (n + m)

表示一个自然数大于或等于另一个自然数的命题

我目前正在努力证明这种关系的自反性，即构造带有签名的证明

geRefl : GE n n

我的第一次尝试是简单地尝试 geRefl {n} = Ge n Z，但它的类型是 Ge n (add n Z)。为了使它与所需的签名统一，我们显然必须执行某种重写，大概涉及引理

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left

我最好的尝试如下：

geRefl : GE n n                                                                 
geRefl {n} = x                                                                  
    where x : GE n (n + Z)                                                      
          x = rewrite plusZeroRightNeutral n in Ge n Z

但这不会进行类型检查。

能否请您给出这个定理的正确证明，并说明其背后的原因？

Answer 1

第一个问题很肤浅：您试图在错误的地方应用重写。如果你有 x : GE n (n + Z)，那么如果你想将它用作 geRefl : GE n n 的定义，你将不得不重写它的类型，所以你必须写

geRefl : GE n n
geRefl {n} = rewrite plusZeroRightNeutral n in x

但这仍然行不通。真正的问题是你只想重写类型 GE n n 的一部分：如果你只是使用 n + 0 = n 重写它，你会得到 GE (n + 0) (n + 0)，你仍然无法证明使用Ge n 0 : GE n (n + 0).

你需要做的是利用如果a = b，那么x : GE n a可以变成x' : GE n b的事实。这正是标准库中的 replace 函数所提供的：

replace : (x = y) -> P x -> P y

使用这个，通过设置P = GE n，并使用Ge n 0 : GE n (n + 0)，我们可以将geRefl写成

geRefl {n} = replace {P = GE n} (plusZeroRightNeutral n) (Ge n 0)

（请注意，Idris 完全能够推断出隐式参数 P，因此它可以在没有它的情况下工作，但我认为在这种情况下它可以更清楚地说明正在发生的事情）

在 Idris 中与重写策略作斗争

Struggling with rewrite tactic in Idris

dependent-type

idris

theorem-proving