Всегда ли возможен такой переход от квантора существования к квантору всеобщности?

Я читаю/тестирую доказательство в Coq

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

Конкретные функции/определения не имеют значения, поскольку они не используются. Через несколько шагов теорема преобразуется к форме, в которой внутренний квантор существования заменяется универсальным:

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

Хотя это не совсем дословная замена exists i на forall i, я несколько удивлен. Мне было интересно, всегда ли возможна такая замена квантора существования универсалиями, или когда это возможно? Каково общее правило/техника для этого преобразования?

(Я смутно припоминаю что-то, называемое сколемизацией, но не совсем понял, когда учился.)

Шаги в 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.

coq coq-tactic
person tinlyx    schedule 03.12.2015    source источник
comment
Гораздо проще помочь, если выложите рабочий код со всеми импортами и т.д., и максимально упростите задачу.   -  person Konstantin Weitz    schedule 03.12.2015
comment
@KonstantinWeitz, спасибо за ответ. Я хотел, чтобы это было кратким, и не хотел упрощать интересную часть, поскольку я не знаю, какая часть актуальна.   -  person tinlyx    schedule 03.12.2015

Ответы (1)


arrow_upward
2
arrow_downward

Да это всегда возможно! Вы наткнулись на каррирование зависимых пар. Используя изоморфизм Карри-Ховарда, вы можете думать о exists a:A, P a как о зависимом пара, состоящая из значения a типа A и доказательства предложения P, которое зависит от a. Ниже приводится определение зависимого карри/некарри для exists продуктов.

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.

Я не думаю, что это имеет какое-либо отношение к сколемизации.

person Konstantin Weitz    schedule 03.12.2015