代码之家 › 专栏 › 技术社区 › krokodil

归纳型与NaT上的相互递归

termination coq recursion

2

krokodil · 技术社区 · 6 年前

考虑这个例子:

Inductive T :=
| foo : T
| bar : nat -> T -> T.

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => evalBar x n
  end
with evalBar (x:T) (n:nat) {struct n} : nat :=
  match n with
  | O => 0
  | S n' => (evalT x) + (evalBar x n')
  end.

COQ以错误拒绝: 递归调用evalbar的主参数等于“n”而不是“x” .

我知道终端检查程序被两种不相关的归纳类型(t和nat)混淆了。但是,我试图定义的函数似乎确实会终止。我怎样才能让COQ接受它?

2 回复 | 直到 6 年前

1

eponier 6 年前

另一种解决方案是使用嵌套的固定点。

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => let fix evalBar n {struct n} :=
                 match n with
                 | 0 => 0
                 | S n' => Nat.add (evalT x) (evalBar n')
                 end
               in evalBar n
  end.

重要的一点是去掉这个论点 x 从 evalBar . 因此递归调用 evalT 在上完成 X 从 bar n x ,而不是 X 作为论点给予 评估 因此,终端检查程序可以验证 埃瓦特 .

这是使版本 nat_rec 在另一个回答工作中提出。

2

1

krokodil 6 年前

我发现的一个解决方案是 nat_rec 而不是 evalBar :

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => @nat_rec _ 0 (fun n' t' => (evalT x) + t') n
  end.

它能用,但我希望我能藏起来 自然采收 在下面 评估 要隐藏详细信息的定义。在我的实际项目中,这种构造被多次使用。