Coq中的连续in和eval&amp；red&amp；Idtac做了什么？ [英] What do the consecutive in's in Coq do and eval & red & Idtac do?

问题描述

我知道OCaml中的语法

let x = val in exp

表示x在表达式exp中具有值v。

但像

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

我假设它是这样做的：

• 为add_left_red提供eval red
的输出
• 那么add_left_red就是add_left
中的值
• 和idtac add_left_red

这就是它的作用吗？

---

仅供参考，我也不知道这行是什么意思。尤其是因为搜索eval和red没有给出任何有用的信息。

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.

这些可合成的块是做什么的？

---

上下文整个脚本

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.

推荐答案

在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被替换为(10*9...)

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

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

以下是使用该策略的一个示例：

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

这篇关于Coq中的连续in和eval&amp；red&amp；Idtac做了什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！