いつ終了チェッカーがレコードアクセッサを減らすのですか

Question

私は自分自身に説明できないCoqの終了チェッカーの動作につまづいています。考えてみましょう：

Require Import Coq.Lists.List. 

Record C a := { P : a -> bool }. 

Arguments P {_}. 

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C). 

Definition list_C {a} (a_C : C a) : C (list a) := {| P := list_P a_C |}. 

(* Note that *) 
Eval cbn in  fun a C => (P (list_C C)). 
(* evaluates to: fun a C => list_P C *) 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works, using a local record *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P1 a_C) in 
    let list_C' := Build_C _ (list_P tree_C) in 
    match t with Node _ x ts => orb (P a_C x) (P list_C' ts) end. 

(* Works too, using list_P directly *) 
Fixpoint tree_P2 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P2 a_C) in 
    match t with Node _ x ts => orb (P a_C x) (list_P tree_C ts) end. 

(* Does not work, using a globally defined record. Why not? *) 
Fixpoint tree_P3 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P3 a_C) in 
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end. 

第一及び第二の例不動点が終了しているかどうかを理解しようとしたときに、コックは基本的に、我々はtree_P2に書いたものにtree_P1に書いたものを評価し、記録アクセサを解決することができ、ことを示しています。

しかし、これは、レコードがローカルに構築されている場合（let tree_C :=…）、Definitionを使用して定義されている場合にのみ機能します。

しかし、Fixpointは他の定義を見ても問題ありません。 list_Pまでだから、レコードに関して特別なのは何ですか、私はCoqにtree_P3を受け入れることができますか？

Answer 1

Coqの中の終端チェッカーのいくつか読みになった後、私は解決策を見つけたと思います。そのため、tree_P1が機能します。必要に応じて

終了チェッカーはまた、それはなぜtree_P2作品である、（のようなlist_C'、P、existsb）と呼ばれている定義を展開します。

ただし、list_Cのように、match … with句に現れる定義は展開されません。ここではそのための最低限の例は次のとおりです。

(* works *) 
Fixpoint foo1 (n : nat) : nat := 
    let t := Some True in 
    match Some True with | Some True => 0 
         | None => foo1 n end. 

(* works *) 
Fixpoint foo2 (n : nat) : nat := 
    let t := Some True in 
    match t with | Some True => 0 
       | None => foo2 n end. 

(* does not work *) 
Definition t := Some True. 

Fixpoint foo3 (n : nat) : nat := 
    match t with | Some True => 0 
       | None => foo3 n end. 

元のコードのための回避策は、終了チェッカーがそれらを展開することを確実にするために、すべての定義が呼ばれる（とに対してパターン一致しない）されていることを確認することです。

Require Import Coq.Lists.List. 

Record C_dict a := { P' : a -> bool }. 

Definition C a : Type := forall r, (C_dict a -> r) -> r. 
Existing Class C. 

Definition P {a} {a_C : C a} : a -> bool := a_C _ (P' _). 

Definition list_P {a} `{C a} : list a -> bool := existsb P. 

Instance list_C {a} (a_C : C a) : C (list a) := 
    fun _ k => k {| P' := list_P |}. 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works now! *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C : C (tree a) := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in 
    match t with Node _ x ts => orb (P x) (P ts) end. 

：型クラスの解像度は、これらの問題のindepenentあるとして、

Require Import Coq.Lists.List. 

Record C_dict a := { P' : a -> bool }. 

Definition C a : Type := forall r, (C_dict a -> r) -> r. 

Definition P {a} (a_C : C a) : a -> bool := 
    a_C _ (P' _). 

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C). 

Definition list_C {a} (a_C : C a) : C (list a) := 
    fun _ k => k {| P' := list_P a_C |}. 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works now! *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in 
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end. 

これも型クラスで動作します。我々は継続渡しスタイルに切り替えることにより、それを行うことができます

Answer 2

質問1については、tree_P1では、クラスインスタンスの定義がfix構造内にあり、終了チェック時に減少していると考えています。

あなたが正しく指摘しているように、次の定義は拒否されます。この定義で

Fixpoint tree_P1' {a} `{C a} (t : tree a) : bool := 
    let tree_C := Build_C _ tree_P1' in 
    match t with Node _ x ts => orb (P x) (@P _ (* mark *) _ ts) end. 

は、コメント (* mark *)後に必要なクラスのインスタンスを使用すると、ライン7で持っている定義によって埋められる。しかし、この定義は fix構築体の外に住んでいると終端チェッカーによって削減されることはありません同じように。その結果、任意のツリー引数に適用されない tree_P1'の出現がコード内に残り、このオカレンスが最初の引数よりも小さい引数でのみ使用されると判断することはできません。

私たちは拒否されている関数の本体を見ることができないので、これは野生の推測です。

終了チェッカー常にローカル定義を展開し、ベータ削減します：