証明の第一歩

命題は型で、証明はその型の値です。

13.1 Prop という型の世界

普通のプログラムでは、Bool を条件分岐に使います。証明の世界では、Prop が命題の種類を表します。P: Prop は「P は何かの命題である」という意味です。

A が型で x: A がその値であるのと同じように、P が命題なら p: P はその命題の証明です。この見方を Curry–Howard 対応と呼びます。

import std::Base

theorem keep(A: Prop, p: A): A {
  p
}

✓ theorem keep : ∀ A: Prop. (A) -> A

keep は、「A が成り立つ証拠 p をもらえば、A の証拠を返せる」という定理です。本体の p は、すでにその型を持つ値なので、正しい証明になります。

ok      keep

13.2 「かつ」の証明を組み立てる

A ∧ B は、両方の証拠を持つ命題です。AndIntro(a, b) は二つの証拠を一つにまとめます。And::left と And::right は、それぞれの側を取り出します。

import std::Base

theorem and_swap(A: Prop, B: Prop, p: A ∧ B): B ∧ A {
  AndIntro(And::right(p), And::left(p))
}

✓ theorem and_swap : ∀ A: Prop. ∀ B: Prop. (And(A, B)) -> And(B, A)

p から「B の証拠」と「A の証拠」を取り出し、順序を逆にして組み立てています。数学の文章に近い見た目ですが、実体は型の付いた項です。

13.3 関数は「ならば」の証明

import std::Base

theorem compose(
  A: Prop,
  B: Prop,
  C: Prop,
  f: (A) -> B,
  g: (B) -> C
): (A) -> C {
  a => g(f(a))
}

✓ theorem compose : ∀ A: Prop. ∀ B: Prop. ∀ C: Prop. ((A) -> B) -> ((B) -> C) -> (A) -> C

f が「A の証拠から B の証拠を作る」、g が「B の証拠から C の証拠を作る」とすると、a => g(f(a)) は A から C への証明です。関数をつなぐだけで、論理の推論規則になります。

演習 13.1：(A) -> A を証明する関数は、本体に何を書けばよいでしょうか。