The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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