Info 白话命令如何工作？

Question

假设我有以下简单的引理，我想获得关于 split 的信息。

Lemma and_prop : forall (P : Prop) (Q : Prop),
  P -> Q -> P /\ Q.
Proof.
  intros P Q HP HQ. 
  Info 100 split.

输出

simple refine ?X10@{__:=P; __:=Q; __:=HP; __:=HQ}

有人可以解释一下这是什么意思以及为什么我需要一个自然数作为信息吗？

Answer 1

你link到the documentation of Info在你的问题的评论中，但不要说手册有什么令人困惑的地方：

The number natural is the unfolding level of tactics in the trace. At level 0, the trace contains a sequence of tactics in the actual script, at level 1, the trace will be the concatenation of the traces of these tactics, etc…

Info 白话对于内置策略（例如 split）不是很有用，它们是在 OCaml 插件中实现的，因此实际上没有 Ltac 跟踪。对于像 apply 这样的策略，它的用处甚至更少，它仍然使用遗留的 OCaml 策略接口：Info 1 apply conj on 什么都不发出（我刚才将其报告为 bug #15223 just now). Unfortunately, split and constructor suffer from the same problem of not telling the user what constructor was applied; I've reported this as bug #15224。

也就是说，simple refine 是战术的基本原始组成部分。它是 the refine tactic 的变体，允许用户部分填写证明项。这只是说您正在使用 evar ?X10 部分填充证明项，其中四个未命名的上下文变量填充有 P、Q、HP 和HQ。这在这里不是很有用，但这里有一些更有用的输出 Info:

Lemma and_prop : forall (P : Prop) (Q : Prop),
  P -> Q -> P /\ Q.
Proof.
  Info 2 refine (fun P Q => _).
  (* simple refine fun P Q : Prop => ?X4@{__:=P; __:=Q};simple refine ?X5@{__:=P; __:=Q};shelve_unifiable *)

这里比较有趣的是simple refine fun P Q : Prop => ?X4@{...}，在这里你可以看到我输入的函数。

在下文中，您可以看到每个额外的信息级别如何剥离一层战术间接，以及最终级别如何显示单独的 simple refines 来引入每个变量：

Ltac split' := split.
Ltac split'' := split'.
Ltac split''' := split''.

Lemma and_prop : forall (P : Prop) (Q : Prop),
  P -> Q -> P /\ Q.
Proof.
  Info 0 split'''. (* split''' *) Undo.
  Info 1 split'''. (* split'' *) Undo.
  Info 2 split'''. (* split' *) Undo.
  Info 3 split'''. (* split *) Undo.
  Info 4 split'''. (* <ltac_plugin::split@0> *) Undo.
  Info 5 split'''. (* <ltac_plugin::split@0>simple refine ?X2;simple refine fun P : Prop => ?X3@{__:=P};
simple refine fun Q : Prop => ?X4@{__:=P; __:=Q};
simple refine fun H : P => ?X5@{__:=P; __:=Q; __:=H};simple refine fun H0 : Q => ?X6@{__:=P; __:=Q; __:=H; __:=H0} *) Undo.

Info 白话命令如何工作？

How does the Info vernacular command work?

coq