16

私が証明しようとしているのは、私の考えでは合理的な定理です。

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

帰納法による証明は、私がこれを証明する必要があるポイントに到達します:

lemma1 : (n : Nat) -> (n - 0) = n

これは、対話型証明器を使用して証明しようとすると (簡単にするために補題)、次のようになります。

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

マイナスの定義について何かが欠けているに違いないと感じたので、ソースで調べました。

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

私が必要とする定義はすぐそこにあります！minus left Z = left. 私の理解では、イドリスはここに置き換えるだけでよくminus m 0、mこれは反射的に真実です。私は何を逃したのですか？

4

4 に答える 4

26

残念ながら、ここで証明したい定理は実際には正しくありません。なぜなら、Idris 自然は減算を 0 で切り捨てるからです。反例theorem1はn=3, m=0です。評価を進めてみましょう。

まず、次のように置き換えます。

3 + (0 - 3) = 0

次に、基礎となる Num インスタンスに構文を desugar し、呼び出される実際の関数を入れます。

plus (S (S (S Z))) (minus Z (S (S (S Z))))) = Z

Idris は厳密な値渡し言語であるため、最初に関数への引数を評価します。したがって、式を縮小しますminus Z (S (S (S Z))))。の定義をminus見ると、最初の引数が であるため、最初のパターンが適用されますZ。したがって、次のようになります。

plus (S (S (S Z))) Z = Z

plusは最初の引数で再帰的であるため、評価の次のステップでは次の結果が得られます。

S (plus (S (S Z)) Z) = Z

plus最初の引数として a を取得するまでこの方法を続け、Zその時点で 2 番目の引数 を返しZ、型を生成します。

S (S (S Z)) = Z

居住者を構築することはできません。

上記が少し衒学的で低レベルに見えた場合は申し訳ありませんが、依存型を使用する場合は特定の削減手順を考慮することが非常に重要です。これは、型の内部で「無料」で取得できる計算であるため、便利な結果が得られるように調整することをお勧めします。

ただし、上記のpdxleifのソリューションは、補題にはうまく機能します。最初の引数のケース分割は、パターン マッチをminus機能させるために必要でした。パターン マッチでは上から下に進み、最初のパターンは最初の引数に具体的なコンストラクターがあることを思い出してください。

于 2014-05-08T07:49:52.427 に答える
10

インタラクティブな編集をいじって、ケース分割と証明検索を行ったところ、次の結果が得られました。

lemma1 : (n : Nat) -> (n - 0) = n
lemma1 Z = refl
lemma1 (S k) = refl

これはマイナスの定義から明らかです。入力 var が単純に n の場合はボーキングしていたのかもしれません。Z などの場合は異なる動作をする可能性があるからです。それとも再帰？

于 2014-05-08T07:06:13.793 に答える
1

完全を期すために (タクティック言語は推敲者リフレクションを支持して廃止されました)、タクティック言語で補題を証明する方法は を呼び出すことであると付け加えますinduction n。次に、 を使用trivialして各ケースを表示できます (intros帰納的な場合の an の後)。

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n
-lemma1> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n
-lemma1> induction n
----------              Other goals:              ----------
elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_Z0 : minus 0 0 = 0
-lemma1> trivial
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_S0 : (n__0 : Nat) ->
          (minus n__0 0 = n__0) -> minus (S n__0) 0 = S n__0
-lemma1> intros
----------              Other goals:              ----------
{hole8},elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
 n__0 : Nat
 ihn__0 : minus n__0 0 = n__0
----------                 Goal:                  ----------
{hole9} : minus (S n__0) 0 = S n__0
-lemma1> trivial
lemma1: No more goals.
-lemma1> qed
Proof completed!
lemma1 = proof
  intros
  induction n
  trivial
  intros
  trivial
于 2015-11-02T10:03:02.450 に答える
1

念のため、イドリスのプレリュードでは、あなたのもののように、多くの算術補題がすでに定義されています。

total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z        = refl
minusZeroRight (S left) = refl
于 2014-12-02T15:04:35.210 に答える