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.这就是我在这里所做的，显然我需要改变一些事情，但我认为基本的想法就在那里。

这就是我现在所处的位置，我只是真的不知道从这里该去哪里，我已经做了尽可能多的研究，但是没有大量的阅读 Material 可供使用 Agda 。我是否需要使用 ≤-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

我们可以使用≤-trans如果我们有suc a ≤ suc b而不仅仅是a ≤ b 。但我们可以得到它!如果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从这里开始很容易!

祝你编码愉快!