在伊德里斯與改寫策略苦苦掙扎

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

在伊德里斯與改寫策略苦苦掙扎

回答

相關問題