What do the consecutive in's in Coq do and eval & red & Idtac do?

Question

I know in OCaml the syntax

let x = val in exp

means x has the value v when in expression exp.

But what does something like

let add_left_red := eval red in add_left in  (* reduce add_left, but leave goal alone *)
  idtac add_left_red.

I assume it does this:

• gives the identifier add_left_red the output of eval red
• then that add_left_red is that value in add_left
• AND in idtac add_left_red

Is that what it does?

---

Fyi I also have no idea what that line does. Especially cuz googling eval and red gave nothing useful.

Idtac did see:

Tacticidtac  ident  ​   string  ​   natural *
Leaves the proof unchanged and prints the given tokens. Strings and naturals are printed literally. If ident is an Ltac variable, its contents are printed; if not, it is an error.

What do those composoble blocks do?

---

Context whole script

Fixpoint add_left (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (add_left p m)
  end.
  
Lemma demo_1 :
  forall (n : nat),
    add_left n O = n.
Proof.
  intros.                                     (* goal : add_left n O = n *)  
  let add_left_red := eval red in add_left in (* reduce add_left, but leave goal alone *)
  idtac add_left_red.                         (* print the result *)
  (* Print eval. gives error *) 
  Print red.
  Print add_left_red.
  admit.
Abort.

Answer 1

In OCaml, there is only one notion of computation, but in Coq, we may want to play with several such notions, because we sometimes want to compute or simplify only progressively the expressions we are looking at.

So there is a command, akin to Compute which makes it possible to take a term, and compute it only partially. This command as an in keyword in the middle.

Here is an example:

Require Import Arith.
Eval cbn[fact] in fact 10.

Here the result shows the computation of fact 10, but only insofar that the multiplications it performs are exposed, but not computed themselves.

Sometimes, in a tactic you want to do just this computation, so will need to use a variant of this eval ... in ... construct (this time with a lower case initial), which is designed for use in tactics.

let x := eval cbn[fact] in (fact 10) in change (fact 10) with x.

So in your goal, fact 10 is replaced by (10 * 9 ...)

if it were in OCaml, you would not bother explaining that you want a partial computation so you would write only let x = fact 10 in ... .

So this is the reason why the keyword appears twice. The first time to separate the computation mechanism you want to apply to the expression, and the second time to separate the expression that is evaluated from the expression where the variable will be used.

Here is an example where the tactic is being used:

Require Import Arith.
Lemma toto : fact 7 = 5040.
let x := eval cbn[fact] in (fact 7) in change (fact 7) with x.

(tested with coq-8.14)

Answer 2

Understanding the realted Eval RED in Term is key. Do that first.

• eval: ref: What do the consecutive in's in Coq do and eval & red & Idtac do?

I think its 
eval RED in TERM

Example:

  Require Import Arith.
  Lemma toto : fact 3 = 6.
  let x :=    (*set the output of eval RED in TERM to id/var x*)
  (eval cbn[fact] in (fact 3))  (* partially reduce fact 3 *)
  in (* output of "let x := (eval RED in TERM)" goes here *)
  idtac x. (* final expression to evaluate with x *)

  (3 * (2 * (1 * 1)))