在Coq中证明终止 [英] Proving Termination in Coq

问题描述

如何证明size_prgm的终止?我曾尝试过，但无法提出一个建立良好的关系以传递给Fix.

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.

推荐答案

终止oracle比以前好得多.使用fold_left定义函数sum_with并将其递归调用size_prgm馈入该函数，效果很好.

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.

这篇关于在Coq中证明终止的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！