2

I am reading/testing a proof in Coq

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

The specific functions/definitions don't matter as they are not used. After a few steps, the theorem is transformed to a form where the inner existential quantifier is changed to a universal:

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

This is basically,

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

Although this is not exactly replacing exists i with forall i verbatim, I am kind of surprised. I was wondering if this kind of replacing existential quantifier with universals always possible, or when is this possible? What's the general rule/technique for this conversion?

(I vaguely remember something called skolemization but didn't quite understand it when learning it.)

The steps in Coq (8.4) to transform the theorem are:

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

1 回答 1

2

是的，这总是可能的！您偶然发现了依赖对的柯里化。使用Curry-Howard 同构，您可以将其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（而不是命题的证明）。这样的产品称为 sigma 类型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 有任何关系。

于 2015-12-03T05:03:25.010 回答