如何正式确定Coq中术语缩减关系的终止？

Question

我有一个术语重写系统(A,→),其中A是一个集合,在A上是一个中缀二元关系.给定A的x和y,x→y表示x减少到y.

为了实现某些属性,我只是用来自定义Coq.Relations.Relation_Definitions和Coq.Relations.Relation_Operators.

现在我要形式化以下属性:

• →正在终止,即:没有无限下行链a0→a1→......

我怎样才能在Coq中实现这一目标？

Answer 1

显示重写关系终止与显示它是有充分根据的相同.这可以使用Coq中的归纳谓词进行编码:

Inductive Acc {A} (R : A -> A -> Prop) (x: A) : Prop :=
  Acc_intro : (forall y:A, R x y -> Acc R y) -> Acc R x.

Definition well_founded {A} (R : A -> A -> Prop) :=
  forall a:A, Acc R a.

(这个定义基本上与标准库中的谓词Acc和well_founded谓词相同,但我改变了关系的顺序以匹配重写系统中使用的约定.)

给定类型A和关系R上A,Acc R x意味着每个序列R从开始减少x : A正在终止; 因此,well_founded R意味着从任何一点开始的每个序列都在终止.(Acc代表"可访问".)

可能不太清楚为什么这个定义有效; 首先,我们怎样才能表明Acc R x对任何事物的持有x？请注意,如果x一个元素没有减少(也就是说,R x y任何元素永远不会持有y),那么这个前提很Acc_intro平常,我们可以得出结论Acc R x.例如,这将允许我们展示Acc gt 0.如果R确实有充分根据,那么我们可以从这些基本案例中倒退,并得出结论,其他元素A是可访问的.正确性的正式证明比这更复杂,因为它必须为每个人一般地工作x,但这至少表明我们如何能够显示每个元素可以单独访问.

好吧,也许我们可以证明这一点Acc R x.那我们怎么用呢？使用Coq生成的归纳和递归原则Acc; 例如:

Acc_ind : forall A (R : A -> A -> Prop) (P : A -> Prop),
   (forall x : A, (forall y : A, R x y -> P y) -> P x) ->
   forall x : A, Acc R x -> P x

如果R有充分理由,这只是有根据的归纳原则.我们可以解释如下.假设我们可以在使用诱导假设的同时显示P x持有量x : A,该假设表示随时P y都有R x y.(根据其含义R,这可能意味着x步骤y,或y严格小于x等等)然后,P x适用于任何x此类Acc R x.有根据的递归类似地工作,并且直观地表示如果对"较小"元素执行每个递归调用,则递归定义是有效的.

Adam Chlipala的CPDT有一章关于一般递归,对这种材料有更全面的报道.