这样从存在量词到全称量词的转换总是可能的吗？

Question

我是reading/testing Coq 中的一个证明

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st') -> c / st || st'.

具体的 functions/definitions 无关紧要，因为它们未被使用。几步之后，定理转化为内在存在量词改为全称的形式：

1 subgoals
______________________________________(1/1)
forall (c : com) (st st' : state) (i : nat),
ceval_step st c i = Some st' -> c / st || st'

这基本上是，

Theorem ceval_step__ceval'': forall c st st', forall i
      ceval_step st c i = Some st' -> c / st || st'.

虽然这并不是完全用 forall i 逐字替换 exists i，但我还是有点惊讶。我想知道这种用普遍性代替存在量词是否总是可能的，或者这何时可能？此转换的一般 rule/technique 是多少？

（我依稀记得有一个东西叫skolemization，但是学的时候不是很明白。）

Coq(8.4)中对定理进行变换的步骤是：

Proof.
  intros c st st' H.
  inversion H as [i E].
  clear H.
  generalize dependent i.
  generalize dependent st'.
  generalize dependent st.
  generalize dependent c.

Answer 1

是的，这总是可能的！您偶然发现了 currying of dependent pairs. Using the Curry-Howard Isomorphism，您可以将 exists a:A, P a 视为一个依赖对，由类型为 A 的值 a 和命题证明 P 组成取决于 a。以下是 exists 产品的相关 curry/uncurry 的定义。

Variable A : Type.
Variable P : A -> Prop.
Variable Q : Prop.

Definition dependentCurryProp (h : (exists a:A, P a) -> Q) : forall a:A, P a -> Q :=
  fun a p => h (ex_intro _ a p).

Definition dependentUncurryProp (h : forall a:A, P a -> Q) : (exists a:A, P a) -> Q := 
  fun e => match e with ex_intro _ a p => h a p end.

您可以使用战术语言编写相同的功能。

Lemma dependentCurryProd (h : (exists a:A, P a) -> Q) : forall a:A, P a -> Q.
  intros a p.
  apply h.
  exists a.
  apply p.
Qed.

Lemma dependentUncurryProd (h : forall a:A, P a -> Q) : (exists a:A, P a) -> Q.
  intros e.
  destruct e as [a p].
  eapply h.
  apply p.
Qed.

同样的技巧适用于依赖产品，其中第一个值 a 是类型 A，第二个值 b 是类型 B a（而不是命题的证明）。这样的产品称为西格玛型sigT A B或{a:A & B a}。

Variable C : Type.
Variable B : A -> Type.

Definition dependentCurry (f : {a:A & B a} -> C) : forall a:A, B a -> C := 
  fun a b => f (existT _ a b).

Definition dependentUncurry (f : forall a:A, B a -> C) : {a:A & B a} -> C := 
  fun p => match p with existT _ a b => f a b end.

我不认为这与 skolemization 有任何关系。

这样从存在量词到全称量词的转换总是可能的吗？

Is conversion from existential quantifier to universal quantifier like this always possible?

coq

coq-tactic