Coqでn：nat、〜n <nを証明する方法

Question

私は時間のために混乱してきたと私はコックに

forall n:nat, ~n<n 

を証明する方法を見つけ出すことはできません。私は本当にあなたの助けが必要です。助言がありますか？

Answer 1

この補題は、標準ライブラリである：結果の中で

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に入ろうとするか、<=に入ろうとすることができます。 <=述語は誘導によって定義され、これらの場合には、その仮説を立証する必要があります。しかし、ここでnを理由にして、nは^の後にの後継者であることを示し、S nとなり、すぐにnに誘導を開始することができます。あなたは仮説1 <= 0を持っていて、これは（目標はFalseである）ことは不可能であることを証明する必要があります。

induction nした後は、基本ケースを証明する必要があります。通常、誘導仮説をケースに分解するためには、inductionの戦術またはその変形の1つを使用します。この戦術は、仮説に関するかなり複雑な依存症例分析を構築する。何が起こっているのかを確認する方法の1つは、1 = 0を必要とするle_nコンストラクタを使用するか、またはS m = 0を必要とするle_Sコンストラクタを使用するという仮説の証明のいずれかです。いずれの場合も、要求は明らかに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。

Answer 2

Require Import Arith. 
auto with arith.