Agda:如何推断_≤_的证明(或者，如何实现二进制搜索树)

Question

我可能不会以最好的方式来做这件事，因为Agda，尤其是Agda标准库对我来说仍然很新。我正在尝试实现二进制搜索树的一些概念。

我对二叉树有一个简单的定义

data BTree (A : Set) : ℕ → Set where
  Leaf : A → BTree A 1
  Node : ∀ {n m} → A → BTree A n → BTree A m → BTree A (1 + n + m)

以及从二叉树中提取最大值和最小值的两个函数CCD_ 1和CCD_。

我现在正试图定义一种数据类型，它可以证明一个特定的树是一个二进制搜索树。这是我迄今为止所拥有的。

data BST : {n : ℕ} → BTree ℕ n → Set where
  sortL : {x : ℕ} → BST (Leaf x)
  sortN : ∀ {n m} → {a : ℕ} → {l : BTree ℕ n} → {r : BTree ℕ m}
                            → (sl : BST l) → (sr : BST r)
                            → {cl : a ≥ (bt-⊔ l)} → {cr : a < (bt-⊓ r)}
                            → BST (Node a l r)

我对节点BST构造函数的直觉是，取存储在节点（a）的值，两个子树（l和r），证明这两个子树是BST（sl和sr），并证明当前值a大于左子树中的所有值，小于右子树中的全部值（cl和bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ0）。

这似乎或多或少奏效了，我可以构建以下简单的树和BST证明。

T₂ : BTree ℕ 3
T₂ = Node 5 (Leaf 3) (Leaf 7)
bst₂ : BST T₂
bst₂ = sortN sortL sortL {s≤s (s≤s (s≤s z≤n))} {s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))}

然而，我想让Agda推断cl和cr的证明，因为它们非常乏味。如果我没有在bst₂的定义中指定它们，那么Agda似乎认为我的代码中有漏洞，给了我与cl和cr相关的下划线变量。

我不清楚该如何进行，也不清楚我是否正确使用了标准库的这一部分。我愿意接受任何能让这件事变得更容易的建议或解决方案。

Answer 1

您可以将小于或等于关系定义为一个函数：

open import Data.Empty
open import Data.Unit.Base using (⊤; tt)
open import Data.Nat.Base
_≤⊤_ : ℕ -> ℕ -> Set
0     ≤⊤ m     = ⊤
suc n ≤⊤ 0     = ⊥
suc n ≤⊤ suc m = n ≤⊤ m
test : 10 ≤⊤ 20
test = tt

还可以具体化原始证明：

≤⊤→≤ : ∀ n m -> n ≤⊤ m -> n ≤ m
≤⊤→≤  0       m      _  = z≤n
≤⊤→≤ (suc n)  0      ()
≤⊤→≤ (suc n) (suc m) p  = s≤s (≤⊤→≤ n m p)
test-test : 10 ≤ 20
test-test = ≤⊤→≤ _ _ test

CCD_ 16评估为CCD_。

以及提取最大值和最小值的两个函数CCD_ 18和CCD_从二叉树。

与其提取，不如储存它们。查看How to Keep Your Neighbours in Order论文，该论文详细解释了如何定义有序的数据类型（论文中的代码与最新版本的Agda不进行类型检查，请参阅此处的一些提示）。

然而，我想让Agda推断bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ0和cr的证明，因为它们非常乏味。

这些CCD_ 22和CCD_。应该可以定义

open import Relation.Nullary
ordered? : ∀ {n} -> (b : BTree ℕ n) -> Dec (BST b)
ordered? = ...

CCD_ 24决定树是否被排序。然后您可以在Relation.Nullary.Decidable.from-yes的帮助下消除此Dec。但请先阅读本文，然后选择一个更合适的BST表示。