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

这就是我所处的位置，我只是真的不知道从这里去哪里，我已经做了尽可能多的研究，但是没有很多关于使用 Agda 的阅读材料。我是否可能需要使用 ≤-refl 或 ≤-trans？

Answer 1