5

私は現在、SoftwareFoundationsという本を読んでいます。定理が定義されるとき、私は接続詞がより理にかなっていると私が信じる含意の連鎖をしばしば見ます。たとえば、鳩の巣原理を定義する際に、著者は次のように書いています。

Theorem pigeonhole_principle: ∀{X:Type} (l1 l2:list X),
  excluded_middle →
  (∀x, appears_in x l1 → appears_in x l2) →
  length l2 < length l1 →
  repeats l1.

この定義は、次のようになっていると、私にはもっと意味があります。

Theorem pigeonhole_principle: ∀{X:Type} (l1 l2:list X),
  (excluded_middle /\
  (∀x, appears_in x l1 → appears_in x l2) /\
  length l2 < length l1) →
  repeats l1.

最初のバージョンが正しいのはなぜですか？接続詞がより適切ではないのはなぜですか？

それはほんの一例です。より一般的には、接続詞がcoqの含意の連鎖を支持して避けられているように見える理由を尋ねています。

4

1 に答える 1

8

これは、関数カリー化の定理証明バージョンです。

要約すると、2つの式は両方とも正しいです（それらは同等です）。

ある人は言う：「排中律」をください。仮説2を教えてください。仮説3を教えてください。さて、これが「repeatsl1」というプロパティです。

もう1つは、「排中律」、仮説2、仮説3を教えてください。これが「リピートl1」というプロパティです。

Coqなどの証明アシスタントのユーザーと実装者も関数型プログラマーであり、カレーバージョンはカレーなしバージョンと同じように自然です。

于 2012-11-29T00:58:10.737 に答える