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策略得到掛起

回答

相關問題