代码之家 › 专栏 › 技术社区 › Sara

如何在Coq中使用带有假设的策略?

coq-tactic coq

Sara · 技术社区 · 8 年前

我是新来考克的,我已经走到了死胡同。我有一个归纳定义,大致如下(我之前定义过归纳接受):

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

1 回复 | 直到 8 年前

Arthur Azevedo De Amorim 8 年前

看来你想说 h 假设是使用 fn2 规则用Coq的行话来说,这需要反转这个假设。为此,您可以致电 inversion h 。应用是相反的过程:将 第2页 假设规则 fun A 导出 fun (n A) .

推荐文章

Jian Wang · elim在Coq中是如何工作的?

7 年前

Lorenz · Coq强制和目标匹配

7 年前

Carl Patenaude Poulin · 证明共自然数的共归纳原理

7 年前

user285827 · 如何利用Coq中包含forall的假设?

7 年前

Carl Patenaude Poulin · 问:为什么我需要手动展开一个值,即使它上面有一个“提示展开”?

7 年前