證明涉及展開兩個遞歸函數COQ

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納秒計數和包含，但然後我想說「列表不能爲零，因爲包含是真實的，所以必須有xl這樣的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已經給他回答一個偉大的解決您的問題。我仍想特別指出他忽略的一個重要問題：在科克，你必須始終從最初的原則出發爭論，並且對你的證明非常迂腐和精確。

您認爲，應該證明步驟如下：在l這樣beq_nat h x是true

列表不能nil，如contains是真實的，所以必須有一個元素x。

即使這具有直觀意義對於人類來說，這是不夠精確的勒柯克理解。正如ejgallego的答案所表明的那樣，問題在於你的非正式推理隱藏了誘導的用法。事實上，在將其轉化爲戰術之前，儘量擴大你的論點是有益的。我們可以這樣做，例如：

讓我們證明，對於每個n : nat和ns : list nat，contains n ns意味着count n 0 ns > 0。我們在列表ns上進行歸納。如果ns = nil，contains的定義意味着False成立;矛盾。因此，我們留下了案例ns = n' :: ns'，我們可以使用以下歸納假設：contains n ns' -> count n 0 ns' > 0。有兩種情況需要考慮：beq_nat n n'是否爲true。

• 如果beq_nat n n'是true，由count的定義，我們可以看到，我們只需要表明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。簡單的算術就是這樣。 （有，不需要輔助引理一個更簡單的方法，但它需要稍微概括你證明的聲明。）

• 如果beq_nat n n'是false，由contains和count的定義，我們需要以表明contains n ns'意味着count n 0 ns' > 0。這正是歸納假設給我們的，我們完成了。

有兩個教訓可以在這裏學到。第一，做形式證明往往需要用系統可以理解的正式術語來翻譯你的直覺。我們直觀地知道在列表中出現某些元素意味着什麼。但是如果我們要更正式地解釋這意味着什麼，我們會採用某種遞歸遍歷的方式，這可能會成爲您在Coq中編寫的count的定義。爲了推理遞歸，我們需要歸納。第二個教訓是，你在Coq中定義事物的方式對你寫的證明有重要的影響。 ejgallego的解決方案不需要超出標準庫中的輔助引理，這正是因爲他對count的定義不是尾遞歸。