coq - 在 coq 中证明 max 的交换性

Question

我有一个功能max：

Fixpoint max (n : nat) (m : nat) : nat :=
  match n, m with
    | O, O => O
    | O, S x => S x
    | S x, O => S x
    | S x, S y => S (max x y)
  end.

和以下的交换性证明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

问题是您m在对变量进行归纳之前引入变量n，这使得归纳假设不那么普遍。试试这个。

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