coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] cbv Manual Clarification

From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] cbv Manual Clarification
Date: Thu, 23 Feb 2012 14:06:51 -0500
Authentication-results: mr.google.com; spf=pass (google.com: domain of gmalecha AT eecs.harvard.edu designates 10.182.75.102 as permitted sender) smtp.mail=gmalecha AT eecs.harvard.edu

Hello --

The Coq manual (http://coq.inria.fr/doc/Reference-Manual011.html#@tactic59) states the following:

The goal may be normalized with two strategies: lazy (lazy tactic), or call-by-value (cbv tactic). ...

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).

This doesn't seem to be accurate. Consider:

Goal (fun x => 2 + x) = (fun y => 2 + y).

(**

============================

(fun x : nat => 2 + x) = (fun y : nat => 2 + y)

**)

cbv.

(**

   ============================

   (fun x : nat => S (S x)) = (fun y : nat => S (S y))

**)

Doesn't this constitute "reduction under the lambda-abstractions"? Based on the manual I would expect [cbv] to do nothing. Is there any tactic that actually implements call-by-value as described in the manual?

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

[Coq-Club] cbv Manual Clarification, Gregory Malecha