證明最大的可交換在COQ

Question

我有一個函數max：

​​

和max可交換的證據如下：

Theorem max_comm : 
    forall n m : nat, max n m = max m n. 
Proof. 
    intros n m. 
    induction n as [|n']; 
    induction m as [|m']; 
     simpl; trivial. 
(* Qed. *) 

這讓送行S (max n' m') = S (max m' n')，這似乎是正確的，並且考慮到基本情況已經被證明，似乎應該能夠告訴coq「只使用遞歸！」。但是，我無法弄清楚如何去做。任何幫助？

Answer 1

問題是你在引入變量n之前引入變量m，這使得歸納假設不那麼一般。試試這個。

intro n; induction n as [| n' IHn']; 
    intro m; destruct m as [| m']; 
    simpl; try (rewrite IHn'); trivial.