Accを使って定義した再帰関数の評価が進まず、自明な定理が直ちに示せなかったのでその原因を調べました。

注意

以下のコードは Rocq 9.0.0 で試しました。また、以下の情報は Rocq 9.0.* 時点のものです。

本題

以下の関数floor_log2を考えます1。

From mathcomp Require Import ssreflect.
From Stdlib Require Import Arith Lia ZifyNat.

Lemma floor_log2_proof {n} : 1 < n -> n / 2 < n.
Proof. by lia. Defined.

Fixpoint floor_log2 n (ACC : Acc lt n) :=
  match le_lt_dec n 1 with
  | left _ => 0
  | right H => S (floor_log2 (n / 2) (Acc_inv ACC (floor_log2_proof H)))
  end.

このとき、以下の一見自明に見える定理はby []やreflexivityだけでは証明できません。

Theorem floor_log2E n (ACC : Acc lt n) :
  floor_log2 n ACC =
    match le_lt_dec n 1 with
    | left _ => 0
    | right H => S (floor_log2 (n / 2) (Acc_inv ACC (floor_log2_proof H)))
    end.
Proof.
Fail by [].
Admitted.

ACCを分解すると証明ができます。

Theorem floor_log2E_retry n (ACC : Acc lt n) :
  floor_log2 n ACC =
    match le_lt_dec n 1 with
    | left _ => 0
    | right H => S (floor_log2 (n / 2) (Acc_inv ACC (floor_log2_proof H)))
    end.
Proof.
case: ACC => ?.
by [].
Qed.

なぜ分解すると証明がうまくいくのか調べたところ、Rocq の reference manual で以下の記述を見つけました。

In order to keep the strong normalization property, the fixed point reduction will only be performed when the argument in position of the decreasing argument (which type should be in an inductive definition) starts with a constructor.

(Inductive types and recursive functions — The Rocq Prover 9.0.1 documentationから引用。閲覧日: 2025年10月27日)

この記述によると、再帰関数の適用は decreasing argument (関数の停止性を保証する呼び出しのたびに小さくなる引数)がコンストラクタでないと評価が進まないそうです。

同様の記述がhttps://rocq-prover.org/doc/v9.0/refman/language/core/inductive.html#reduction-ruleでも確認できます。

floor_log2の decreasing argument はACCです。なので、ACCを分解してコンストラクタの形で表さないと評価が進まないということのようです。

分かってしまえば何と言うことはないのですが、こういう挙動に関する記述を探すのは意外と苦労するのでメモしておきます。

  1. 定義の方法はXavier Leroy, “Well-founded recursion done right”を参考にしています。この資料では整礎関係に基づく再帰関数を定義するとてもシンプルな方法が紹介されています。 ↩︎