coq - Coq 中的终止谓词

Question

考虑一个对评估关系建模的谓词。该关系将以真或假停止，这就是为什么我希望我的链的值是配置或布尔值：

Inductive compile_step :
  conf_type + bool -> conf_type + bool -> Prop

我知道评估终止，我想正式证明它。所以我定义了一个终止谓词：

Inductive terminating {A} (r: A -> A -> Prop) (c': A) :=
| TStep : (forall c1, r c' c1 -> terminating r c1) ->
          terminating r c'.

并尝试证明：

Lemma compiling_terminates (c': A):
  terminating compile_step c'.

现在，让我惊讶的是 Coq 变得疯狂。明智的做法是应用 TStep 并解决此目标：

(H) c' ⟹ c1 意味着终止 compile_step c1

这是问题开始的地方：

1. 反转 H：

错误：反转需要对排序集进行案例分析，这在归纳定义 compile_step 中是不允许的。

2. 破坏H：

错误：归纳定义 compile_step 不允许对排序集进行案例分析。

3. 感应 H：

错误：找不到消除组合器 compile_step_rec，可能不允许消除排序集上的归纳定义 compile_step。

错误会在层次结构的更深层次上重现。

对此有简单的解释吗？有简单的解决方案吗？

也许这对你们中的一些人来说是有用的。

标签： coq