IH 不能用作什么提示。在 Coq 中，当使用 eauto 直接给出归纳假设时意味着什么？

Question

看到相关问题引理不能用作提示但没有看起来超级有用+似乎更好地问新人，向那里的海报提出不相关的问题。我尝试做简单的引理：

  From mathcomp Require Import all_ssreflect.
  Require Import ZArith.
  From Hammer Require Import Tactics.
  From Hammer Require Import Hammer.

  Theorem n_plus_0_eq_n_sketch1:
  forall n:nat,
    n + 0 = n.
  Proof.
    have IH: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n. by apply nat_ind. (* succeeds *)

    
    (* close target with guessed lemmas **)
    (* by sauto use: IH. *) (* fails *)
    by eauto using IH. (* Gives error, IH cannot be used as a hint. *)

但是 eauto 策略给出了错误：

IH cannot be used as a hint.

为什么会这样？我给出的引理有什么问题？

我已经让它在其他情况下工作，所以我很困惑：

  Theorem add_comm_eauto_using:
    forall n m: nat,
      n + m = m + n.
    Proof.
      intros. 
      assert (H: forall n, n + 0 = n) by eauto using n_plus_zero_eq_n.
      assert (H': forall n m, S (n + m) = n + S m) by eauto using Sn_plus_m_eq_n_plus_Sm.
      induction n.
      - eauto using H, H'.
      - 
      (* auto using IHn, H, H'.  *)
      simpl.
      (* auto using IHn, H, H'. *)
      rewrite IHn.
      auto using H, H'.
    Qed.

是否有一些 eauto 之类的细节无法统一目标和我的引理之类的东西？

---

ref:

• 引理不能用作提示

Answer 1

eauto 通过匹配头符号来工作。不幸的是
IH 的头符号是一个变量 P 所以这就是您收到错误的原因（请参阅这里）

这是被接受的，但没有解决目标

have IH1 := IH (fun n => n + 0 = n).
eauto using IH1.