0

我是 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,但我也没有成功。非常感谢您的帮助!

4

1 回答 1

1

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

于 2016-03-10T21:22:21.883 回答