The Coq mailing list

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

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.

It also does not help to reimplement P with an explicit match, i.e.:

    Definition P' {a} (a_C : C a) : a -> bool :=
      match a_C with Build_C _ P => P end.


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