请注意，这是一个作业，所以最好不要发布完整的解决方案，相反，我只是被卡住了，需要一些关于我接下来应该看什么的提示。
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.这就是我在这里所做的，显然我需要改变一些东西，但我认为基本的想法就在那里。
这就是我所处的位置，我真的不知道从哪里开始，我已经做了尽可能多的研究，但是没有很多关于使用 Agda 的阅读材料。我可能需要使用 ?-refl 或 ?-trans 吗？
这里棘手的部分是了解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
我们可以使用?-transif 我们有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，我们最好检查一下land的类型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很容易从这里开始！
快乐编码！