7

「Certified Programming with Dependent Types」という本を読んで Coq を学んでいますが、構文を理解するのに苦労していforallます。

例として、この相互帰納的なデータ型を考えてみましょう: (コードは本から)

Inductive even_list : Set :=
| ENil : even_list
| ECons : nat -> odd_list -> even_list

with odd_list : Set :=
| OCons : nat -> even_list -> odd_list.

そして、この相互再帰的な関数定義:

Fixpoint elength (el : even_list) : nat :=
  match el with
  | ENil => O
  | ECons _ ol => S (olength ol)
  end

with olength (ol : odd_list) : nat :=
  match ol with
  | OCons _ el => S (elength el)
  end.

Fixpoint eapp (el1 el2 : even_list) : even_list :=
  match el1 with
  | ENil => el2
  | ECons n ol => ECons n (oapp ol el2)
  end

with oapp (ol : odd_list) (el : even_list) : odd_list :=
  match ol with
  | OCons n el' => OCons n (eapp el' el)
  end.

そして、誘導スキームが生成されました。

Scheme even_list_mut := Induction for even_list Sort Prop
with odd_list_mut    := Induction for odd_list Sort Prop.

今私が理解していないのは、のタイプから、even_list_mut3つの引数を取ることがわかります:

even_list_mut
     : forall (P : even_list -> Prop) (P0 : odd_list -> Prop),
       P ENil ->
       (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
       (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
       forall e : even_list, P e

しかし、それを適用するには、2 つのパラメーターを提供する必要があり、目標を 3 つの前提 ( P ENil、forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)およびforall (n : nat) (e : even_list), P e -> P0 (OCons n e)ケース) に置き換えます。

つまり、実際には 3 つではなく 5 つのパラメーターを取得するようです。

しかし、このタイプについて考えると、この考えは失敗します。

fun el1 : even_list =>
  forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2
       : even_list -> Prop

と

fun el1 el2 : even_list => elength (eapp el1 el2) = elength el1 + elength el2
     : even_list -> even_list -> Prop

構文の仕組みを説明できる人はいforallますか?

ありがとう、

4

1 に答える 1

7

実際、even_list_mut6 つの引数を取ります。

even_list_mut
 : forall
     (P : even_list -> Prop)                                      (* 1 *)
     (P0 : odd_list -> Prop),                                     (* 2 *)
     P ENil ->                                                    (* 3 *)
     (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->  (* 4 *)
     (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> (* 5 *)
     forall e : even_list,                                        (* 6 *)
     P e

矢印は単なるシンタックス シュガーと考えることができます。

A -> B
===
forall _ : A, B

したがって、次のように書き直すことができますeven_list_mut。

even_list_mut
 : forall
     (P  : even_list -> Prop)
     (P0 : odd_list -> Prop)
     (_  : P ENil)
     (_  : forall (n : nat) (o : odd_list), P0 o -> P (ECons n o))
     (_  : forall (n : nat) (e : even_list), P e -> P0 (OCons n e))
     (e : even_list),
     P e

そのような項を適用すると、いくつかの引数が統一によって推論できる場合があります (項の戻り値の型を目標と比較する)。したがって、これらの引数は、Coq がそれを理解したために目標になりません。たとえば、私が持っているとしましょう：

div_not_zero :
  forall (a b : Z) (Anot0 : a <> 0), a / b <> 0

そしてゴールに当てはめます42 / 23 <> 0。Coq は、それがaすべきこと42とbすべきことを理解することができます23。残された唯一の目標は、 を証明すること42 <> 0です。しかし実際には、Coq は暗黙的に42and23を引数として に渡しますdiv_not_zero。

これが役立つことを願っています。

編集1：

追加の質問に答える:

fun (el1 : even_list) =>
  forall (el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
: even_list -> Prop

el1 : even_listは、型 を返す1 つの引数 の関数ですforall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2。非形式的には、 list が与えられるel1と、 statement が構築されfor every list el2, the length of appending it to el1 is the sum of its length and el1's lengthます。

fun (el1 el2 : even_list) =>
  elength (eapp el1 el2) = elength el1 + elength el2
: even_list -> even_list -> Prop

el1 : even_listは と の 2 つの引数を持つ関数でel2 : even_list、型 を返しますelength (eapp el1 el2) = elength el1 + elength el2。非公式に、2 つのリストが与えられると、ステートメント が作成されfor these particular two lists, the length of appending them is the sum of their lengthます。

2 つのことに注意してください: - 最初に「ステートメントを構成する」と言いましたが、これは「ステートメントの証明を構成する」とは大きく異なります。これらの 2 つの関数は、型/命題/ステートメントを返すだけで、真または偽である可能性があり、証明可能または証明不可能である可能性があります。-最初のものは、 list を入力するel1と、非常に興味深い型を返します。そのステートメントの証明があれば、 の任意の選択についてel2、それを に追加する長さel1が長さの合計になることがわかります。

実際、考慮すべき別のタイプ/ステートメントを次に示します。

forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
: Prop

このステートメントは、任意の 2 つのリストについて、追加の長さは長さの合計であることを示しています。

あなたも混乱するかもしれないことの1つは、これが起こっているということです:

fun (el1 el2 : even_list) =>
  (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *)

タイプが

forall (el1 el2 : even_list),
  elength (eapp el1 el2) = elength el1 + elength el2

タイプが

Prop

funとは関連していますforallが、非常に異なるものです。実際、すべての形式は、型が であると仮定してfun (t : T) => p t、型が である項です。forall (t : T), P tp tP t

したがって、次のように書くと混乱が生じます。

fun (t : T) => forall (q : Q), foo
               ^^^^^^^^^^^^^^^^^^^
               this has type  Prop

これにはタイプがあるため：

forall (t : T), Prop (* just apply the rule *)

この微積分forallは型を計算できるため、実際には 2 つのコンテキストで表示される可能性があります。したがって、forall計算内 (これが型構築の計算であるという事実を示唆しています) 内に表示されるか、型内 (通常は型を表示する場所) 内に表示される可能性があります。しかし、それはforallすべての意図と目的で同じです。一方、funは計算にしか現れません。

于 2013-07-04T09:57:31.463 に答える