The Coq mailing list

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

Hi,

Am Freitag, den 03.11.2017, 15:01 +0100 schrieb William J. Bowman:
> I agree with Tej that the problems in your code appear to result from
> scope and type classes, but I want to point out something about the
> termination checker some find surprising.

Not sure what you mean with scope, but here is the example again,
devoid of any type classes:

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.

Definition tree_C  {a} {a_C : C a} : C (tree a) := {| P := tree_P1 a_C |}.

(* 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.


Again, note that the difference between tree_P2 and tree_P3 is that I
replaced (list_P tree_C) with (P (list_C tree_C)), which should be the
same, shouldn’t they?

(Sorry for the confusion introduced because of type classes…)

> The Coq termination checker normalizes the body of a recursive
> function *before* checking that it terminates. 

Right, I noticed. And I am trying to use this fact here, expecting it
to reduce (P (list_C tree_C)) to (list_P tree_C).

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

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