3

私は何時間も混乱しており、証明する方法がわかりません

forall n:nat, ~n<n

コックで。私は本当にあなたの助けが必要です。助言がありますか？

クラッシュです。詳細については、デバッグ ナビゲーターを介してスタック トレースを参照してください。

4

2 に答える 2

6

この補題は標準ライブラリにあります:

Require Import Arith.
Lemma not_lt_refl : forall n:nat, ~n<n.
Print Hint.

その中にはlt_irrefl. それを実現するより直接的な方法は、

info auto with arith.

これは目標を証明し、次の方法を示します。

intro n; simple apply lt_irrefl.

証明の場所はわかっているので、第一原理からの証明方法のヒントを示します (これが宿題のポイントだと思います)。

まず、否定を証明する必要があります。これはn<n、仮説として推し進め、矛盾を推測できることを証明することを意味します。次に、推論するためにn<n、それをその定義に展開します。

intros h H.
red in H.   (* or `unfold lt in H` *)

S n <= n次に、それが起こり得ないことを証明する必要があります。第一原理からこれを行うには、その時点で 2 つの選択肢がありnます<=。述語は帰納法によって定義され、多くの場合、これらのケースではそれ<=について帰納する必要があります。つまり、仮説の証明について帰納法によって推論する必要があります。ただし、ここでは、最終的に を推論して、が の m番目の後継者ではないことnを示す必要があり、すぐに導入を開始できます。nS nn

の後induction n、ベース ケースを証明する必要があり1 <= 0ます。仮説 があり、これが不可能であることを証明する必要があります (目標は ですFalse)。通常、帰納的仮説をケースに分解するには、induction戦術またはその変形の 1 つを使用します。この戦術は、仮説に関するかなり複雑な従属ケース分析を構築します。何が起こっているかを確認する 1 つの方法は、 を呼び出すsimple inversionことです。これにより、2 つのサブゴールが残ります: 仮説の証明がコンストラクターを1 <= 0使用してle_n、それが必要になるか1 = 0、または証明がle_Sコンストラクターを使用して、それが必要になりS m = 0ます。どちらの場合も、要件は の定義と明らかに矛盾しているSため、戦術discriminateはサブゴールを証明します。の代わりにsimple inversion H、使用できますinversion H、この特定のケースでは、目標を直接証明します (不可能な仮説のケースは非常に一般的であり、本格的なinversion戦術に組み込まれています)。

S n <= nさて、帰納法のケースに目を向けると、すぐに から証明したいポイントにたどり着きS (S n) <= S nます。これを、一般化できる別の補題 (最初に証明する必要があります) として述べることをお勧めしますforall n m, S n <= S m -> n <= m。

于 2011-11-12T17:01:19.467 に答える
3 
Require Import Arith.
auto with arith.
于 2011-11-12T14:15:42.730 に答える