あなたの直感は的を射ていますが、なぜあなたが言ったことを意味するのかをbool_ind考えると、他の2つを明確にするのに役立つかもしれません. bool_ind私達はことを知っています
bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b
これを論理式として読むと、あなたがしたのと同じ読みが得られます。
- eans の
すべての述語
Pについて、bool
- 成立する場合
P true、および
P false成立すれば、- すべてのブール値について
b、
しかし、これは単なる論理式ではなく、型です。具体的には、(従属) 関数タイプです。そして、関数型として、次のように言います（名前のない引数と結果の名前を発明する自由を許可してくれれば）：
- 与えられた値
P : bool -> Prop、
- 値
Pt : P true,
- 値
Pf : P false、および
- 値
b : bool,
(もちろん、これはカリー化された関数なので、型を散文に分解する方法は他にもありますが、これが私たちの目的には最も明確です。)
ここで非常に重要なことは、Coq がプログラミング言語でありながら定理の証明者として機能する (またはその逆) のは、カリー-ハワード対応(型は命題であり、値はそれらの命題の証明) です。たとえば、単純関数型->は含意に対応し、従属関数型forallは全称量化に対応します。(表記はかなり暗示的です :-)) したがって、Coq で φ → ψ を証明するには、型 の値を作成する必要がありますφ -> ψ: 型の値を取る関数φ(つまり、命題 φ の証明)そして、それを使用して型の値を構築しますψ(命題 ψ の証明)。
SetCoqでは、すべての型をこのように考えることができTypeますProp。(したがって、「P true (bool rec の Set で bool_rect の Type) が命題値として扱われているように見える」と言うとき、あなたは正しいです!) たとえば、どのようにするかを考えてみましょう自分たちで実装bool_indします。関数へのすべてのパラメーターとその戻り値の型をリストすることから始めます。
Definition bool_ind' (P : bool -> Prop)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
ここまでは順調ですね。この時点で、 type の何かを返したいのですがP b、それが何かはわかりませんb。したがって、これらの状況ではいつものように、パターン マッチを行います。
match b with
現在、2つのケースがあります。まず、b可能性がありますtrue。この場合、タイプ の何かを返す必要がありP true、幸運にもそのような値があります: Pt。
| true => Pt
falseケースは似ています：
| false => Pf
end.
bool_ind'を実装すると、非常に「プルーフ」ではなく、非常に「プログラム的」に見えることに注意してください。もちろん、カリー・ハワード対応のおかげで、これらは同じです。ただし、他の 2 つの関数については、まったく同じ実装で十分であることに注意してください。
Definition bool_rec' (P : bool -> Set)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
Definition bool_rect' (P : bool -> Type)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
この計算定義を見ると、 、 、および に関する別の方法がbool_ind明らかbool_recになります。それらは、のすべての値についてbool_rect話すために知っておく必要があることをカプセル化しています。しかし、いずれにせよ、私たちはその情報をパッケージ化しています: もし私が何かを知っているなら、私はそれをすべてののために知っています.booltruefalsebool
関数の定義は、bool_{ind,rec,rect}ブール値で関数を記述する通常の方法を抽象化します。true 分岐に対応する引数が 1 つと、false 分岐に対応する引数が 1 つあります。または、言い換えれば、これらの関数は単なるifステートメントです。非依存型言語では、より単純な type を持つことができますforall S : Set, S -> S -> bool -> S:
Definition bool_simple_rec (S : Set) (St : P) (Sf : P) (b : bool) : S :=
match b with
| true => St
| false => Sf
end.
ただし、型は値に依存する可能性があるため、bあらゆる場所に型を通す必要があります。しかし、それが望ましくないことが判明した場合は、より一般的な関数を使用して次のように伝えることができます。
Definition bool_simple_rec' (S : Set) : S -> S -> bool -> S :=
bool_rec (fun _ => S).
!P : bool -> Setを使用する必要があるとは誰も言いませんでした。bool
これらの関数はすべて、再帰型にとってより興味深いものです。たとえば、Coq には次のタイプの自然数があります。
Inductive nat : Set := O : nat | S : nat -> nat.
そして、私たちは持っています
nat_ind : forall P : nat -> Prop,
P O ->
(forall n' : nat, P n' -> P (S n')) ->
forall n : nat,
P n
対応するnat_recとnat_rect. (読者のための演習: これらの関数を直接実装してください。)
一見すると、これは単なる数学的帰納法の原理です。natただし、 sに再帰関数を記述する方法でもあります。それらは同じものです。一般に、再帰関数natは次のようになります。
fix f n => match n with
| O => ...
| S n' => ... f n' ...
end
次のマッチのアームO(基本ケース) は、 type の値ですP O。次の一致のアームS n'(再帰的なケース) は、 type の関数に渡されるものですforall n' : nat, P n' -> P (S n'):n'の値は同じで、 の値はP n'再帰呼び出しの結果ですf n'。
_recと関数の間の等価性について考えるもう 1 つの方法は_ind、無限型よりも無限型の方が明確だと私が思うのはbool、数学的なindオークション ( で起こるProp) と (構造的な) recursion (とで発生しSetますType)。
実践してこれらの関数を使用しましょう。ブール値を自然数に変換する単純な関数を定義し、直接および を使用して実行しbool_recます。この関数を記述する最も簡単な方法は、パターン マッチを使用することです。
Definition bool_to_nat_match (b : bool) : nat :=
match b with
| true => 1
| false => 0
end.
別の定義は
Definition bool_to_nat_rec : bool -> nat :=
bool_rec (fun _ => nat) 1 0.
そして、これら 2 つの機能は同じです。
Goal bool_to_nat_match = bool_to_nat_rec.
Proof. reflexivity. Qed.
(注: これらの関数は構文的に equalです。これは、単純に同じことを行うよりも強力な条件です。)
ここでは、P : bool -> Setですfun _ => nat。これにより、引数に依存しない戻り値の型が得られます。私たちのPt : P trueis は1、与えられたときに計算するものですtrue。同じく当方のPf : P falseは0
依存関係を使用したい場合は、便利なデータ型を作成する必要があります。どうですか
Inductive has_if (A : Type) : bool -> Type :=
| has : A -> has_if A true
| lacks : has_if A false.
この定義でhas_if A trueは、 は に同型Aであり、has_if A falseは に同型unitです。次に、渡された場合にのみ最初の引数を保持する関数を作成できますtrue。
Definition keep_if_match' (A : Type) (a : A) (b : bool) : has_if A b :=
match b with
| true => has A a
| false => lacks A
end.
別の定義は
Definition keep_if_rect (A : Type) (a : A) : forall b : bool, has_if A b :=
bool_rect (has_if A) (has A a) (lacks A).
そして、それらは再び同じです:
Goal keep_if_match = keep_if_rect.
Proof. reflexivity. Qed.
ここで、関数の戻り値の型は引数に依存するbため、P : bool -> Type実際に何かを行います。
自然数と長さのインデックス付きリストを使用した、より興味深い例を次に示します。ベクトルとも呼ばれる長さのインデックス付きリストを見たことがない場合、それらはまさに缶に書かれているとおりです。vec A ns のリストですn A。
Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A O
| vcons : forall n, A -> vec A n -> vec A (S n).
Arguments vnil {A}.
Arguments vcons {A n} _ _.
(Arguments機械は暗黙の引数を処理します。) さて、ある特定の要素のコピーのリストを生成したいnので、それを修正点で書くことができます:
Fixpoint vreplicate_fix {A : Type} (n : nat) (a : A) : vec A n :=
match n with
| O => vnil
| S n' => vcons a (vreplicate_fix n' a)
end.
または、次を使用できますnat_rect。
Definition vreplicate_rect {A : Type} (n : nat) (a : A) : vec A n :=
nat_rect (vec A) vnil (fun n' v => vcons a v) n.
nat_rect再帰パターンをキャプチャするためvreplicate_rect、それ自体は修正点ではないことに注意してください。注意すべきことの 1 つは、 の 3 番目の引数nat_rectです。
fun n' v => vcons a v
v概念的には、への再帰呼び出しの結果がありますvreplicate_rect n' a。nat_rectその再帰パターンを抽象化するので、直接呼び出す必要はありません。はn'確かに と同じですがn'、vreplicate_fix明示的に言及する必要はないようです。なぜそれが渡されるのですか？型を書き出すと、それは明らかになります。
fun (n' : nat) (v : vec A n') => vcons a v : vec A (S n')
どの型があり、その結果、結果がどの型であるn'かを知る必要があります。v
これらの関数の動作を見てみましょう。
Eval simpl in vreplicate_fix 0 tt.
Eval simpl in vreplicate_rect 0 tt.
(* both => = vnil : vec unit 0 *)
Eval simpl in vreplicate_fix 3 true.
Eval simpl in vreplicate_rect 3 true.
(* both => = vcons true (vcons true (vcons true vnil)) : vec bool 3 *)
実際、それらは同じです。
(* Note: these two functions do the same thing, but are not syntactically
equal; the former is a fixpoint, the latter is a function which returns a
fixpoint. This sort of equality is all you generally need in practice. *)
Goal forall (A : Type) (a : A) (n : nat),
vreplicate_fix n a = vreplicate_rect n a.
Proof. induction n; [|simpl; rewrite IHn]; reflexivity. Qed.
nat_rect上記では、再実装と友達の演習を行いました。答えは次のとおりです。
Fixpoint nat_rect' (P : nat -> Type)
(base_case : P 0)
(recurse : forall n', P n' -> P (S n'))
(n : nat)
: P n :=
match n with
| O => base_case
| S n' => recurse n' (nat_rect' P base_case recurse n')
end.
これにより、再帰パターンがどのよう nat_rectに抽象化されているか、およびそれが十分に一般的である理由が明確になることを願っています。