在Coq中證明終止

如何證明終止爲size_prgm？我嘗試過，但不能拿出一個良好的關係傳遞給Fix。在Coq中證明終止

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.

來源

2013-10-22 Konstantin Weitz

簡短的回答，因爲我沒有太多的時間，現在（我會稍後嘗試重新回到你）：這是每一個勒柯克用戶有一個非常常用的（和愚蠢的）問題體驗一天。

如果我沒有記錯，這個問題有兩個「通用」解決方案，還有很多非常具體的問題。對於前者：

建立一個內在的固定點：我真的不記得如何正確地做到這一點。

使用相互遞歸類型：您的代碼的問題是您在Stmt類型中使用list 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-22 07:36:23 Vinz

終止甲骨文是比它曾經是相當好。使用fold_left定義函數sum_with並將其遞歸調用size_prgm可以很好地工作。

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-22 11:55:25 gallais

在Coq中證明終止

回答

相關問題