等式を証明する

等式の命題、反射律、矛盾を使います。

14.1 a = b は値が等しいことの証拠

import std::Base

theorem two_plus_two(): (2: Nat) + 2 = 4 {
  Refl
}

✓ theorem two_plus_two : 2 + 2 = 4

a = b は、型 Nat の二つの項が等しいという命題です。Refl は反射律、つまり「同じものは同じものに等しい」を与えます。2 + 2 と 4 は、計算によって同じ形に簡約できるので、カーネルはこの証明を受け取れます。

== と a = b を混同しないでください。== は実行時に使う等価比較で、a = b は証明の世界で扱う命題です。

間違った命題は、通りません。

import std::Base

theorem wrong(): (2: Nat) + 2 = 5 {
  Refl
}

✗ wrong

error 4:3: type mismatch: expected `2 + 2 = 5`, found `2 + 2 = 2 + 2`
  differing part: expected `5`, found `4`

コードの下には、使用中の CLI が返した実際の型エラーを表示します。

Refl は (4: Nat) = 4 の証明であって、2 + 2 = 5 の証明ではない、という指摘です。Refl が証明できるのは、「計算した結果が一致する」ことだけです。

14.2 等式をつなぐ

Refl の型や等式の項は、証明すべき命題から決まります。証明中では Refl と書きます。

import std::Base

theorem sym_ex(a: Nat, b: Nat, e: a = b): b = a {
  Eq::sym(e)
}

theorem trans_ex(
  a: Nat,
  b: Nat,
  c: Nat,
  e1: a = b,
  e2: b = c
): a = c {
  Eq::trans(e1, e2)
}

theorem congr_ex(a: Nat, b: Nat, e: a = b): Succ(a) = Succ(b) {
  Eq::congr(Succ, e)
}

✓ theorem sym_ex : ∀ a: Nat. ∀ b: Nat. (a = b) -> b = a
✓ theorem trans_ex : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. (a = b) -> (b = c) -> a = c
✓ theorem congr_ex : ∀ a: Nat. ∀ b: Nat. (a = b) -> Succ(a) = Succ(b)

14.3 間違った等式を仮定したら

import std::Base

theorem two_plus_two_ne_five(h: (2: Nat) + 2 = 5): False {
  match h: False {
  }
}

✓ theorem two_plus_two_ne_five : ¬(2 + 2 = 5)

この定理は、「もし 2 + 2 = 5 の証拠があるなら、矛盾に到達する」と主張します。2 + 2 は 4 になるので、(4: Nat) = 5 は、Refl のどの形とも一致しません。腕が空の match は、あり得る構成子が一つもないことを表しています。

14.4 公理を足すことの意味

公理 axiom を宣言すると、証明されていない仮定を採用できます。これ自体が、常に不正という意味ではありません。たとえば排中律は、次のように公理として足せます。

import std::Base

axiom em(P: Prop): P ∨ ¬P

theorem not_not(P: Prop, n: ¬¬P): P {
  Or::elim(em(P), p => p, np => False::elim(n(np)))
}

✓ axiom em : ∀ P: Prop. Or(P, ¬P)
✓ theorem not_not : ∀ P: Prop. (¬(¬P)) -> P

ok      em (axioms: em)
ok      not_not (axioms: em)

出力にも、not_not が公理 em に依存していることが表示されます。公理を使った定理は、公理に依存した結果です。証明済みであることと、公理なしで成り立つことは、区別してください。

演習 14.1：theorem reflexive(x: Nat): x = x を完成させてください。