小编Bor*_* E.的帖子

我对术语有以下定义：

Inductive term : Type :=
  | Var : variable -> term
  | Func : function_symbol -> list term -> term.

一个函数，该函数pos_list获取术语列表并为每个子术语返回“位置”列表。例如，对于[Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]]我来说，应该知道[[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]]每个元素在子项的树层次结构中的位置。

Definition pos_list (args:list term) : list position :=
  let fix pos_list_aux ts is head :=
    let enumeration := enumerate ts in
      let fix post_enumeration ts is head :=
        match is with
        | [] => [] …

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

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

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

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

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