n m : natCoq で が隣接する偶数であると言う方法の 1 つは、その関係を 0 と 2 から帰納的に定義することです。
Inductive adj_ev : nat -> nat -> Prop :=
| ae_0 : adj_ev 0 2
| ae_1 : forall ( n m : nat ), adj_ev n m -> adj_ev m ( S ( S m ) )
| ae_2 : forall ( n m : nat ), adj_ev n m -> adj_ev m n.
ae_00 と 2 が隣接する偶数であることを示します。ae_1は、いくつかn m : natが隣接する偶数である場合、 と もそうであるmと述べていm + 2ます。これら 2 つのコンストラクターを使用すると、隣接する偶数のすべてのペアを無限大までカバーできます。ちょっと待って！これはn、 のm場合にのみ機能しn < mます。ae_2したがって、リレーション内の特定の数値ペアを反転 する最後のコンストラクターが必要です。
リレーションを定義したので、それが機能することを確認するためにサニティ チェックを行います。adj_ev 1 3たとえば、1 と 3 は隣り合った偶数ではないことを知っていますadj_ev。だから私は確かにそれを証明~ ( adj_ev 1 3 )できますよね？
Theorem test' : ~ ( adj_ev 1 3 ).
unfold not. intros H.
inversion H. inversion H0.
数回反転した後、すぐに無限ループに陥ります。Coq に「どうすれば隣接して偶数になるnことができるのか?」と尋ねているようなものです。mCoq は、「まあ、おそらくandmはn隣接しており...」と答えます。Coq は、「まあ、おそらく隣接しており、さらには...」と無限に言います。mnnm
一般的な問題は、いくつかの帰納的に定義された対称関係があるR場合、 が実際に成り立つ場所で成り立つことを示すのは簡単ですRが、成り立たない場所で成り立たないことを示すのは難しいことです。このような場合、矛盾を抽出するよりも優れた戦術があるinversionかもしれませんが、それが何であるかはわかりません。
何かご意見は？