Coq 中的连续 in 和 eval & 做什么？红&伊达克做吗？

Question

我知道在 OCaml 中，语法

let x = val in exp

意味着在表达式 exp 中，x 的值为 v。

但是像我假设的那样，

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

它会执行以下操作：

• 将 eval red 的输出提供给标识符 add_left_red
• ，然后 add_left_red 就是 中的值>add_left
• AND in idtac add_left_red

这就是它的作用吗？

---

仅供参考，我也不知道那条线是做什么的。特别是因为谷歌搜索 eval 和 red 没有提供任何有用的信息。

Idtac 确实看到了：

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.

那些可组合的是什么块吗？

---

上下文整个脚本

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

了解术语中的 Eval RED 是关键。首先这样做。

• 评估：参考：Coq 中的连续 in 做什么以及 eval & 做什么？红& Idtac 做什么？

I think its 
eval RED in TERM

示例：

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

Answer 2

在 OCaml 中，只有一种计算概念，但在 Coq 中，我们可能想要使用几种这样的概念，因为我们有时只想逐步计算或简化我们正在查看的表达式。

因此，有一个类似于Compute的命令，它可以获取一个术语，并仅部分计算它。这个命令作为一个 in 关键字在中间。

下面是一个例子：

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

这里的结果显示了事实 10 的计算，但仅限于它执行的乘法被公开，但本身并未计算。

有时，在某种策略中，您只想进行此计算，因此需要使用此 eval ... in ... 构造的变体（这次使用小写首字母），即设计用于战术。

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

因此，在您的目标中，如果事实 10 在 OCaml 中，则事实 10 会被 (10 * 9 ...) 替换

，您不会费心解释您想要部分计算，因此您只需在 中编写 let x = fact 10 。 .. .

所以这就是这个关键词出现两次的原因。第一次将要应用于表达式的计算机制分开，第二次将计算的表达式与将使用变量的表达式分开。

下面是使用该策略的示例：（

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

使用 coq-8.14 进行测试）