The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

The certicoq project (https://www.cs.princeton.edu/~appel/certicoq/)
has recently been discussing what "evaluation" should mean for Coq
programs (including programs with axioms).  I noticed the following
Coq behavior that surprised me.  I apologize for the long email, which
I attempt to make self contained.  Consider the program [demo]

   Definition bb := bool.
   Definition demo (t:True) : bb := match t with I => true end.

To look beneath Print form, I use Malecha's quoting plugin,
template-coq (https://github.com/gmalecha/template-coq/tree/coq-8.5).
First quote the program

   Quote Recursively Definition p_demo := demo.
   Print p_demo.

p_demo =
PType "Coq.Init.Logic.True"
  (("True", {| ctors := ("I", tRel 0, 0) :: nil |}) :: nil)
  (PType "Coq.Init.Datatypes.bool"
     (("bool",
      {| ctors := ("true", tRel 0, 0) :: ("false", tRel 0, 0) :: nil |})
      :: nil)
     (PConstr "Top.bb" (tInd (mkInd "Coq.Init.Datatypes.bool" 0))
        (PConstr "Top.demo"
           (tLambda (nNamed "t") (tInd (mkInd "Coq.Init.Logic.True" 0))
              (tCase 0
                 (tLambda (nNamed "t")
            (tInd (mkInd "Coq.Init.Logic.True" 0))
                    (tConst "Top.bb")) (tRel 0)
                 ((0, tConstruct (mkInd "Coq.Init.Datatypes.bool" 0) 0)
                  :: nil))) (PIn (tConst "Top.demo")))))
     : program

This quotes everything in the Coq context that is hereditarily used in
the toplevel program.  The toplevel program (item "PIn") is just the
defined constant (tConst "Top.demo").  The definiens of "Top.demo"
(bound in the quoted context as 'PConstr "Top.demo"') is

        (tLambda (nNamed "t") (tInd (mkInd "Coq.Init.Logic.True" 0))
           (tCase 0
              (tLambda (nNamed "t")
         (tInd (mkInd "Coq.Init.Logic.True" 0))
                 (tConst "Top.bb")) (tRel 0)
              ((0, tConstruct (mkInd "Coq.Init.Datatypes.bool" 0) 0)
               :: nil)))

Notice the defined constant (tConst "Top.bb") under a lambda in the
mechanically generated return predicate of the Case statement.

Now we quote the cbv evaluated program

   Quote Definition qcbv_demo := Eval cbv in demo.
   Print qcbv_demo.

qcbv_demo =
tLambda (nNamed "t") (tInd (mkInd "Coq.Init.Logic.True" 0))
  (tCase 0
     (tLambda (nNamed "t")
        (tInd (mkInd "Coq.Init.Logic.True" 0))
        (tInd (mkInd "Coq.Init.Datatypes.bool" 0)))
     (tRel 0)
     ((0, tConstruct (mkInd "Coq.Init.Datatypes.bool" 0) 0) :: nil))
     : term

The instance of (tConst "Top.bb") under a lambda has been unfolded to
its definiens, (tInd (mkInd "Coq.Init.Datatypes.bool" 0)).

This is not the behavior I expect for Eval cbv.  What is the
specification of cbv for Coq?

Best,
Randy