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)

以及两个函数 bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ 和 bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ，它们从二叉树中提取最大值和最小值。

我现在正在尝试定义一种数据类型来证明特定树是二叉搜索树。这是我目前所拥有的。

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 和 cr).

这似乎或多或少的工作，我可以构造以下简单树和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.[=28= 相关的下划线变量]

我不清楚该怎么做，也不清楚我是否正确使用了标准库的这一部分。我愿意接受任何可以使这更容易的建议或解决方案。

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

test-test 计算结果为 s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))).

as well as two functions bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ and bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ which extract the maximum and minimum values from a binary tree.

存储它们比提取它们更好。检查 How to Keep Your Neighbours in Order paper which in great details explains how to define ordered data types (the code in the paper doesn't type check with recent versions of Agda, see some tips ).

However, I want to have Agda infer the proofs for cl and cr since they are extremely tedious.

这些sortN和sortL也很乏味。应该可以定义

open import Relation.Nullary

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

ordered?决定一棵树是否有序。然后你可以在Relation.Nullary.Decidable.from-yes的帮助下消除这个Dec。但是先阅读论文并选择更合适的表示 BST.

Agda：如何推断 _≤_ 的证明（或者，如何实现二叉搜索树）

Agda: How to infer proof of _≤_ (or, how to implement a binary search tree)

agda

dependent-type