在伊德里斯与改写策略苦苦挣扎

我正在通过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

但这并不进行类型检查。

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

来源

2016-06-16 user1502040

它会更容易使它'GE：（m：Nat） - >（n ： Nat） - > GE n（m + n）'代替。然后'geRefl = GE Z'。 – RhubarbAndC

@RhubarbAndC我考虑过这个，但它让其他事情变得更加困难。 – user1502040

第一个问题是肤浅的：你试图在错误的地方应用重写。如果你有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)

（注意，伊德里斯是完全能够以推断隐含参数P，所以它没有这个工作，但我认为在这种情况下，它使得它更清楚发生了什么）

来源

2016-06-17 02:24:53 Cactus

在伊德里斯与改写策略苦苦挣扎

回答

相关问题