消除與命題案件勒柯克

Question

給定一個自然數列表類型的定義明顯，而這需要的最後一個元素或返回默認值的功能last，我試圖證明以下引理：

Lemma last_ignores_first : forall l : natlist, forall def n : nat, 
    length l > 0 -> 
    last def (n :: l) = last def l. 

現在我想證明一點，因爲l不是空的，所以對於h和t，它必須能夠以h::t的形式書寫，因此證明將遵循last的定義。但是，我怎樣才能在Coq中使用這些知識？如果我在l上做induction或destruct，我將不得不考慮l是[]的情況，這是一個被假設阻止的情況。我如何告訴它，l必須遵循某種形式？

Answer 1

您只需要使用反轉對你的假設，指出length l > 0：

intros [|x l] def n H. 
- (* Case l = [], contradiction *) 
    simpl in H. inversion H. 
- (* Continue normally *)