代替案の注文に依存する関数に関する証明

Question

ハスケルでかなりの経験をして、私はちょうど定理証明のためにIdrisを使い始めました。これは、単純なステートメントを証明しようとしたときに直面した問題を示す最小限の例です。

たちが総機能test持って考えてみましょう。もちろん

total test : Integer -> Integer 
test 1 = 1 
test n = n 

を、私たちは関数がtest n = nに単純化することができていることがわかりますが、のは、それを証明してみましょう。

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test n = Refl 

しかし、これは型チェックしません：私は単純にすべてのケースの上につもりです

Type mismatch between 
     n = n (Type of Refl) and 
     test n = n (Expected type) 

Specifically: 
     Type mismatch between 
       n 
     and 
       test n 

ので、問題はイドリスはlemma_testの第二のケースのために推測することができないということのようですnは1と等しくなく、testの2番目のケースも適用する必要があります。

Integerのためのケースのように私たちは、もちろん、面倒な、または不可能であることができる、明示的にすべてのケースを一覧表示しようとすることができます：

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test 2 = Refl 
lemma_test 3 = Refl 
... 

このようなステートメントを証明する方法はあります有限集合のデータコンストラクタ上で定義されていないが、この例ではtestのようなパターンマッチングが上から下に作用するという事実に依存する関数に対して、

多分、このような機能が非常に頻繁に起こると考えて、私が見逃している単純な解決策があるかもしれません。

Answer 1

Integerは原始的であり、誘導的に定義されたタイプではないため、完全なパターンマッチングはできません。具体的には、Idrisでは（そして実際には最先端のAgdaでも！）、問題は、以前のすべてのパターンに関する情報を保持していないため、「デフォルト」のパターンマッチについて実際には証明できませんそれは一致しませんでした。私たちの場合、test n = 1は、nが1と等しくないという証拠を私に与えません。

通常の解決策ではなく、フォールスルーの（あまりにも良いかもしれないBoolean平等）決定可能平等を使用することです。ここでは

import Prelude 

%default total 

test : Integer -> Integer 
test n with (decEq n 1) 
    test n | Yes p = 1 
    test n | No p = n 

lemma_test : (n : Integer) -> (test n) = n 
lemma_test n with (decEq n 1) 
lemma_test _ | (Yes Refl) = Refl 
lemma_test n | (No contra) = Refl 

、No結果が失敗した試合についての明確な証拠を運びます。

Answer 2

Integerがどのように定義されているのかわかりません、または誘導などの方法がわからないので、これはあなたの質問に対する完全な答えではありません。しかし、おそらくNatバージョンもあなたに有益でしょうか？ （また、多分あなたは実際にあなたの第二の例では、あなたが唯一の正のナチュラルを列挙するので、Natを意味？）

あなたはNatの使用するtestを変更する場合：あなたは徹底的なパターンでマッチングを行うことができます

total test : Nat -> Nat 
test (S Z) = 1 
test n = n 

をlemma_test：

total lemma_test : (n : Nat) -> test n = n 
lemma_test (S Z) = Refl 
lemma_test Z = Refl 
lemma_test (S (S k)) = Refl 

Answer 3

Integerはイドリスで定義されているのではなく、GMPのbigintsに延期されていません。これはIdrisにとっては事実上不透明ですが、このようにコンパイル時の事例についてあなたが判断できるものではないようです。誘導的に定義されたNatのようなものを使って、基本ケースと再帰的ケースの形で証明について話すことができます。

このタイプのエラーは、test nではありませんが、test nという表現を減らすことはできません。私はそれが動作する方法であるかどうかはわかりません - 明らかにそれは総機能であり、それはafaikの総機能を減らすことになっています。おそらくIdrisに対するIntegerの不透明度に関連しているのでしょうか？

自由変数をlabmdaパラメータとして導入することで、replでの削減をテストできます。例えば。\n => test nは\n => test n : Integer -> Integerをそのまま返信します（変更なし）。ただし、定義からtest 1 = 1ケースを削除してもう一度試してみると、\n => n : Integer -> Integerが返されます。test n〜nになります。そしてあなたの証拠はそのまま現れます。