Dan Felteyが示唆したPierce教授の2012年夏のビデオ4.1のおかげで、重要なのは、抽出される定理が通常の種類の命題ではなく、のメンバーを提供する必要があることです。TypeProp
特定の定理の場合、影響を受ける構成は帰納的プロップexとその表記法existsです。ピアス教授が行ったことと同様に、独自の代替定義ex_tを記述して、の発生をの発生exists_tに置き換えることができます。PropType
exこれは、Coqの標準ライブラリで定義されているのとexists同様の通常の再定義です。
Inductive ex (X:Type) (P : X->Prop) : Prop :=
ex_intro : forall (witness:X), P witness -> ex X P.
Notation "'exists' x : X , p" := (ex _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
別の定義は次のとおりです。
Inductive ex_t (X:Type) (P : X->Type) : Type :=
ex_t_intro : forall (witness:X), P witness -> ex_t X P.
Notation "'exists_t' x : X , p" := (ex_t _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
さて、やや残念ながら、これらの新しい定義を使用して、ステートメントと定理の証明の両方を繰り返す必要があります。
いったい何？
量化子の別の定義を使用することによってのみ異なる、定理の繰り返しのステートメントと定理の繰り返しの証明を行う必要があるのはなぜですか？
で既存の定理を使用してProp、で定理をもう一度証明したいと思っていましたType。Coqがを使用する環境での証明戦術を拒否し、目標がを使用する場合inversion、その戦略は失敗します。Coqは、「エラー：反転には、帰納的定義では許可されていないソートセットのケース分析が必要になる」と報告しています。この動作はCoq8.3で発生しました。Coq8.4でまだ発生するかどうかはわかりません。PropPropexistsTypeexists_t
私は個人的にその深遠さをかなり理解しているとは思えませんが、証明を繰り返す必要性は実際には深いと思います。それは、「非叙述的」であり、非叙述的ではなく、むしろ暗黙のうちに「層化」されているという事実を含んでいPropますType。非叙述性は（私が正しく理解している場合）ラッセルのパラドックスに対する脆弱性であり、それ自体のメンバーではないセットのセットSはSのメンバーでもSの非メンバーでもあり得ません。Typeより低いタイプを含むより高いタイプのシーケンスを暗黙的に作成することにより、ラッセルのパラドックスを回避します。Coqは、カリーハワード対応の型としての式の解釈に浸っているため、これを正しく理解すれば、特定の式が表す現象であるゲーデルの不完全性を回避する方法として、Coqの型の階層化を理解することもできます。それ自体のような公式に対する制約は、それによってそれらの真偽について知ることができなくなります。
地球に戻って、ここに「exists_t」を使用した定理の繰り返しのステートメントがあります。
Theorem divalg_t : forall n m : nat, exists_t q : nat,
exists_t r : nat, n = plus (mult q m) r.
の証明を省略したdivalgので、の証明も省略しdivalg_tます。「exists」や「inversion」などの証明戦術が、新しい定義「ex_t」や「exists_t」とまったく同じように機能するという幸運があることだけを述べておきます。
最後に、抽出自体は簡単に実行できます。
Extraction Language Haskell.
Extraction "divalg.hs" divalg_t.
結果として得られるHaskellファイルには、いくつかの定義が含まれています。その中心となるのは、以下のかなり優れたコードです。そして、私はHaskellプログラミング言語をほぼ完全に知らなかったために少しだけ妨げられました。Ex_t_introタイプがEx_t;である結果を作成することに注意してください。OとSは、ペアノ算術のゼロおよび後続関数です。beq_natペアノの数が等しいかどうかをテストします。nat_recは、引数の中で関数を繰り返す高階関数です。の定義はnat_recここには示されていません。いずれにせよ、Coqで定義された帰納型「nat」に従ってCoqによって生成されます。
divalg :: Nat -> Nat -> Ex_t Nat (Ex_t Nat ())
divalg n m =
case m of {
O -> Ex_t_intro O (Ex_t_intro n __);
S m' ->
nat_rec (Ex_t_intro O (Ex_t_intro O __)) (\n' iHn' ->
case iHn' of {
Ex_t_intro q' hq' ->
case hq' of {
Ex_t_intro r' _ ->
let {k = beq_nat r' m'} in
case k of {
True -> Ex_t_intro (S q') (Ex_t_intro O __);
False -> Ex_t_intro q' (Ex_t_intro (S r') __)}}}) n}
更新2013-04-24：私はもう少しHaskellを知っています。上記の抽出されたコードを他の人が読むのを助けるために、私が同等で読みやすいと主張する次の手書きのコードを提示します。また、削除しなかった抽出された定義Nat、O、S、およびnat_recも示しています。
-- Extracted: Natural numbers (non-negative integers)
-- in the manner in which Peano defined them.
data Nat =
O
| S Nat
deriving (Eq, Show)
-- Extracted: General recursion over natural numbers,
-- an interpretation of Nat in the manner of higher-order abstract syntax.
nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
nat_rec f f0 n =
case n of {
O -> f;
S n0 -> f0 n0 (nat_rec f f0 n0)}
-- Given non-negative integers n and m, produce (q, r) with n = q * m + r.
divalg_t :: Nat -> Nat -> (Nat, Nat)
divalg_t n O = (O, n) -- n/0: Define quotient 0, remainder n.
divalg_t n (S m') = divpos n m' -- n/(S m')
where
-- Given non-negative integers n and m',
-- and defining m = m' + 1,
-- produce (q, r) with n = q * m + r
-- so that q = floor (n / m) and r = n % m.
divpos :: Nat -> Nat -> (Nat, Nat)
divpos n m' = nat_rec (O, O) (incrDivMod m') n
-- Given a non-negative integer m' and
-- a pair of non-negative integers (q', r') with r <= m',
-- and defining m = m' + 1,
-- produce (q, r) with q*m + r = q'*m + r' + 1 and r <= m'.
incrDivMod :: Nat -> Nat -> (Nat, Nat) -> (Nat, Nat)
incrDivMod m' _ (q', r')
| r' == m' = (S q', O)
| otherwise = (q', S r')