agda - 关于succ函数的形象

Question

我通常这样定义自然数:

data Nat : Set where
  zero : Nat
  succ : Nat → Nat

也就是说，第一应该是

one : Nat 
one = succ zero

稍后，我们可以定义图像数据类型，

data Image_∋_ {A B : Set} (f : A → B) : B -> Set where
  im : (x : A) → Image f ∋ (f x)

为了证明“那个在后继函数的图像中”之类的东西，我写道:

one-succ : Image succ ∋ one
one-succ  = im zero

我想要以下内容。

• 定义不允许零作为其后继函数输入的前驱函数。所以下一个无效。

pred : Nat → Nat
pred zero  = zero
pred (succ n) = n

• 我想要一个名为 Z⁺ 的变量，表示正数，但在其定义中使用后继函数的图像(上面定义的 Image_∋_ 数据类型)。

Answer 1

图像 f ∋ y 读作“存在一些 x 使得 y ≡ f x”。 im x 对 Image f ∋ y 的模式匹配揭示了 x。

因此 Image succ ∋ n 类型的元素证明 n 的形式为 succ m 其中 m 包含在该元素内。因此定义很简单

ipred : ∀ {n} → Image succ ∋ n → Nat
ipred (im m) = m

因为n ≡ succ m 而succ m的前身是m。

如果我们将 im 重命名为 isucc 会更好读:

open Image_∋_ renaming (im to isucc)

ipred : ∀ {n} → Image succ ∋ n → Nat
ipred (isucc m) = m

另一种写法是

data Image_∋_ {A B : Set} : (A → B) → B → Set where
  _·_ : (f : A → B) → (x : A) → Image f ∋ f x

pred : ∀ {n} → Image succ ∋ n → Nat
pred (.succ · m) = m

这里 Image f ∋ y 中的 f 是一个索引而不是参数，所以 _·_ (之前是 im) 现在接收两个参数:一个函数及其参数。不可能在函数上进行模式匹配，但是 .succ 是一个“无可辩驳的模式”，即它说“f 可以什么都不是，但是 succ”。

---

Nat⁺ 可以定义为

data Nat⁺ : Set where
  nat⁺ : ∀ {n} → Image succ ∋ n → Nat⁺

succ⁺ 收到一个自然数(隐含地)和一个证明，该数字对于某些 m 是 succ m 的形式。

你总是可以取正自然数的前导:

pred⁺ : Nat⁺ → Nat
pred⁺ (nat⁺ (im m)) = m

但由于 Nat⁺ 是非索引的单构造数据类型，因此可以将其定义为记录:

record Nat⁺ : Set where
  constructor nat⁺
  field
    {pred⁺} : Nat
    image   : Image succ ∋ pred⁺
open Nat⁺

open Nat⁺ 在范围内引入 pred⁺ : Nat⁺ → Nat。