coq 中存在变量的实例化规则

Posted

技术标签:

【中文标题】coq 中存在变量的实例化规则【英文标题】:rules on instantiation of existential variables in coq 【发布时间】:2020-05-14 03:04:48 【问题描述】:

我正在研究编程语言基础,但对这一行感到困惑:

"存在变量不能 用包含普通变量的术语实例化 在存在变量创建时存在。 "

为什么不呢?我可以举一个表现出不良行为的例子吗?

谢谢。

【问题讨论】:

【参考方案1】:

这是一个说明性示例:

(* An empty type *)
Inductive empty : Type := .

(* A proposition quantifying existentially over an empty type can only be false... *)
Lemma this_cannot_be_true : exists x : empty, (forall y : empty, x = y).
Proof.
  eexists.   (* I'm telling you there is such an x, just put an evar ?x for now. *)
  intros y.  (* Now we must prove a universal property, so we introduce a new variable... *)
  Fail instantiate (1 := y).  (* Oh look, y : empty, let's instantiate our evar with it! *)
  (* If this didn't fail, we would have the goal (y = y), which would be proved by reflexivity. Luckily, the previous tactic failed. *)
Abort.

(* To clear out any doubt that the above proposition is false. *)
Lemma empty_type_is_empty P : empty -> Prop : (exists x : empty, P x) -> False.
Proof.
  intros [[]].
Qed.

【讨论】:

这实际上只是范围界定,这是相当常识的。只是当你使用策略而不是仅仅写术语时可能有点难以看出。在intros y 之后,证明项看起来像this_cannot_be_true := ex_intro _ _ ?X (fun y => ?Goal)instantiate 正在尝试设置 X := y,而下面的 reflexivity 会留下 ex_intro _ _ y (fun y => eq_refl y)。这被拒绝了,因为您试图在绑定/定义的上下文之外使用y(在fun y 下)。 这是一个很好的解释。我只是不会假设提出这个问题的人熟悉该策略产生的证明术语。只有具有正确背景的人才有“常识”。

以上是关于coq 中存在变量的实例化规则的主要内容,如果未能解决你的问题,请参考以下文章

coq 中的存在实例化和泛化

无法实例化 MatchXpath

Java静态方法,静态变量,初始化顺序

Java对象实例化顺序

python的类定义与实例化

在统一过程中,高级类型的实例化和包含如何交互?