证明一系列步骤终止答案

【问题标题】：Prove that a sequence of steps terminates证明一系列步骤终止
【发布时间】：2016-12-15 10:41:33
【问题描述】：

我有一个重写 lambda 项的小系统。它具有通常的（三个）确定性按值调用重写规则。我没有在这里列出它们。

重写被建模为Steps，从一个Term 到另一个。我也有 reachable 术语之间的StarStep 关系，后者可以通过零个或多个重写步骤从第一个生成。

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

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

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

【问题讨论】：

请注意，您可以在 collacoq 文件的开头Comments "pkgs: coq-reals".，它会加载更多的 Coq 库，因此您不必重新实现字符串。

标签： coq lambda-calculus

【解决方案1】：

我相信这是经典推理的一个例子。该陈述类似于以下命题，在建设性设置中无法证明：

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.

【讨论】：