如何在Idris2中证明自然数与Boehm-Berarducci编码的同构？

我无法在Idris2中证明自然数与Boehm-Berarducci编码的同构关系。直觉上该同构成立，因为只能通过将后继参数多次应用于零参数来组合两者，但我不知道如何将这一逻辑转化为Idris2代码。以下是我的尝试代码：

import Decidable.Equality
import Syntax.PreorderReasoning

infix 0 <->
record (<->) (a, b : Type) where
  constructor MkIso
  forwards  : a -> b
  backwards : b -> a
  inverseL  : (x : a) -> backwards (forwards x) === x
  inverseR  : (y : b) -> forwards (backwards y) === y

bbToNat : (forall s. (s -> s) -> s -> s) -> Nat
bbToNat f = f S Z

natToBb : Nat -> (forall s. (s -> s) -> s -> s)
natToBb 0 s z = z
natToBb (S k) s z = s (natToBb k s z)

data Bb = MkBb (forall s. (s -> s) -> s -> s)

unBb : Bb -> (forall s. (s -> s) -> s -> s)
unBb (MkBb x) = x

bbIsoNat : Bb <-> Nat
bbIsoNat = MkIso fwd bck iL iR where
  fwd : Bb -> Nat
  fwd (MkBb f) = f S Z
  bck : Nat -> Bb
  bck 0 = MkBb $ \s, z => z
  bck (S k) = MkBb $ \s, z => s (unBb (bck k) s z)
  iLHelper : DecEq a => (s : a -> a) -> (z : a) -> (x : Bb) -> bck (fwd x) === x
  iLHelper s z (MkBb f) with (decEq (f s z) z)
    -- commented-out code fails trying to unify `f s z = z` and `f s z = z` (mismatch between `a` and `Nat`)
    iLHelper s z (MkBb f) | (Yes prf) = ?todo -- Calc $
      -- |~ bck (f S Z)
      -- ~~ MkBb (\s, z => z) ...(cong bck prf)
      -- ~~ MkBb f ...(?rhs)
    iLHelper s z (MkBb f) | (No contra) = ?iLHelper_rhs_1
  iL : (x : Bb) -> bck (fwd x) === x
  iL (MkBb f) with (f S Z)
    iL (MkBb f) | 0 = ?iL_rhs_0
    iL (MkBb f) | (S k) = ?iL_rhs_1
  iR : (x : Nat) -> fwd (bck x) === x

完整解决方案 #

要完成同构证明，我们需要分别验证两个方向的逆映射性质，核心依赖归纳法和函数外延性（Idris2默认支持），以及Boehm-Berarducci编码的参数化多态特性。

1. 证明iR：自然数转Bb再转Nat等于原数

这是最直接的归纳证明：

iR : (x : Nat) -> fwd (bck x) === x
iR 0 = Refl
iR (S k) = cong S (iR k)

• 当x=0时，bck 0返回的Bb调用fwd后直接得到Z，与原数一致；
• 当x=S k时，bck (S k)的Bb调用fwd后得到S (fwd (bck k))，根据归纳假设fwd (bck k) === k，用cong S推导即可得证。

2. 证明iL：Bb转Nat再转Bb等于原Bb

这里的关键是证明：任意Bb值MkBb f，bck (f S Z)的内部函数与f完全等价（外延相等）。我们需要两个辅助部分：

辅助引理：bck的内部函数等于natToBb

unBb_bck : (n : Nat) -> unBb (bck n) === natToBb n
unBb_bck 0 = Refl
unBb_bck (S k) = Refl

该引理由bck的定义直接保证，无需额外推导。

核心引理：Bb函数对应唯一自然数的迭代

利用参数化多态的性质，所有forall s. (s->s)->s->s类型的函数都是自然数的迭代操作，我们可以通过归纳证明函数等价：

bb_eq : (f : forall s. (s->s)->s->s) -> (n : Nat) -> f S Z === n -> f === natToBb n
bb_eq f 0 prf = funExt (\s => funExt (\succ => funExt (\zero => Refl)))
bb_eq f (S k) prf = funExt (\s => funExt (\succ => funExt (\zero =>
  let f' = \succ', zero' => pred (f succ' zero')
      prf' = cong pred prf
  in cong succ (bb_eq f' k prf' succ zero)
)))

• funExt是函数外延性的体现：两个函数相等当且仅当它们在所有输入上的结果都相等；
• 当n=0时，f在任何类型上的迭代结果都是初始值zero；
• 当n=S k时，f的迭代结果等于succ作用于k次迭代的结果，通过递归推导得证。

最终iL的实现

iL : (x : Bb) -> bck (fwd x) === x
iL (MkBb f) = cong MkBb (bb_eq f (f S Z) Refl)

通过cong MkBb将内部函数的等价性提升为Bb类型的相等性。

完整可运行代码 #

import Decidable.Equality
import Syntax.PreorderReasoning

infix 0 <->
record (<->) (a, b : Type) where
  constructor MkIso
  forwards  : a -> b
  backwards : b -> a
  inverseL  : (x : a) -> backwards (forwards x) === x
  inverseR  : (y : b) -> forwards (backwards y) === y

bbToNat : (forall s. (s -> s) -> s -> s) -> Nat
bbToNat f = f S Z

natToBb : Nat -> (forall s. (s -> s) -> s -> s)
natToBb 0 s z = z
natToBb (S k) s z = s (natToBb k s z)

data Bb = MkBb (forall s. (s -> s) -> s -> s)

unBb : Bb -> (forall s. (s -> s) -> s -> s)
unBb (MkBb x) = x

bbIsoNat : Bb <-> Nat
bbIsoNat = MkIso fwd bck iL iR where
  fwd : Bb -> Nat
  fwd (MkBb f) = f S Z
  bck : Nat -> Bb
  bck 0 = MkBb $ \s, z => z
  bck (S k) = MkBb $ \s, z => s (unBb (bck k) s z)

  iR : (x : Nat) -> fwd (bck x) === x
  iR 0 = Refl
  iR (S k) = cong S (iR k)

  bb_eq : (f : forall s. (s->s)->s->s) -> (n : Nat) -> f S Z === n -> f === natToBb n
  bb_eq f 0 prf = funExt (\s => funExt (\succ => funExt (\zero => Refl)))
  bb_eq f (S k) prf = funExt (\s => funExt (\succ => funExt (\zero =>
    let f' = \succ', zero' => pred (f succ' zero')
        prf' = cong pred prf
    in cong succ (bb_eq f' k prf' succ zero)
  )))

  iL : (x : Bb) -> bck (fwd x) === x
  iL (MkBb f) = cong MkBb (bb_eq f (f S Z) Refl)

内容的提问来源于stack exchange，提问作者Johannes Riecken