Agda 和二叉搜索树

Question

请注意，这是一个作业，所以最好不要发布完整的解决方案，相反，我只是卡住了，需要一些关于我接下来应该看什么的提示。

module BST where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)


data Ord (n m : ℕ) : Set where
  smaller : n < m -> Ord n m
  equal   : n ≡ m -> Ord n m
  greater : n > m -> Ord n m

cmp : (n m : ℕ) -> Ord n m
cmp zero zero       = equal refl
cmp zero (suc n)    = smaller (s≤s z≤n)
cmp (suc n) zero    = greater (s≤s z≤n)
cmp (suc n) (suc m) with cmp n m 
... | smaller n<m-pf = smaller (s≤s n<m-pf)
... | equal   n≡m-pf = equal (cong suc n≡m-pf)
... | greater n>m-pf = greater (s≤s n>m-pf)


-- To keep it simple and to exclude duplicates,
-- the BST can only store [1..]
--
data BST (min max : ℕ) : Set where
  branch : (v : ℕ)
         → BST min v → BST v max 
         → BST min max
  leaf   : min < max -> BST min max

这些已经导入：

≤-refl : ∀ {a} → a ≤ a 

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c 

我们需要实现这个扩大BST范围的功能：

widen : ∀{min max newMin newMax}
      → BST min max
      → newMin ≤ min
      → max ≤ newMax
      → BST newMin newMax

到目前为止我有这个：

widen : ∀{min max newMin newMax}
      → BST min max
      → newMin ≤ min
      → max ≤ newMax
      → BST newMin newMax
widen (leaf min<max-pf) newMin<min-pf max<newMax-pf = BST newMin<min-pf max<newMax-pf
widen (branch v l r) newMin<min-pf max<newMax = branch v 
                                                (widen l newMin<min-pf max<newMax) 
                                                (widen r newMin<min-pf max<newMax)

现在这显然不起作用，因为新边界不必严格小于/大于最小值/最大值。给出了一个提示：It is not strictly necessary, but you may find it helpful to implement an auxiliary function that widens the range of a strictly smaller than relation of the form min < max. 这就是我在这里所做的，显然我需要改变一些事情，但我认为基本的想法就在那里。

这就是我所在的地方，我只是真的不知道从哪里开始，我已经做了尽可能多的研究，但是没有很多阅读材料可供使用阿格达。我是否可能需要使用 ≤-refl 或 ≤-trans？

Answer 1

这里的棘手部分是了解widen 函数实际需要更改的内容。一旦你明白了，编写代码就相当容易了。

让我们从leaf 部分开始，我们有：

widen (leaf min<max) newMin≤min max≤newMax = {! !}

leaf min<max 的类型为 BST min max。应用widen 后，我们希望树的类型为BST newMin newMax - 这意味着我们必须将证明min < max 更改为newMin < newMax。

幸运的是，我们知道 newMin ≤ min 和 max ≤ newMax。 ≤ 是可传递的（它源于≤ 在ℕ 上形成一个总顺序的事实）并且很容易遵循newMin ≤ newMax - 这很好，但我们必须告诉Agda。

这就是≤-trans 发挥作用的地方。回想一下：

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c

这就是传递性的定义！正是我们正在寻找的。 （相当小的）问题是我们的证明使用< 和≤。如果他们没有

trans-4 : ∀ {a b c d} → a ≤ b → b ≤ c → c ≤ d → a ≤ d

写起来会很容易（你只需要应用≤-trans 两次）。您可能想实际编写此函数，它将帮助您完成下一部分。

我们知道a ≤ b (newMin ≤ min) 和c ≤ d (max ≤ newMax)，但我们只知道b < c - 我们不能只应用≤-trans 两次。查看Data.Nat，我们发现

_<_ : Rel ℕ Level.zero
m < n = suc m ≤ n

所以我们真正想写的是这样的：

trans-4 : ∀ {a b c d} → a ≤ b → suc b ≤ c → c ≤ d → suc a ≤ d

这有点难，所以让我们把它分成两个步骤。我们需要证明：

trans₁ : ∀ {a b c} → a ≤ b → suc b ≤ c → suc a ≤ c -- a ≤ b → b < c → a < c
trans₂ : ∀ {a b c} → suc a ≤ b → b ≤ c → suc a ≤ c -- a < b → b ≤ c → a < c

如果我们有suc a ≤ suc b 而不仅仅是a ≤ b，我们可以使用≤-trans。但我们可以得到它！如果a ≤ b，那么肯定是a + 1 ≤ b + 1。再次快速浏览标准库：

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

我把剩下的留作练习。一旦知道newMin < newMax，重构leaf 中的证明就变得很简单了。

---

branch 部分实际上在 Agda 中更容易编写，当然，棘手的部分是弄清楚我们需要更改哪些证明。

我们有：

widen (branch v l r) newMin≤min max≤newMax = {! !}

同样，branch v l r 的类型为 BST min max，我们需要 BST newMin newMax。正如您所注意到的，我们需要创建一个新分支并递归扩展l 和r。

如果我们想递归应用widen，我们最好检查l和r的类型：

l : BST min v
r : BST v max

因为这个答案已经比较长了，我来讨论l子树，其他情况是对称的。

问题当然是如果我们将widen应用到l，我们还需要提供两个新的证明。 min 没有改变，所以我们可以将newMin≤min 作为第一个传递。第二个呢？我们不能再给它max≤newMax，因为我们的子树是BST min v而不是BST min max。

我们的最终树必须看起来像BST newMin newMax，并且我们知道它必须包含v。这为我们提供了一种扩展左子树类型的选择 - BST newMin v。

这是什么意思？因此，第二个证明的类型是v ≤ v，从这里很容易！

编码愉快！