The Coq mailing list

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

Hi,

Am Freitag, den 03.11.2017, 11:11 -0400 schrieb Joachim Breitner:
> Hi,
> 
> Am Freitag, den 03.11.2017, 16:00 +0100 schrieb William J. Bowman:
> > > On Nov 3, 2017, at 3:39 PM, Joachim Breitner 
> > > <mail AT joachim-breitner.de>
> > >  wrote:
> > > 
> > > Without δ, why does it unfold `list_P` and `existsb` to see that the
> > > recursion on the list is nicely structural? And why do tree_P1 and
> > > tree_P2 still work even when I specify Opaque list_P.?
> > 
> > I was about to conjecture exactly what you discovered; thank you for
> > digging into the source. And the question you pose is most
> > mysterious. Are some definitions treated differently than others?
> 
> there is more code in that file of interest:
> 
>         | Const (kn,u) ->
>             if evaluable_constant kn renv.env then
>               try List.iter (check_rec_call renv []) l
>               with (FixGuardError _ ) ->
>                 let value = (applist(constant_value renv.env (kn,u), l)) in
>                 check_rec_call renv stack value
>             else List.iter (check_rec_call renv []) l
> 
> so it looks like it unfolds constants on the fly, if it cannot prove
> termination without the unfolding and if they are evaluable. Great,
> that explains why it unfolds list_P and existsb. But why not P when
> applied to list_C? P certainly is not opaque.

I think I nailed it:

While the termination checker evaluates constants on demand, it only
does so when they are in head positions. In particular, it does not
evaluate the scrutinee of a match, as these examples show:

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


So the problem in my original example is not that it does not evaluate
P, but that it ends up with

  match list_C tree_C with …

and now it does not unfold list_C.


I wonder if I can work-around it by never defining a dictionary, but
only ever pass it to a continuation. And it does:


    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.


And this now also works with type classes:


    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.


I’m not yet sure if I want to apply this pattern of defining every
instance as a continuation in my actual development, but at least there
is a way forward.


Thanks for your help,
Joachim

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

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