Агда и двоичные поисковые деревья

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) 

Теперь это, очевидно, d потому что новые границы не должны быть строго меньше/больше min/max. Подсказка была дана: 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

Трудная часть здесь понимает, что функция 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 - это хорошо и все, но мы должны сказать об этом Агда.

Здесь ≤-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, и это легко!

Счастливое кодирование!