在伊德里斯挣扎着改写策略

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).

你需要做的是使用if 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,所以它可以在没有它的情况下工作,但我认为在这种情况下它可以更清楚地发生了什么)