Idrisの書き直し戦術に苦労している

Question

私は自然数から基本的な数学を構築する、テリー・タオの本物の分析教科書を見ています。できるだけ多くの証明を公式化することで、Idrisと従属型の両方に慣れることを望みます。

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

一つ自然数別以上であるという命題を表す：

Iは、以下のデータ型を定義しています。

私は現在、すなわち署名付き証明を構築するために、この関係の再帰性を証明するために苦労してい

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 

が、これはです。TypeCheckていません。

この定理の正確な証拠を与えて、それの背後にある推論を説明できますか？

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 : (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) 

として（イドリスは完全に可能であることに注意してください：これは標準ライブラリの replace機能を提供して正確に何であります暗黙的なパラメータ Pを推論するためには、それがなくても動作しますが、この場合は何が起きているのかがはっきりします）