形式証明において、本質的ではない面倒くささの一端は、 似ているけれど違うので直接は使えない、という状況に真面目に対応する必要があることである。
CIC (Rocq とか Lean の基礎) において、命題と bool はまさにこの典型例である。 命題と bool はどちらも成り立ったり成り立たなかったりするし、 and や or といった論理演算はどちらにも存在して、対応がある。
ここで、Rocq/SSReflect でも Lean でも、命題の and は /\ 演算子で表現し、bool の and は && 演算子で表現する。
そして、一方 (例えば bool 式) が真であることがわかっている場合に、 対応するもう一方 (命題) が真であることを証明しようとするのは、 素朴な CIC では手間がかかる。 人間の感覚としては自明なのに手間が必要というのは、そこには改善の余地があるということだ。
また、bool と命題では証明を行うときの便利さが異なる。
bool が便利なところ:
命題が便利なところ:
証明においてはこれら両方の便利さを利用したいわけで、 SSReflect や Lean ではそれなりに系統的な対策が行われている。
どういう対策かというと、SSReflect では、bool で表現できるものはなるべく bool で表現し、必要になった場合には bool と命題を簡単に変換できる、というようになっている。 (このへんは mathcomp book に詳しい。)
Lean では (少し観察した限りでは) なるべく命題で扱うようになっていると思う。 たとえば、if 式では条件節に bool ではなく命題を書く。 しかし、bool には bool の便利さがあるので、その便利さもなるべく得られるような仕掛けがある。
まず、bool の便利なところとして、部分項を rewrite できるという点がある。 これは rewrite というのは内部的には eq_ind_r : forall [A : Type] [x : A] (P : A -> Prop), P x -> forall [y : A], y = x -> P y の適用であり、 goal をまず P y という関数適用の形に変形し、y を置き換えて x にする、というものだからで、 P y という形で括り出せるかぎりはどの部分項でも置換できるからである。
それに対して、A <-> B という前提があっても、 素朴にはゴール全体を A から B に変える、あるはその逆にしか使えない。 これは、A <-> B の証明は、A -> B の証明と B -> A の証明のペアだからである。 A -> B の証明があれば、apply により goal を B から A に変えられる。 しかし apply というのは goal 全体に適用するものであり、 goal の部分項に apply するということはできない。 したがって、部分項を書き換えることは (素朴には) できないのである。
ところが、Lean では命題でも部分項を rewrite できる。
theorem foo (A B C : Prop) (h : A <-> B) : (A /\ C) <-> (B /\ C) := by rw [h] #print foo /- theorem foo : ∀ (A B C : Prop), (A ↔ B) → (A ∧ C ↔ B ∧ C) := fun A B C h => Eq.mpr (id (congrArg (fun _a => _a ∧ C ↔ B ∧ C) (propext h))) Iff.rfl -/
証明項をみると、propext というのが使われている。 propext というのは、公理 propositional extensionality のようだ。 公理を使って、命題の等価性 (<->) を等値性 (=) に変換して、部分項を書き換えているようだ。
ちなみに、最近は Rocq でも setoid rewrite により似たことが可能になった。
Require Setoid.
Theorem foo (A B C : Prop) (h : A <-> B) : (A /\ C) <-> (B /\ C).
Proof.
rewrite h.
reflexivity.
Qed.
Print foo.
(*
foo =
fun (A B C : Prop) (h : A <-> B) =>
(fun lemma : A <-> B =>
Morphisms.trans_co_eq_inv_impl_morphism RelationClasses.iff_Transitive
(A /\ C) (B /\ C)
(Morphisms_Prop.and_iff_morphism A B lemma C C
(Morphisms.reflexive_proper_proxy
(Morphisms.reflexive_reflexive_proxy RelationClasses.iff_Reflexive) C))
(B /\ C) (B /\ C) (Morphisms.eq_proper_proxy (B /\ C)))
h (RelationClasses.reflexivity (B /\ C))
: forall A B C : Prop, A <-> B -> A /\ C <-> B /\ C
*)
証明項をみると、Lean よりも Rocq のほうがずいぶんと長い。 これは公理を使わずにがんばって実現しているためだろう。
まず、命題は計算できない。True と True /\ True は異なる項であり、型検査でも区別される。
それに対して bool の式は計算できる。 そして、CIC の型検査はそういった計算による変形をしても同じ項とみなす。
そのため、term = true という命題で term を計算して true になるなら、 reflexivity (rfl) でそのまま証明できる。
ただ、term に変数が入っていると計算が進まない。 たとえば、x || ~~ x = true は x の具体的な値が不明なので、 orb (||) や negb (~~) の内部での場合分けが簡約できない。 そこで変数 x を場合分けすると、x が true に置換された場合と false に置換された場合の変数が消えたふたつの goal ができて、 あとは計算で証明を終わらせられる。
ということを SSReflect では by case: x. などと書くわけである。 変数が複数あっても by case: x; case: y. などと証明できるので簡単である。 (ただ、変数が多くなってくるとサブゴールが多くなりすぎて証明に時間がかかってしまうが、そんなにたくさんの変数が出てくることは稀である。)
なお、この計算というのは、true || x は計算が進んで x になるが、x || true は計算を進められないなど、 関数 (この場合 orb) の中身に依存した挙動がある。 仕組みを理解していればわかるのだが、わかりやすいとはいえないかもしれない。
上にも書いたが、この計算というのは bool だからできるのであって、命題ではできない。
しかし、Lean の simp は上述の、命題の部分項を rewrite できるという機能を利用し、命題の単純化も行う。 simp はデフォルトでいろいろな定理を利用するが、その中には or_true と true_or も含まれており、 命題の単純化もしてしまう。
or_true (p : Prop) : (p ∨ True) = True true_or (p : Prop) : (True ∨ p) = True
これは命題で計算しているようなものかも知れない。
命題は証明可能と反証可能以外に、証明も反証もできないということがあり得るので、 true と false の 2種類に場合分けできるとは限らない。
しかし、2種類に場合分けできることも多々ある。
そのようなことを示すのに、SSReflect では、reflect という型で命題と bool が対応していることを表現する。
<URL:https://github.com/rocq-prover/rocq/blob/v9.3/theories/Corelib/Init/Datatypes.v#L51-L59>
(************************************************)
(** * Reflect: a specialized inductive type for
relating propositions and booleans,
as popularized by the Ssreflect library. *)
(************************************************)
Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
Lean には Decidable という型があって、ある命題が判定可能であることを表現する。
<URL:https://github.com/leanprover/lean4/blob/v4.32.1/src/Init/Prelude.lean#L962-L976>
`Decidable` instances are primarily used via `if`-expressions and the tactic `decide`. In
conditional expressions, the `Decidable` instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
`Bool`-based conditional. In proofs, the tactic `decide` synthesizes an instance of `Decidable p`,
attempts to reduce it to `isTrue h`, and then succeeds with the proof `h` if it can.
Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance
on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical
instances can be found via unification rather than instance synthesis.
-/
class inductive Decidable (p : Prop) where
/-- Proves that `p` is decidable by supplying a proof of `¬p` -/
| isFalse (h : Not p) : Decidable p
/-- Proves that `p` is decidable by supplying a proof of `p` -/
| isTrue (h : p) : Decidable p
reflect も Decidable も、場合分けすると真の場合と偽の場合に分かれるので、 真でも偽でもない (その命題を証明も反証もできない) ということはありえないことを示している。
reflect と Decidable の違いは、bool の index である。 reflect と Decidalbe は引数の数が異なり、前者は 2引数で、後者は 1引数である。 最初の引数は命題でどちらも同じだが、reflect は reflect P b と bool な第2引数がある。
reflet は、命題と bool の関係を示しているので、命題と bool を変換することに利用できる。 これに対して、Lean の Decidable は、単に命題が判定可能という性質を示すだけなので、bool との変換は想定されていないのだと思う。 これは、Lean が bool よりは命題を好むことと関係しているのかも。
あと、reflect の index は、場合分けをしたときに同時に書き換えを行うのに利用される。 これにより、いちいち書き換えをするように指定しなくてよいので便利である。
Lean の if 式は if c then t else e という普通の形なのだが、 条件節 c には命題を書くというのが面白い。
if c then t else e という式は ite という関数を用いて ite c t e と実装される。 ただし、ここには Decidable c 型の暗黙の引数が隠れていて、場合分けはこの Decidable c 型の引数に対して行われる。
<URL:https://github.com/leanprover/lean4/blob/v4.32.1/src/Init/Prelude.lean#L1100-L1121>
/--
`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
-/
/-
Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
-/
@[macro_inline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
h.casesOn (fun _ => e) (fun _ => t)
まぁ、bool の式を書きたければ if term = true then t else e と書けばいいので、上位互換であると言えるかも知れない。
でも、こんなところに依存型を使うと、厄介なことが起きるのではないかと思って考えてみて、以下の例を思いついた。
theorem foo (a b : Nat) : (if a < b then 1 else 2) = (if (1+a) < (1+b) then 1 else 2) := by
rw [Nat.add_lt_add_iff_left] -- この rw が失敗する
#check Nat.add_lt_add_iff_left
-- Nat.add_lt_add_iff_left {k n m : Nat} : k + n < k + m ↔ n < m
ここでは条件節が a < b と (1+a) < (1+b) と違いだけの項が等しい、ということを証明しようとしている。 そのために Nat.add_lt_add_iff_left を使って (1+a) < (1+b) を a < b に書き換えようとしている。 しかし、その書き換えが失敗する。 これは、ite 関数の条件節 (命題な引数) を書き換えても、Decidable な引数がそのままで、 それらが整合しなくなってしまうからである。
まぁ、simp [Nat.add_lt_add_iff_left] とすると動くので、rw でうまくいかなかったら simp を使えば良い、と対応されている話ではあるのかも。
[latest]