将二进制值类型加一
Increment binary value type by one
我想将二进制值加一，但我仍然不太熟悉 agda 中的递归工作原理。
为什么我在这里没有得到正确的输出？
Bin 类型定义
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
我的增量函数
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = ⟨⟩ I
inc (x I) = (inc x) I
快速修正你的算法
你的增量函数不正确。考虑到您对二进制数的定义：
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
你的自增函数应该这样写：
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
当右边的数字为零时，你只需要将其替换为一个，但一定不要忘记保留数字的左边部分。
当右边的数是1的时候，左边的部分要一直递增，但是还要把这个1变成0。
新算法的快速验证
但是，不要相信我的话，让我们尝试（部分）验证我们的功能。毕竟，我们在证明助手中，不是吗？
验证此类功能的一个好方法是评估它应该提供哪些 属性。增量函数的结果必须等于 1 加上它的输入值。 Agda 提供自然数，所以让我们将您的二进制数转换为自然数来检查这样的 属性。首先，一些导入：
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
然后是一个将二进制数转换为自然数的函数：
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
最后，我们的验证属性:
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
此验证当然是不完整的（本质上），但至少它让您对您的算法充满信心。在编写算法时，您应该始终尝试并证明这些假设，这是 Agda 的重点（好吧，不是全部，但至少是其中的一部分）。
关于验证的更多信息
为了进一步阐明我的观点，我决定通过实施从自然数到二进制数的倒数转换来尝试并继续验证您对二进制数的表示：
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
我们可以直接证明这两个变换在上升和下降时是互反的：
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
然后我尝试反过来做：
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
这边需要prop₂，签名如下：
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
这个属性应该是真的（在我们认为的二进制数应该满足它的意义上），但它无法在你的形式主义中被证明，因为你可以在无限多的数字中表示零方式，并且所有这些方式都不是介词相等的（例如，当 n 等于 0 时 prop₂ 的第一种情况需要证明无法证明的 ⟨⟩ ≡ (⟨⟩ O) ） .
总而言之，验证不仅可以让我们找到错误的算法（或证明算法是正确的），还可以揭示我们理论本身基础的不一致或错误（即使在这种情况下，快速浏览一下足以看出 0 可以表示无数种不同的方式）。
作为旁注，我并不是说应该总是有一种方法来表示抽象数据类型的特定元素，但它确实有帮助，尤其是在使用命题相等性时，这通常是必需的.
另一方面，如果我有点忘乎所以，我很抱歉，但我发现这类主题对于使用证明助手和形式验证非常有启发性。
请随时询问任何进一步的解释。
完整（在某种程度上是不完整的）代码
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
prop₂ {zero} = {!!}
prop₂ {suc n} = {!!}
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
标准库
最后一点，二进制数存在于文件 Data.Nat.Binary.Base 的标准库中，相关属性（特别是在您的表示中无法证明的互惠属性）在文件 Data.Nat.Binary.Properties 如果您想看看它们是如何在那里实现的。
当我们将 inc 定义为 Bin → Bin 时，我们是说它采用 Bin 类型的值和相同类型的 returns 值，即 Bin。
由于我们有 3 个构造函数可用于创建 Bin，因此 Bin 类型的所有值都将具有以下 3 种形式之一：
- ⟨⟩
- b I 其中 b 是 Bin 类型的某个值
- b O 其中 b 是 Bin 类型的某个值
对于情况 1，因为 ⟨⟩ 代表零。
inc ⟨⟩ = ⟨⟩ I
对于情况 2，我们知道将 1 加到以 0 结尾的数字只会将最后一位数字更改为 1，所以
inc (x O) = x I
对于情况 3，当数字以 1 结尾时，在递增它时我们在末尾得到零，并且生成需要向前传递的结转。可以使用我们相同的 inc 函数传递结转。假设 (inc x) 给出一个二进制数，我们获取该输出并在末尾附加零。
inc (x I) = (inc x) O
此外，只是为了扩展 MrO 给出的出色答案，他正确地指出，因为有无限多种方式来表示零（和所有数字）
(b ↓) ↑ = b
无法证明第一个有效数字前有前导零的 b。但是，如果我们将 ↓↑ 的域限制为仅规范的二进制数，即没有任何前导零的二进制数，则可以得出证明。
(b ↓) ↑ = b 对于规范 b
的证明
扩展 MrO 的代码，
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩ O
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
-- One b -> b start with ⟨⟩ I
data One : Bin → Set where
first : One (⟨⟩ I)
nextO : ∀ { b : Bin }
→ One b
------------
→ One (b O)
nextI : ∀ { b : Bin }
→ One b
------------
→ One (b I)
-- Can i.e Canonical representing binary numbers without extras leading zeros after ⟨⟩. For e.g ⟨⟩ O O I I and ⟨⟩ I I both represents binary form of number 3 but only ⟨⟩ I I is the canonical
data Can : Bin → Set where
startWithZero : Can (⟨⟩ O)
startWithOne : ∀ {b : Bin }
→ One b
------------
→ Can b
-- If m ≤ n then m ≤ (n + 1)
≤-sucʳ : ∀ {m n : ℕ }
→ m ≤ n
-----------
→ m ≤ suc n
≤-sucʳ z≤n = z≤n
≤-sucʳ (s≤s m≤n) = s≤s (≤-sucʳ m≤n)
-- If m ≤ n then m ≤ (n + p)
≤-addʳ : ∀ (m n p : ℕ)
→ m ≤ n
--------
→ m ≤ n + p
≤-addʳ m n zero m≤n rewrite +-comm n zero = m≤n
≤-addʳ m n (suc p) m≤n rewrite +-comm n (suc p) | +-comm p n = ≤-sucʳ (≤-addʳ m n p m≤n)
-- If a natural number n has eqivalent binary form (⟨⟩ I b) then 1 ≤ n
1-≤-oneb : ∀ { b : Bin }
→ One b
---------
→ suc zero ≤ b ↑
1-≤-oneb first = s≤s z≤n
1-≤-oneb {b O} (nextO oneb) = ≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb)
1-≤-oneb {b I} (nextI oneb) = ≤-sucʳ (≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb))
-- If 0 ≤ (n + 1) then 1 ≤ n
0-≤-suc : ∀ (n : ℕ)
→ 0 ≤ suc n
-----------
→ 1 ≤ suc n
0-≤-suc n z≤n = s≤s z≤n
-- If 1 ≤ n and binary form of n is b then binary form of (n + n) using ↓ is b O
↓-over-+ : ∀ (n : ℕ)
→ 1 ≤ n
-----------------------
→ (n + n) ↓ ≡ (n ↓) O
↓-over-+ (suc zero) s≤n = refl
↓-over-+ (suc (suc n)) (s≤s s≤n) = begin
(suc (suc n) + (suc (suc n))) ↓
≡⟨⟩
inc (( suc n + (suc (suc n))) ↓)
≡⟨ cong (inc) (cong (_↓) (+-comm (suc n) (suc (suc n)))) ⟩
inc (inc ((suc n + suc n) ↓))
≡⟨ cong (inc) (cong inc (↓-over-+ (suc n) (0-≤-suc n s≤n))) ⟩
refl
-- For all binary numbers that are canonical, ↑↓ is identity (returns same b)
↑↓-canb : ∀ ( b : Bin )
→ Can b
--------------
→ (b ↑) ↓ ≡ b
↑↓-canb _ startWithZero = refl
↑↓-canb _ (startWithOne first) = refl
↑↓-canb (b O) (startWithOne (nextO x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
↑↓-canb (b I) (startWithOne (nextI x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
我想将二进制值加一，但我仍然不太熟悉 agda 中的递归工作原理。
为什么我在这里没有得到正确的输出？
Bin 类型定义
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
我的增量函数
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = ⟨⟩ I
inc (x I) = (inc x) I
快速修正你的算法
你的增量函数不正确。考虑到您对二进制数的定义：
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
你的自增函数应该这样写：
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
当右边的数字为零时，你只需要将其替换为一个，但一定不要忘记保留数字的左边部分。
当右边的数是1的时候，左边的部分要一直递增，但是还要把这个1变成0。
新算法的快速验证
但是，不要相信我的话，让我们尝试（部分）验证我们的功能。毕竟，我们在证明助手中，不是吗？
验证此类功能的一个好方法是评估它应该提供哪些 属性。增量函数的结果必须等于 1 加上它的输入值。 Agda 提供自然数，所以让我们将您的二进制数转换为自然数来检查这样的 属性。首先，一些导入：
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
然后是一个将二进制数转换为自然数的函数：
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
最后，我们的验证属性:
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
此验证当然是不完整的（本质上），但至少它让您对您的算法充满信心。在编写算法时，您应该始终尝试并证明这些假设，这是 Agda 的重点（好吧，不是全部，但至少是其中的一部分）。
关于验证的更多信息
为了进一步阐明我的观点，我决定通过实施从自然数到二进制数的倒数转换来尝试并继续验证您对二进制数的表示：
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
我们可以直接证明这两个变换在上升和下降时是互反的：
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
然后我尝试反过来做：
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
这边需要prop₂，签名如下：
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
这个属性应该是真的（在我们认为的二进制数应该满足它的意义上），但它无法在你的形式主义中被证明，因为你可以在无限多的数字中表示零方式，并且所有这些方式都不是介词相等的（例如，当 n 等于 0 时 prop₂ 的第一种情况需要证明无法证明的 ⟨⟩ ≡ (⟨⟩ O) ） .
总而言之，验证不仅可以让我们找到错误的算法（或证明算法是正确的），还可以揭示我们理论本身基础的不一致或错误（即使在这种情况下，快速浏览一下足以看出 0 可以表示无数种不同的方式）。
作为旁注，我并不是说应该总是有一种方法来表示抽象数据类型的特定元素，但它确实有帮助，尤其是在使用命题相等性时，这通常是必需的.
另一方面，如果我有点忘乎所以，我很抱歉，但我发现这类主题对于使用证明助手和形式验证非常有启发性。
请随时询问任何进一步的解释。
完整（在某种程度上是不完整的）代码
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
prop₂ {zero} = {!!}
prop₂ {suc n} = {!!}
↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
标准库
最后一点，二进制数存在于文件 Data.Nat.Binary.Base 的标准库中，相关属性（特别是在您的表示中无法证明的互惠属性）在文件 Data.Nat.Binary.Properties 如果您想看看它们是如何在那里实现的。
当我们将 inc 定义为 Bin → Bin 时，我们是说它采用 Bin 类型的值和相同类型的 returns 值，即 Bin。
由于我们有 3 个构造函数可用于创建 Bin，因此 Bin 类型的所有值都将具有以下 3 种形式之一：
- ⟨⟩
- b I 其中 b 是 Bin 类型的某个值
- b O 其中 b 是 Bin 类型的某个值
对于情况 1，因为 ⟨⟩ 代表零。
inc ⟨⟩ = ⟨⟩ I
对于情况 2，我们知道将 1 加到以 0 结尾的数字只会将最后一位数字更改为 1，所以
inc (x O) = x I
对于情况 3，当数字以 1 结尾时，在递增它时我们在末尾得到零，并且生成需要向前传递的结转。可以使用我们相同的 inc 函数传递结转。假设 (inc x) 给出一个二进制数，我们获取该输出并在末尾附加零。
inc (x I) = (inc x) O
此外，只是为了扩展 MrO 给出的出色答案，他正确地指出，因为有无限多种方式来表示零（和所有数字）
(b ↓) ↑ = b
无法证明第一个有效数字前有前导零的 b。但是，如果我们将 ↓↑ 的域限制为仅规范的二进制数，即没有任何前导零的二进制数，则可以得出证明。
(b ↓) ↑ = b 对于规范 b
的证明扩展 MrO 的代码，
module BinaryNumber where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O
_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)
prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl
_↓ : ℕ → Bin
zero ↓ = ⟨⟩ O
suc n ↓ = inc (n ↓)
↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl
-- One b -> b start with ⟨⟩ I
data One : Bin → Set where
first : One (⟨⟩ I)
nextO : ∀ { b : Bin }
→ One b
------------
→ One (b O)
nextI : ∀ { b : Bin }
→ One b
------------
→ One (b I)
-- Can i.e Canonical representing binary numbers without extras leading zeros after ⟨⟩. For e.g ⟨⟩ O O I I and ⟨⟩ I I both represents binary form of number 3 but only ⟨⟩ I I is the canonical
data Can : Bin → Set where
startWithZero : Can (⟨⟩ O)
startWithOne : ∀ {b : Bin }
→ One b
------------
→ Can b
-- If m ≤ n then m ≤ (n + 1)
≤-sucʳ : ∀ {m n : ℕ }
→ m ≤ n
-----------
→ m ≤ suc n
≤-sucʳ z≤n = z≤n
≤-sucʳ (s≤s m≤n) = s≤s (≤-sucʳ m≤n)
-- If m ≤ n then m ≤ (n + p)
≤-addʳ : ∀ (m n p : ℕ)
→ m ≤ n
--------
→ m ≤ n + p
≤-addʳ m n zero m≤n rewrite +-comm n zero = m≤n
≤-addʳ m n (suc p) m≤n rewrite +-comm n (suc p) | +-comm p n = ≤-sucʳ (≤-addʳ m n p m≤n)
-- If a natural number n has eqivalent binary form (⟨⟩ I b) then 1 ≤ n
1-≤-oneb : ∀ { b : Bin }
→ One b
---------
→ suc zero ≤ b ↑
1-≤-oneb first = s≤s z≤n
1-≤-oneb {b O} (nextO oneb) = ≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb)
1-≤-oneb {b I} (nextI oneb) = ≤-sucʳ (≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb))
-- If 0 ≤ (n + 1) then 1 ≤ n
0-≤-suc : ∀ (n : ℕ)
→ 0 ≤ suc n
-----------
→ 1 ≤ suc n
0-≤-suc n z≤n = s≤s z≤n
-- If 1 ≤ n and binary form of n is b then binary form of (n + n) using ↓ is b O
↓-over-+ : ∀ (n : ℕ)
→ 1 ≤ n
-----------------------
→ (n + n) ↓ ≡ (n ↓) O
↓-over-+ (suc zero) s≤n = refl
↓-over-+ (suc (suc n)) (s≤s s≤n) = begin
(suc (suc n) + (suc (suc n))) ↓
≡⟨⟩
inc (( suc n + (suc (suc n))) ↓)
≡⟨ cong (inc) (cong (_↓) (+-comm (suc n) (suc (suc n)))) ⟩
inc (inc ((suc n + suc n) ↓))
≡⟨ cong (inc) (cong inc (↓-over-+ (suc n) (0-≤-suc n s≤n))) ⟩
refl
-- For all binary numbers that are canonical, ↑↓ is identity (returns same b)
↑↓-canb : ∀ ( b : Bin )
→ Can b
--------------
→ (b ↑) ↓ ≡ b
↑↓-canb _ startWithZero = refl
↑↓-canb _ (startWithOne first) = refl
↑↓-canb (b O) (startWithOne (nextO x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
↑↓-canb (b I) (startWithOne (nextI x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl