2

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

1 に答える 1

2

はい、これはいつでも可能です。従属ペアのカリー化に出くわしました。Curry-Howard Isomorphismを使用すると、 type の値とに依存する命題の証明でexists a:A, P a構成される従属ペアと考えることができます。以下は、製品の従属カレー/アンカレーの定義です。aAPaexists

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で、2 番目の値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.

これはスコーレム化とは何の関係もないと思います。

于 2015-12-03T05:03:25.010 に答える