coq - “econstructor”的相反（？）命令是什么

Question

例如，

Lemma ex_1:
exists n, n=1.
Proof.

显示一个子目标：

exists n : nat, n = 1

econstructor 命令将目标更改为

?n = 1

可以得到什么命令

exists n : nat, n = 1

再次从“？n = 1”？

或者，假设我们为此证明了一些带有 (exists n, ~) 形式的 sublemma。我们如何“应用”这个sublemma？

标签： coq

Answer 1

Théo Winterhalter 给出了一些在这种情况下有效的策略，但总的来说，在某些意义上econstructor是不可逆的。

econstructor可以将两种不同的证明状态带到相同的最终状态。

也就是说，econstructor在证明状态上不是单射的。例如，考虑这种（相当愚蠢的）情况。

Inductive exists': Prop :=
| intro (n: nat): n = 1 -> exists'.

Goal exists'.
Proof.
  econstructor.

我们最终得到完全相同的结束状态，即使起始目标（之前econstructor）不同。

econstructor一般会丢失信息。

即使我们知道原始状态是什么，也可能无法回到原来的状态。对于这个例子，我们将使用inhabited标准库，但它同样适用于exists，因为inhabited A它等价于exists a: A, True.

Goal forall A: Type, inhabited A -> inhabited A.
Proof.
  intros A H.
  econstructor.

现在证明状态是

1 subgoal
A : Type
H : inhabited A
______________________________________(1/1)
A

我们想用它H来解决目标。但这（通常）是不可能的。我们不能仅仅从 type 元素A存在的陈述开始并生成 type 的实际术语A。问题是因为H是 a Prop，如果目标也是 a ，我们可以破坏它（或匹配它）Prop。使用之后econstructor，情况就不再如此了，所以我们必须有一个明确的类型见证A。在您的示例中，它有效，因为我们确切知道nat满足的哪个元素n = 1，但一般来说，我们不知道

证明助手Lean 使用一般语句forall A, nonempty A -> A（nonempty与 Coq 相同inhabited）为其经典逻辑库提供支持。Coq 中的排中证明同样适用（假设功能外延和命题外延）。所以，如果我们有forall A: Type, inhabited A -> A，那么排中律，甚至选择公理的一些强版本，都是可证明的（加上一些外延公理）。

---

另请注意，当您使用 时econstructor，任何存在变量最终都必须使用当前上下文中存在的值进行实例化。如果你有H: exists n: nat, n = 1，你必须在使用H 前econstructor破坏。

Hypothesis H: exists n: nat, n = 1.

Goal exists n: nat, n = 1.
Proof.
  destruct H as [x H].
  econstructor.
  exact H.
Defined.

Goal exists n: nat, n = 1.
Proof.
  econstructor.
  destruct H as [x H].
  Fail exact H.
Abort.