coq - 如何在 Coq 中使用带有假设的策略？

Question

我是 Coq 的新手，我遇到了死胡同。我有一个大致像这样的归纳定义（我之前已经定义了归纳接受）：

Inductive fun : accepts -> Prop :=
  | fn1 : fun True
  | fn2 : forall (n : nat )(A : accepts), fun A -> fun (n A).

我需要证明的是：

Lemma lem_1  (A : formula) (n : nat) (h : fun (n A)) : fun A.

当然，在开始我得到的证明时

 A : accepts
 n : nat
 h : fun (n A)
 ============================
 fun A

我花了很长时间阅读有关战术的文章，试图找到某种方法可以将 h 插入我的 fn2 或类似的东西，但我就是找不到方法。有人可以在这里指导我并给我一些想法吗？我也尝试过将有趣的 A 简化为 A，但我也没有成功。非常感谢您的帮助！

score 1 · Accepted Answer

您似乎想争辩说您的h假设是使用该fn2规则产生的。在 Coq 行话中，这需要反转该假设。为此，您可以调用inversion h. 应用是相反的过程：将规则与状态为推导fn2的假设结合起来。fun Afun (n A)

1 回答 1