証明書がCOQで2つの再帰関数を展開することを含む

Question

私はCoqを学び始めました。かなり単純なものを証明しようとしています。リストにxが含まれている場合、そのリストのxのインスタンス数は0より大きくなります。

私は含まれており、以下のような機能を数える定義しました：私は証明しようとしている

Fixpoint contains (n: nat) (l: list nat) : Prop := 
    match l with 
    | nil => False 
    | h :: t => if beq_nat h n then True else contains n t 
    end. 

Fixpoint count (n acc: nat) (l: list nat) : nat := 
    match l with 
    | nil => acc 
    | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t 
    end. 

を：

Lemma contains_count_ge1 : forall (n: nat) (l: list nat), contains n l -> (count n 0 l > 0). 

私は証拠がdefinitioを展開伴います理解カウント数が含まれていますが、「含まれているので、リストはゼロではありません。xのlにはbeq_nat h xが本当です」と表示されています。これを行うための戦術の使い方を理解することはできません。どんな指針も大変ありがとうございます。

Answer 1

まあ、基本的なCoqについては、ここで取り上げることができるIMO以外の多くの疑問があります。この特定の問題のために、私はこの方法を進行する（実際に私はMathCompですでに提供さ補題を使用します）：

From Coq Require Import PeanoNat Bool List. 

Fixpoint contains (n: nat) (l: list nat) : bool := 
    match l with 
    | nil => false 
    | h :: t => if Nat.eqb h n then true else contains n t 
    end. 

Fixpoint count (n : nat) (l: list nat) : nat := 
    match l with 
    | nil => 0 
    | h :: t => if Nat.eqb h n then S (count n t) else count n t 
    end. 

Lemma contains_count_ge1 n l : contains n l = true -> count n l > 0. 
Proof. 
induction l as [|x l IHl]; simpl; [now congruence|]. 
now destruct (Nat.eqb_spec x n); auto with arith. 
Qed. 

私の「標準」解決策：

Lemma test n (l : list nat) : n \in l -> 0 < count_mem n l. 
Proof. by rewrite lt0n => /count_memPn/eqP. Qed. 

とcountの異なる定義と有用であることを証明し得るcontains：

Fixpoint contains (n: nat) (l: list nat) : bool := 
    match l with 
    | nil => false 
    | h :: t => Nat.eqb h n || contains n t 
    end. 

Fixpoint count (n : nat) (l: list nat) : nat := 
    match l with 
    | nil => 0 
    | h :: t => Nat.b2n (Nat.eqb h n) + (count n t) 
    end. 

Answer 2

ejgallegoはすでに彼の答えにあなたの問題に最適なソリューションを与えました。私はまだ彼が残した重要な点を強調したいと思います.Coqでは、常に第一原理から主張し、あなたの証明について非常にぺだんと正確でなければなりません。あなたは次のように証拠を進めるべきであると主張し

：containsが真であるので、beq_nat h xがtrueなるようなlに要素xが存在しなければならないよう

リストは、nilすることはできません。

これは人間には直感的な意味合いがありますが、Coqが理解するには十分正確ではありません。 ejgallegoの答えが示すように、問題は、あなたの非公式な推論が誘導の使用を隠すことです。確かに、それを戦術に翻訳する前でさえ、あなたの議論をより詳細に展開しようとするのは有益です。

n : natとns : list natの場合は、contains n nsはcount n 0 ns > 0を意味することを証明しましょう。我々はリストnsの誘導によって進める。 ns = nilの場合、の定義は、Falseが成立することを意味します。矛盾。したがって、我々は以下の帰納仮説：contains n ns' -> count n 0 ns' > 0を用いることができるケースns = n' :: ns'を残す。考慮すべき2つのサブケースがあります：beq_nat n n'がtrueであるかどうか。

• beq_nat n n'がcountの定義によって、trueであれば、私たちはただcount n (0 + 1) ns' > 0ことを示さなければならないことがわかります。ここに進むための直接的な方法はないことに注意してください。これは、アキュムレータを使用してcountをテール再帰的に書き込んだためです。これは関数型プログラミングでは完全に合理的ですが、countに関する証明プロパティをより困難にすることができます。この場合、帰納法によっても証明された次の補題が必要です：forall n acc ns, count n acc ns = acc + count n 0 ns。私はあなたがこれを証明する方法を理解できるようにします。しかし、すでに確立していると仮定すると、その目標は、1 + count n 0 ns' > 0に縮小されます。これは単純な算術演算によって真実です。 （そこ補助補題を必要としなくても簡単な方法ですが、それはあなたが証明しているの文を一般少し必要になります。）containsとcountの定義によって、falseある

• beq_nat n n'場合、当社は必要になりますcontains n ns'はcount n 0 ns' > 0を示しています。これはまさに誘導仮説が私たちに与えるものであり、私たちは完了しています。

ここでは2つの教訓があります。最初の1つは、正式な証明を行うには、しばしばシステムが理解できる正式な用語であなたの直感を翻訳する必要があるということです。私たちは直感的に何らかの要素がリストの中にあることを意味するものを知っています。しかし、それが正式な意味を説明するならば、リストの再帰的なトラバーサルに頼ることになります。これはおそらくCoqで書いたcountという非常に明確な定義になります。そして再帰について推論するためには、誘導が必要です。第2の教訓は、あなたがCoqで物事を定義する方法が、あなたが書いた証明に重要な結果をもたらすということです。 ejgallegoの解は、countの定義がテール再帰的ではなかったため、標準ライブラリのものを超えて補助的補助定を必要としませんでした。