Coq Qed策略得到挂起

-1

我证明了一个引理（Proof completed），但是当我使用Qed保存它时，系统变得忙碌。在同一个文件中，除了这个之外，还有其他类似的引理，其中Qed执行正常。任何机构都可以教我解决方案吗？Coq Qed策略得到挂起

感谢，

Wilayat

2013-02-18 Khan

你能提供错误代码吗？ – Ptival 2013-02-18 15:52:11

很难在不知道具体的例子你工作的话。每当你在Coq中键入Qed时，内核将分析你的策略产生的证据并确保它实际上是有效的;战术引擎本身实际上不执行许多检查。因此，尽管您的问题证明与其他问题稍有不同，但可能会导致它产生一个非常大的证明术语，这会使内核花费很长时间。

来源

2013-03-08 02:42:46

@Ptival这是产生错误的代码。我现在修复它。我仍然不明白这个问题。如果两条线都没有评论，那么在战术结束后，直觉。“，证明完成，但'Qed'被绞死。 '引理vis_handle ：全部文章， top_label <？= 1 = true - > （wrq，oel）= handle_w wr pr u b - > List.filter（vis_oe_b l）oel == oel。 o证明。介绍。（* 在H0中展开handle_w。展开在H0中的open_w *）反转H0。简单*。重写 - > H; SIMPL。展开url_label; SIMPL。 * *; * * * * * * * * * * * * * *毁坏你;简化在* ... destruct p;直觉。 QED。 ' – Khan 2013-03-09 09:59:21

Coq Qed策略得到挂起

回答

相关问题