Reflのリライトを使用して

Question

私は第8章Ididrisによるタイプドリブン開発を進めており、リライトとReflとのやりとりに関する質問があります。 plusCommutative 1 kが1 + kのすべてのインスタンスを探し、k + 1と交換します

myReverse : Vect n elem -> Vect n elem 
myReverse [] = [] 
myReverse {n = S k} (x :: xs) 
    = let result = myReverse xs ++ [x] in 
      rewrite plusCommutative 1 k in result 

：

このコードは、表現上の作品を書き換え方法の例として示されています。

私の質問には回答された状態でmyPlusCommutesとしてexerciesの一部としてplusCommutativeを書き換えるには、この解決策である。なぜなら何から

myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl 

：私はこのラインでトラブルを抱えています

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n 
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl 
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in 
         rewrite plusSuccRightSucc m k in Refl 

私はそのような行でそれ自身でReflを使って理解することができます：

myPlusCommutes Z m = Refl 

私はこのエラーを取得する：

When checking right hand side of myPlusCommutes with expected type 
     0 + m = m + 0 

Type mismatch between 
     plus m 0 = plus m 0 (Type of Refl) 
and 
     m = plus m 0 (Expected type) 

Specifically: 
     Type mismatch between 
       plus m 0 
     and 
       m 

まず第一に、私は実現しなかった一つのことは、REFLが=の右側から動作し、その方向からの反射を求めて表示されていることです。

次に、plus m 0 = plus m 0からm = plus m 0に変化REFL結果を書き換え、左からの書き換えが、最初の交換後に停止し、私が持っていると同じように、これまでmでplus m 0のすべてのインスタンスを置き換えるためにするようつもりはないように思わ期待される。

最終的には、これが私の質問です。なぜ書き換えがそのような振る舞いをするのですか？等価型の書き換えは異なりますか？その場合は、=の左側に置き換えて書き換えますか？

λΠ> :set showimplicits 
λΠ> :t Refl 
Refl : {A : Type} -> {x : A} -> (=) {A = A} {B = A} x x 

イドリスは、コンテキストからの情報を使用して用語Reflにタイプを帰しようとしていることを意味し：

Answer 1

何が起こっているかを理解するために、ここでは考慮にReflが多型であるという事実を取る必要があります。例えば。 ReflのmyPlusCommutes Z m = Reflは、タイプplus m 0 = plus m 0である。 Idrisは、LHSのmyPlusCommutes 'を出力し、タイプm = mをReflに帰属させることができました。また、x式を指定することもできます。Refl {x = m}。

今、あなたの現在の目標、すなわちrewrite Eqに関してrewrite作品があなたの目標では、ないReflのいくつかの可能なタイピングでのRHSとEqのLHSのすべての出現を置き換えます。

私はあなたに私が何を意味するか説明するために書き換えのシーケンスを使用しての愚かな例を挙げてみましょう：

foo : (n : Nat) -> n = (n + Z) + Z 
foo n = 
    rewrite sym $ plusAssociative n Z Z in -- 1 
    rewrite plusZeroRightNeutral n in  -- 2 
    Refl          -- 3 

• 我々がゴールn = (n + Z) + Zで始まり、その後、
• ライン1を使用してn = n + (Z + Z)に目標を回します次に、
• 2行目は現在の目標n = n + Z（これは定義的にはn = n + (Z + Z)に等しい）をn = n
0123に変えます
• 3行目は現在の目標を証明する用語を提供します（もっと明示したければReflの代わりにRefl {x = n}と書くことができます）。