The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I saw this on Stack Exchange and started looking into it. Your first question really surprised me - it appears you have dead code that helps the termination checker. What’s going on in that the let-bound list_C (I’ll call it list_C’ to avoid confusion with the definition it shadows) is used for typeclass instantiation rather than the global instance. Here’s a demonstration (note that I personally started with Set Typeclasses Debug, but you can see the impact of typeclass resolution by looking at the terms before the termination checker runs):

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 }.

Opaque list_C.

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

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

Set Printing All.

Fixpoint tree_P1' {a} `{C a} (t : tree a) {struct t} : bool.
Proof.
  set (tree_C := Build_C _ (tree_P1' _ _)).
  refine (match t with Node _ x ts => orb (P x) (P ts) end).
  Show Proof.
  Fail Guarded.
Abort.

(* Works *)
Fixpoint tree_P1'' {a} `{C a} (t : tree a) {struct t} : bool.
Proof.
  set (tree_C := Build_C _ (tree_P1'' _ _)).
  set (list_C' := Build_C _ list_P).
  refine (match t with Node _ x ts => orb (P x) (P ts) end).
  Show Proof.
  (* note that list_C' is the argument to P this time *)
Defined.

So in tree_P2 it’s not evaluation but instead typeclass resolution not actually using the global list_C.

​

On Fri, Nov 3, 2017 at 9:27 AM, Joachim Breitner <mail AT joachim-breitner.de> wrote:

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/