1

私は関数を持っています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に「再帰を使用するだけです！」と伝えることができるはずです。しかし、私はそれを行う方法を理解することはできません。何か助けはありますか？

4

1 に答える 1

4

問題は、変数に対してm帰納法を実行する前に変数を導入することですn。これにより、帰納法の仮説が一般的ではなくなります。代わりにこれを試してください。

intro n; induction n as [| n' IHn'];
  intro m; destruct m as [| m'];
    simpl; try (rewrite IHn'); trivial.
于 2013-01-19T13:33:54.610 に答える