证明一系列步骤终止

我有一个可以重写lambda术语的小系统。它具有通常的（三个）确定性按值重写规则。我没有在这里列出。证明一系列步骤终止

重写模拟为Step从一个Term到另一个。我也有可达项之间的关系，其中后者可以由第一个零或更多重写步骤产生。

我现在想表明重写终止（带有值或卡住）。我已经删除了细节，因为我不认为他们在这里重要，但如果需要，我可以添加更多细节。

这里是（在浏览器中或here CollaCoq）代码：

Variable Term: Type. 
Variable Step: Term -> Term -> Prop. 
Inductive StarStep: Term -> Term -> Prop := 
| StepNone : forall t, StarStep t t 
| StepOne : forall t t', Step t t' -> forall t'', StarStep t' t'' -> StarStep t t''. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''.

所以，我想告诉

如果不是那“从所有到达的情况下，说明有可能又一步“那么存在可从t 到达的状态t'，使得它是不可能从中走出来的。

我被困在如何继续。我是否需要更多的信息，例如诱导或破坏（=个案分析）t？当它被否定时，我该如何使用假设中的信息？

编辑：Here are more details about Term and Step

来源

2016-12-15 larsr

注意，您可以'评论“PKGS：COQ-雷亚尔” .'你collacoq文件的开头，它将让你不加载更多勒柯克库必须重新实现字符串。 – ejgallego

我相信这是经典推理的一个实例。声明类似于下面的命题，这是不是在建设性的设置可证：

Goal forall (A : Type) (P : A -> Prop), 
    ~ (forall x, P x) -> exists x, ~ P x.

，因为知识，“这是不正确的，FORALL ...”不会产生一个对象，你需要证明一些东西的存在。

下面是使用经典逻辑的法律可能的解决方案：

Require Import Coq.Logic.Classical_Pred_Type. 
Require Import Coq.Logic.Classical_Prop. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''. 
Proof. 
    intros t H. 
    apply not_all_ex_not in H. 
    destruct H as [tt H]. 
    apply imply_to_and in H. 
    firstorder. 
Qed.

事实上，我们甚至不需要知道StarStep什么，因为以前的命题以下抽象的版本是经典有效逻辑（证明保持不变）：

Goal forall (A : Type) (P Q : A -> Prop), 
    ~ (forall s, Q s -> exists t, P t) -> 
    exists s, Q s /\ forall t, ~ P t.

来源

2016-12-15 13:27:27

证明一系列步骤终止

回答

相关问题