2

How can I prove termination for size_prgm? I tried, but can't come up with a well founded relation to pass to Fix.

Inductive Stmt : Set :=
| assign: Stmt
| if': (list Stmt) -> (list Stmt) -> Stmt.

Fixpoint size_prgm (p: list Stmt) : nat := 
  match p with
  | nil  => 0
  | s::t => size_prgm t +
            match s with
            | assign  => 1
            | if' b0 b1 => S (size_prgm b0 + size_prgm b1)
            end
  end.
4

2 回答 2

3

The termination oracle is quite better than what it used to be. Defining a function sum_with using fold_left and feeding it the recursive call to size_prgm works perfectly well.

Require Import List.

Inductive Stmt : Set :=
| assign: Stmt
| if': (list Stmt) -> (list Stmt) -> Stmt.

Definition sum_with {A : Type} (f : A -> nat) (xs : list A) : nat :=
  fold_left (fun n a => n + f a) xs 0.

Fixpoint size_prgm (p: Stmt) : nat := 
  match p with
  | assign    => 1
  | if' b0 b1 => sum_with size_prgm b1 + sum_with size_prgm b0
end.
于 2013-10-22T11:55:25.877 回答
1

简短的回答，因为我现在没有太多时间（我稍后会回复你）：这是每个 Coq 用户每天都必须经历的一个非常常见的（也是愚蠢的）问题。

如果我没记错的话，这个问题有两个“通用”解决方案和许多非常具体的解决方案。对于前两个：

  1. 建立一个内部固定点：我真的不记得如何正确地做到这一点。

  2. 使用相互递归类型：你的代码的问题是你list Stmt在你的Stmt类型中使用，而 Coq 无法计算你想到的归纳原则。但你可以使用像

    Inductive Stmt : Set :=
  | assign : Stmt
  | if': list_Stmt -> list_Stmt -> Stmt
with list_Stmt : Set :=
  | Nil_Stmt : list_Stmt
  | Cons_Stmt : Stmt -> list_Stmt -> list_Stmt.

现在在此类型上编写您的函数，并在此类型和您的原始Stmt类型之间进行双射。

你可以尝试浏览 Coq-Club 邮件列表，这种话题是经常出现的。

希望对你有帮助，V

于 2013-10-22T07:36:23.950 回答