The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi,



I am stumbling about behavior of Coq’s termination checker that I
cannot explain to myself. Consider:

Require Import Coq.Lists.List.

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

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

Instance list_C  {a} `{C a} : C (list a) := { P := list_P }.

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

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

(* Works *)
Fixpoint tree_P1 {a} `{C a} (t : tree a) : bool :=
    let tree_C := Build_C _ tree_P1 in
    let list_C := Build_C _ list_P in (* Question 1: Why is this line needed 
*)
    match t with Node _ x ts => orb (P x) (P ts) end.

Instance tree_C  {a} `{C a} : C (tree a) := { P := tree_P1 }.

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

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

(* And hence, this (identical?) code does not work *)
Fixpoint tree_P4 {a} `{C a} (t : tree a) : bool :=
    let tree_C := Build_C _ tree_P4 in
    match t with Node _ x ts => orb (P x) (P ts) end.

The first and second example show that, when trying to understand
whether a fixpoint is terminating, Coq is able to resolve record
accessors, basically evaluating what we wrote in tree_P1 to what we
wrote in tree_P2.

But this seems to only work if the record is built locally (let tree_C
:=…), not if it is defined using Definition.

But Fixpoint can look through other definitions just fine, e.g. through
list_P. So what is special about records, and can I make Coq accept
tree_P3 and tree_P4?


Thanks,
Joachim


-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part