The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

"Eval compute" or even "Eval cbv" do assume a set of default reduction rules to use, see the documentation in
  https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#sec391

In particular I think that both include not only beta-reduction by default, but also delta-reduction (unfolding of definition) which can go in depth under lambdas.

Using your example I have:

Set Printing All.

(* unfolds all definitions and reduces *)

Eval cbv in (id demo).
(*      = fun t : True => match t return bool with
                       | I => true
                       end *)

(* does not reduce as 'demo' is not a value *)

Eval cbv beta in (id demo).
(*      = @id (True -> bb) demo *)

(* unfolds definitions but not beta-reduction *)

Eval cbv delta in (id demo).
(*      = (fun (A : Type) (x : A) => x) (True -> bool)
         (fun t : True => match t return bool with
                          | I => true
                          end) *)

(* unfolds definition, except bb, beta-reduces *)

Eval cbv beta delta -[bb] in (id demo)
(*      = fun t : True => match t return bb with
                       | I => true
                       end *)

On Wed, Jan 13, 2016 at 9:26 AM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

I think the problem can already be shown without template-coq:

  Definition bb := bool.
  Definition demo (t:True) : bb := match t with I => true end.
  Print demo.
  (* fun t : True => match t return bb with
                         | I => true
                         end *)
  Eval compute in demo.
  (* fun t : True => match t return bool with
                         | I => true
                         end *)
  (* bb, which is under a lambda, became bool *)

The reference manual states:

  The call-by-value strategy is the one used in ML languages:
  the arguments of a function call are evaluated first, using
  a weak reduction (no reduction under the λ-abstractions).

So, if I understand that correctly, cbv should not reduce under lambdas and this is a bug in cbv.

On 01/13/2016 02:49 PM, Randy Pollack wrote:

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