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