6

discriminate舞台裏で戦術がどのように機能するのか興味がありました。したがって、私はいくつかの実験を行いました。

最初に単純な帰納的定義:

Inductive AB:=A|B.

discriminate次に、戦術によって証明できる簡単な補題:

Lemma l1: A=B -> False.
intro.
discriminate.
Defined.

証明がどのように見えるか見てみましょう:

Print l1.

l1 = 
fun H : A = B =>
(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)
     : A = B -> False

これはかなり複雑に見えますが、ここで何が起こっているのかわかりません。したがって、同じ補題をより明示的に証明しようとしました。

Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined.

Coqがこれで何を作ったかをもう一度見てみましょう:

Print l2.

l2 = 
fun e : A = B =>
match
  e as e0 in (_ = a)
  return
    (match a as x return (A = x -> Type) with
     | A => fun _ : A = A => IDProp
     | B => fun _ : A = B => False
     end e0)
with
| eq_refl => idProp
end
     : A = B -> False

今、私は完全に混乱しています。これはさらに複雑です。ここで何が起こっているのか誰でも説明できますか?

4

2 に答える 2

9

l1この用語を調べて、そのすべての部分を説明しましょう。

l1 : A = B -> False

l1は含意であるため、Curry-Howard 対応により、抽象化 (関数) になります。

fun H : A = B =>

ここで、 type を持たなければならない抽象化の本体を構築する必要がありますFalse。このdiscriminateタクティックは、 body を application として実装することを選択します。これは、 の帰納原理の単なるラッパーでf xあり、 の証明があれば、必要な命題の証明を得ることができるということです ( ):f = fun H0 : False => False_ind False H0FalseFalseFalse_ind : forall P : Prop, False -> P

(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)

ベータ削減の 1 つのステップを実行すると、上記を単純化して次のようになります。

False_ind False
          (eq_ind A
             (fun e : AB => match e with
                            | A => True
                            | B => False
                           end) I B H)

への最初の引数False_indは、構築している項の型です。あなたが証明するならA = B -> True、それはだったでしょうFalse_ind True (eq_ind A ...)。

ところで、体をさらに単純化できることは簡単にわかります。False_ind動作させるには、 の証明を提供する必要がありますが、Falseここで構築しようとしているのはまさにそれです! False_indしたがって、次のようにして、完全に取り除くことができます。

eq_ind A
  (fun e : AB => match e with
                 | A => True
                 | B => False
                 end) I B H

eq_indequals は equals の代わりに使用できるという、等式の帰納法です。

eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
   P x -> forall y : A, x = y -> P y

言い換えると、 の証明があれば、 に等しいすべてP xのに対して が成り立ちます。yxP y

それでは、順を追ってFalse使用の証明を作成しましょうeq_ind(最終的に項を取得する必要がありeq_ind A (fun e : AB ...)ます)。

もちろん、 から始めて、eq_indそれをいくつかに適用します-その目的のためにx使用しましょう。A次に、述語が必要Pです。書き留める際に心に留めておくべき重要なことの 1 つPは、証明できなければならないということP xです。この目標は簡単に達成できTrueます。自明な証明を持つ命題を使用します。覚えておくべきもう 1 つのことは、( False) を証明しようとしている命題です。入力パラメーターが でない場合は、それを返す必要がありますA。上記のすべてで、述語はほとんどそれ自体を記述します。

fun x : AB => match x with
              | A => True
              | B => False
              end

の最初の 2 つの引数があり、eq_indさらに 3 つ必要です。Someは、私たちが証明したい命題、すなわち、およびこの答えの冒頭で呼び出される証明 thatに私たちを導きます。これらを互いに積み重ねるとxATrueIyBA = BH

eq_ind A
       (fun x : AB => match x with
                  | A => True
                  | B => False
                  end)
       I
       B
       H

そして、これがまさにdiscriminate私たちに与えられたものです（いくつかのラップを法として）。

于 2017-03-23T07:33:25.477 に答える