When the completion controller reduces write access

Question

I stumble on Coqs completion check behavior, which I cannot explain to myself. Consider:

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. 

The first and second examples show that when trying to understand whether an endpoint ends, Coq can resolve the records, mainly evaluating what we wrote in tree_P1 what we wrote in tree_P2 .

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

But Fixpoint can look at other definitions perfectly, for example. through list_P . So, what is special about the entries, and can I get Coq to accept tree_P3 ?

Answer 1

After some reading of the completion check in Coq, I think I found a solution:

The completion controller will always disclose local definitions and beta reduction. This is why tree_P1 works.

The completion controller also expands the definitions that are called (for example, list_C' , P , existsb ) existsb , so tree_P2 works.

However, the term verification tester does not expand the definitions that are used in the match … with list_C , for example list_C . The following is a minimal example:

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

The source code workaround is to make sure all definitions are invoked (not matched against patterns) to ensure that the completion checker expands them. We can do this by switching to the style of continuing the passage:

 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. 

This even works with class types, since class class resolution is an integral of these problems:

 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. 

Answer 2

In question 1. I believe that in tree_P1 definition of the class instance is inside the fix construct and reduced during the completion check.

The following definition is rejected, as you indicate correctly.

 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. 

In this definition, an instance of the class is needed after the comment (* mark *) populated with the definition that you have on line 7. But this definition lives outside the fix construct and will not be reduced by checking completion in the same way. As a result, the rest of the tree_P1' will remain in the code, which does not apply to any tree-like argument, and the completion checker will not be able to determine that this entry is used only for arguments that are less than the initial argument.

This is a wild assumption because we cannot see the body of the rejected function.