关于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)

为了证明类似 "the one is in the Image of the successor function" 我写道：

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

我想要以下内容。

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

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

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

Answer 1

Image f ∋ y 读作 "there is some x such that 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 是一个 "irrefutable pattern"，即它说“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。

关于succ函数的形象

About the image of the succ function

agda