識別戦術はどのように機能しますか？

Question

私はカーテンの後ろでdiscriminate戦術がどのように働いているのか興味がありました。そこで私はいくつかの実験を行った。その後

Inductive AB:=A|B. 

discriminate戦術によって証明することができ、簡単な補題：

まず、単純な誘導定義

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 l1: A=B -> False. 
intro. 
discriminate. 
Defined. 

のは、証明はどのようなものか見てみましょう

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

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

ましょう再びコックはこれで作られたものを参照してください：

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 

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

Answer 1

このl1の用語を説明し、そのすべての部分を説明してください。

l1 : A = B -> False 

l1ので、カリー=ハワード同型対応によって、それは抽象化（機能）だ、含意です：

fun H : A = B => 

は、今、私たちはタイプFalseを持っている必要があり、私たちの抽象化の体を構築する必要があります。 discriminate戦術は身体をアプリケーションとして実装することを選択しますf x、f = fun H0 : False => False_ind False H0そしてFalseの証拠があれば、あなたが望む命題の証拠を得ることができると言われるFalseの誘導原則のラッパーです（False_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) 

、我々はFalse_indへの最初の引数は、我々が構築している用語のタイプである

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

に上記簡素化します。 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_indはイコール等号の代わりに使用することができると言って、平等のための誘導原理である：つまり

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

、場合1つはP xの証明を有し、次いで全てについてyはxに等しく、P yが成立する。

eq_indを使用してFalseの証明をステップバイステップで作成します（最後にeq_ind A (fun e : AB ...)という用語を取得する必要があります）。

eq_indから始めて、xに適用します。そのためにAを使用しましょう。次に、述語Pが必要です。 Pを書いている間、覚えておくべき重要なことの1つは、P xを証明できることです。この目標は達成が容易です。Trueという命題を使用しますが、それは簡単な証明があります。覚えておくべきもう一つのことは、私たちが証明しようとしている命題（False）です。入力パラメータがAでない場合、それを返すべきです。すべての述語以上により はほとんど自分自身を書き込みます

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

我々はeq_indのために最初の二つの引数を持っているし、我々は3つの必要があります：Trueの証拠であるxがAある支店の証明、すなわちI。 yがあります。これは、私たちが証明したいという命題につながります。すなわち、Bと、この回答の冒頭にHというA = Bという証明があります。スタッキングこれら互いの上に私たちは

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

を取得し、これはdiscriminateは（いくつかのラッピングを法）私たちを与えたまさにです。

Answer 2

別の答えは差別的な部分に焦点を当てていますが、私はマニュアルプルーフに焦点を当てます。あなたは試してみました：注意とコックを使用して、私はしばしば不快になるべきである何

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

は、コックは、それが内部的にうまく型付けされた用語に書き換え、不明確な定義を受け入れることです。 Coqはそれ自身をいくつか追加しているので、あまり冗長ではありません。しかし、一方で、Coqは入力したものとは異なる用語を操作します。

これはあなたの証拠の場合です。当然、eのパターンマッチングには、eqタイプの単一のコンストラクタであるコンストラクタeq_reflが必要です。ここでCoqは平等に人が住んでいないことを検出し、コードを修正する方法を理解しますが、入力したものは適切なパターンマッチングではありません。

二つの成分は、ここで何が起こっているかを理解するのに役立ちます。

• eq
• の定義フルパターンマッチング構文を、as、inとreturn用語

まずとともに、 eqの定義を見ることができます。

Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : x = x. 

この定義は、より自然な（いずれにしても、より対称的）ように見えることに注意してください。

Inductive eq {A : Type} : A -> A -> Prop := eq_refl : forall (x:A), x = x. 

これはeqは、最初の定義ではなく秒で定義されていることは本当に重要です。特に、私たちの問題については、重要なことは、x = yではxがパラメータであり、yはインデックスであることです。つまり、xはすべてのコンストラクターで一定ですが、yは各コンストラクターで異なる可能性があります。タイプVector.tと同じ違いがあります。要素を追加すると、ベクトルの要素の型は変更されません。そのため、要素として実装されます。しかし、そのサイズは変わる可能性があるため、インデックスとして実装されています。

ここで、パターンマッチングの拡張構文を見てみましょう。ここで私が理解していることを簡単に説明します。より安全な情報の参照を躊躇しないでください（https://coq.inria.fr/refman/Reference-Manual020.html）。 return句を使用すると、ブランチごとに異なる戻り値の型を指定できます。この節では、一致した単語と型インデックスをそれぞれバインドする、パターンマッチングの句のasとin節で定義されている変数を使用できます。 return句は、各ブランチのコンテキストで解釈され、このコンテキストを使用してasとinの変数を置換し、ブランチを1つずつタイプチェックし、外部視点からmatchを入力するために使用されます。

Definition test n := 
    match n as n0 return (match n0 with | 0 => nat | S _ => bool end) with 
    | 0 => 17 
    | _ => true 
    end. 

nの値に応じて、我々は同じ型を返すされていません。

はここas句と不自然な例です。 testのタイプはforall n : nat, match n with | 0 => nat | S _ => bool endです。しかし、Coqがどのような場合に一致するかを決めることができれば、タイプを単純化することができます。例：ここでは

Definition test2 n : bool := test (S n). 

、コックはnが何であれ、testに与えられたS nはタイプboolのものとしてつながる、ということを知っています。

同等性については、今回はin節を使用して同様のことを行うことができます。

Definition test3 (e:A=B) : False := 
    match e in (_ = c) return (match c with | B => False | _ => True end) with 
    | eq_refl => I 
    end. 

ここでは何が起こっていますか？本質的には、Coqタイプは、matchとmatchのブランチを別々にチェックします。eq_reflの場合、cは（パラメータと同じ値のインデックスをインスタンス化するeq_reflという定義のため）Aに等しいので、タイプTrue、ここではIの値が返されました。しかし、外部から見ると、cはB（eはA=Bなので）、returnはmatchがFalseという値を返していると主張しています。 test2で見たタイプのパターンマッチングを単純化するCoqの機能をここで使用します。他のケースではBよりTrueを使用しましたが、特にTrueは必要ありません。 eq_reflブランチで何かを返すことができるような、いくつかの居住型が必要です。

Coqによって生成された奇妙な用語に戻ると、Coqによって使用される方法は類似していますが、この例では確かに複雑です。特に、Coqは、役に立たないタイプや用語が必要な場合に、idPropが住むタイプIDPropを使用することがよくあります。これらは上に使用されたTrueとIに対応しています。

最後に、coq-clubに関する議論をlinkで行いました。これは、拡張パターンマッチングがCoqでどのようにタイプされているかを理解するのに役立ちました。