noConfusion は帰納法の原理から従う

[Seasawher]

Lean において、Nat の noConfusion （コンストラクタは単射）は、rec （帰納法）から示すことができますか？

はい。しかも Nat.succ の単射性だけなら、帰納法の仮定は必要なく、Nat.rec で前者関数を作るだけで示せます。

Lean の Nat.rec は、論理的には帰納法の原理、計算的には原始再帰の原理です。コンストラクタに適用された rec はι簡約によって対応する場合へ計算されます。

private def predRec : Nat → Nat :=
Nat.rec
(motive := fun _ => Nat)
0
(fun n _ih => n)
theorem succ_injective_from_rec {m n : Nat}
(h : Nat.succ m = Nat.succ n) : m = n := by
exact congrArg predRec h

ここでは定義的に

predRec 0 = 0
predRec (Nat.succ n) = n

となります。したがって

h : Nat.succ m = Nat.succ n

の両辺に predRec を適用すると、

congrArg predRec h :
predRec (Nat.succ m) = predRec (Nat.succ n)

すなわち定義的に

m = n

が得られます。

コンストラクタの非交差性も rec から示せる

厳密には noConfusion は単射性だけでなく、

0 ≠ Nat.succ n
Nat.succ n ≠ 0

という異なるコンストラクタ同士の非交差性も含みます。公式リファレンスでも、noConfusion はコンストラクタの単射性と非交差性を導く一般的な命題だと説明されています。

これも Nat.rec から作れます。

private def IsZeroRec : Nat → Prop :=
Nat.rec
(motive := fun _ => Prop)
True
(fun _ _ih => False)
theorem zero_ne_succ_from_rec (n : Nat) :
0 ≠ Nat.succ n := by
intro h
have hz : IsZeroRec 0 :=
True.intro
exact h ▸ hz

IsZeroRec 0 は定義的に True、IsZeroRec (Nat.succ n) は定義的に False です。したがって 0 = Nat.succ n なら、等式による輸送によって True の証明から False の証明が得られてしまいます。

結論

Nat.noConfusion の内容は、次のものから導出できます。

1. Nat.rec の除去・計算規則
2. 等式の除去規則 Eq.rec
   Lean上では congrArg や ▸ として使用

したがって「Nat.rec だけから」というより、正確には

Nat.rec と等式の通常の除去規則から Nat.noConfusion を構成できる

となります。Lean自身も、帰納型の recursor に基づく補助構成として noConfusion と noConfusionType を生成しています。