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

Question

我正在学习编程语言基础，被这句话搞得一头雾水。

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

为什么不呢？能不能给我举个例子，表现出不需要的行为？

谢谢。

Answer 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.