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