Rcoq模拟题
组1
一、 系统指令
Q1. 在 Rocq 中，命令 Check (negb true). 的主要作用是？
A. 计算出该表达式的结果为 false。
B. 查看该表达式的类型，结果显示为 bool。
C. 检查 negb 这个函数是否存在于当前库中。
D. 打印出 negb 函数的源代码。
答案：B。解析：
Check只看类型，不求值。
Q2. 若要将表达式 1 + 2 彻底简化并输出结果 3，应使用的语句是？
A. Check 1 + 2.
B. Compute 1 + 2.
C. Locate 1 + 2.
D. Print 1 + 2.
答案：B。解析：
Compute是计算（归约）求值的指令。
Q3. 命令 Search (0 + _ = _). 的作用是？
A. 定义一个名为 Search 的加法函数。
B. 寻找当前库中所有符合“0加某数等于某数”模式的定理。
C. 检查 0 是否属于自然数集合。
D. 彻底化简目标中的加法运算。
答案：B。解析：
Search用于搜索库中已有的定理。
二、 关键字定义
Q4. 下列关于关键字 Inductive 的描述，哪项是最准确的？
A. 它是用来定义递归函数，必须保证能够终止。
B. 它是用来定义归纳数据类型（如枚举、链表等），并给出其构造器。
C. 它是用来声明一个局部的逻辑假设，只在 Section 内有效。
D. 它是用来将目标中的一个符号替换为另一个符号。
答案：B。解析：
Inductive用于定义数据类型及其构造器（Constructor）。
Q5. 语句 Fixpoint factorial (n:nat) := ... 相比于 Definition，其特殊之处在于？
A. 它定义的函数是全局可见的。
B. 它定义的函数允许进行自我调用（递归）。
C. 它定义的函数只能处理布尔值。
D. 它定义的函数必须返回一个 Prop 类型的值。
答案：B。解析：
Fixpoint专门用于定义递归。
Q6. 在 Section 内部使用 Variable n : nat. 声明的变量，其特点是？
A. 它是全局公理，在所有文件中都生效。
B. 它是一个递归函数。
C. 它的作用域仅限于当前的 Section 块，离开后即失效。
D. 它是 Notation 的另一种写法。
答案：C。解析：
Variable是局部声明。
三、 证明策略
Q7. 当目标 (Goal) 是 forall b : bool, b = negb (negb b) 时，最合适的起始策略是？
A. reflexivity.
B. simpl.
C. intros b.
D. split.
答案：C。解析：目标有
forall，先用intros。
Q8. 紧接上题，当假设区有了 b : bool，目标是 b = negb (negb b)，下一步该做什么？
A. reflexivity. (因为此时还没化简，两边不相等)
B. destruct b. (因为 b 是布尔值，需要分 true/false 两种情况讨论)
C. apply b. (b 只是个变量，不是定理)
D. rewrite b.
答案：B。解析：对于归纳类型变量（nat/bool），常用
destruct分类讨论。
Q9. 策略 simpl. 在证明过程中的主要作用是？
A. 引入一个新的前提条件。
B. 执行定义好的函数逻辑进行化简（如展开 match 和递归）。
C. 证明左右两边完全相等的等式。
D. 撤销上一步操作。
答案：B。解析：
simpl就是简化目标。
Q10. 如果目标是 A /\ B（合取命题），你应该使用哪个策略？
A. left.
B. right.
C. split.
D. exists.
答案：C。解析：
split拆分“且”；left/right用于“或” (\/)。
Q11. 语句 rewrite <- H. 的含义是？
A. 将目标中所有出现的 H 的右端项替换为左端项。
B. 将假设 H 从上下文中删掉。
C. 证明目标 H 与当前假设一致。
D. 声明 H 是一个递归定义的函数。
答案：A。解析：
<-代表从右往左替换。
四、 核心理论
Q12. 在 Rocq 的归约规则中，处理“函数应用（将参数带入函数体）”的规则名称是？
A. $\delta$ (delta) 归约
B. $\beta$ (beta) 归约
C. $\iota$ (iota) 归约
D. $\zeta$ (zeta) 归约
答案：B。解析：Beta 归约是最基础的函数调用归约。
Q13. 关于 Prop 和 Set 的区别，下列说法正确的是？
A. Prop 用于描述数据类型，Set 用于描述逻辑命题。
B. Prop 用于逻辑证明，Set 用于程序和数据。
C. 两者完全相同，只是名字不一样。
D. Set 里的东西不能通过 Check 查看。
答案：B。解析：
Prop是逻辑世界，Set是计算世界。
Q14. 依据 Curry-Howard 同构，一个“证明项”对应于程序设计中的？
A. 变量名
B. 一个程序（Lambda 项/函数体）
C. 编译器错误信息
D. 程序的注释
答案：B。解析：证明即程序，命题即类型。
五、 语句辨析
Q15. 语句 Lemma test : forall n, n + 0 = n. Proof. intros. auto. Qed. 中 Qed. 的作用是？
A. 标志证明的开始。
B. 暂时跳过该证明，标记为黄色。
C. 标志证明的圆满结束，并验证证明项的正确性，将其存入环境。
D. 定义一个名为 Qed 的函数。
答案：C。解析：
Qed是 Proof 结束的标志。
组2
一、 命令与输出
Q1：执行语句 Check (plus 1 1). 系统会输出什么？
A. 2 : nat
B. plus 1 1 : nat
C. nat : Prop
D. plus 1 1 : Prop
答案：B。解析：
Check只看类型（nat），不进行计算，所以不会变成 2。
Q2：如果你想在 Rocq 中看到函数 negb 的具体逻辑（源代码），你应该使用哪条语句？
A. Check negb.
B. Compute negb.
C. Print negb.
D. Search negb.
答案：C。解析：
二、 关键字含义
Q3：语句 Fixpoint mult (n m : nat) : nat := ... 的含义是？
A. 定义一个名为 mult 的全局常量。
B. 声明一个名为 mult 的逻辑公理。
C. 定义一个名为 mult 的递归函数。
D. 定义一个名为 mult 的归纳数据类型。
答案：C。解析：
Fixpoint是递归函数的专属关键字。
Q4：语句 Inductive bool : Set := true | false. 的含义是？
A. 定义一个递归函数 bool，包含两个参数。
B. 定义一个名为 bool 的归纳数据类型，它有两个构造器。
C. 证明 bool 是一个命题，其值为 true 或 false。
D. 声明一个全局变量 bool，初始值为 true。
答案：B。解析：
Inductive用于定义类型，“|”分隔的是它的构造器。
Q5：语句 Notation "x + y" := (plus x y). 的意思是？
A. 强制将所有 x 替换为 y。
B. 定义加号为 plus 函数的简写（记法）。
C. 证明 x+y 等于 plus x y。
D. 声明一个名为 Notation 的函数。
答案：B。解析：
Notation就是给已有的定义起一个好听的符号名（语法糖）。
三、 证明策略选择
Q6：当前目标 (Goal) 是 forall x y : nat, x + y = y + x，第一步操作最合适的是？
A. reflexivity.
B. simpl.
C. rewrite.
D. intros x y.
答案：D。解析：看到
forall或->，最基本的起手式就是intros。
Q7：当前目标 (Goal) 是 S (S O) = 2，此时执行哪条指令能直接完成证明？
A. intros.
B. destruct.
C. reflexivity.
D. split.
答案：C。解析：
S (S O)内部就是 2，左右相等，用自反性reflexivity。
Q8：假设区有 H: x = y，目标是 x + 1 = y + 1，应使用哪条指令？
A. apply H.
B. rewrite H.
C. destruct H.
D. simpl H.
答案：B。解析：利用已知等式进行替换，用
rewrite。
四、 综合
Q9：关于语句 Admitted. 的说法正确的是？
A. 它表示证明已经完美结束，可以保存。
B. 它表示放弃当前证明，系统会假设该命题成立并允许继续。
C. 它会执行所有的计算并将结果存入内存。
D. 它必须出现在 Inductive 定义的结尾。
答案：B。解析：
Admitted是“承认、承认”的意思，即跳过证明（黄色标记）。
Q10：在语句 rewrite <- H. 中，符号 <- 的含义是？
A. 将目标中与 H 结论相反的部分删掉。
B. 利用等式 H，将目标中的右边部分替换为左边部分。
C. 利用等式 H，将目标中的左边部分替换为右边部分。
D. 表示 H 是一个递归定义的假设。
答案：B。解析：默认
rewrite H是左换右，加了<-就是右换左。
- 指令类：求值选
Compute，求类型选Check，看源码选Print。 - 关键字类：递归选
Fixpoint，定义类型选Inductive，普通定义选Definition。 - 策略类：
- 看到
forall/->$\rightarrow$intros - 看到
bool/nat变量 $\rightarrow$destruct - 看到等式替换 $\rightarrow$
rewrite - 最后一步（左右相等）$\rightarrow$
reflexivity - 目标是
A /\ B$\rightarrow$split
- 看到
- 逻辑类：全称量词是
forall，存在量词是exists。
