Свидетельства о членстве для деревьев AVL

Question

Я немного борюсь с представлением о доказательстве принадлежности для Data.AVL деревьев. Я хотел бы иметь возможность передавать значение типа n ∈ m, чтобы означать, что n появляется в качестве ключа в дереве AVL, так что при таком доказательстве get n m всегда может успешно присвоить значение, связанное с n. Вы можете предположить, что мои деревья AVL всегда содержат значения, полученные из полурешетки соединения (A, ∨, ⊥) над сетоидом (A, ≈), хотя под идемпотенцией остается неявным.

module Temp where 

open import Algebra.FunctionProperties 
open import Algebra.Structures renaming (IsCommutativeMonoid to IsCM) 
open import Data.AVL 
open import Data.List 
open import Data.Nat hiding (_⊔_) 
import Data.Nat.Properties as ℕ-Prop 
open import Data.Product hiding (_-×-_) 
open import Function 
open import Level 
open import Relation.Binary renaming (IsEquivalence to IsEq) 
open import Relation.Binary.PropositionalEquality 

module ℕ-AVL {v} (V : Set v) 
    = Data.AVL (const V) (StrictTotalOrder.isStrictTotalOrder ℕ-Prop.strictTotalOrder) 

data ≈-List {a ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) : Rel (List A) (a ⊔ ℓ) where 
    [] : ≈-List _≈_ [] [] 
    _∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys) 

_-×-_ : {a b c d ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → 
      REL A C ℓ₁ → REL B D ℓ₂ → A × B → C × D → Set (ℓ₁ ⊔ ℓ₂) 
(R -×- S) (a , b) (c , d) = R a c × S b d 

-- Two AVL trees are equal iff they have equal toList images. 
≈-AVL : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (ℕ-AVL.Tree A) (a ⊔ ℓ) 
≈-AVL _≈_ = ≈-List (_≡_ -×- _≈_) on (ℕ-AVL.toList _) 

_∈_ : {a ℓ : Level} {A : Set a} {_≈_ : Rel A ℓ} {_∨_ : Op₂ A} {⊥ : A} 
     {{_ : IsCM _≈_ _∨_ ⊥}} → ℕ → ℕ-AVL.Tree A → Set (a ⊔ ℓ) 
n ∈ m = {!!} 

get : {a ℓ : Level} {A : Set a} {_≈_ : Rel A ℓ} {_∨_ : Op₂ A} {⊥ : A} → 
     {{_ : IsCM _≈_ _∨_ ⊥}} → (n : ℕ) → (m : ℕ-AVL.Tree A) → n ∈ m → A 
get n m n∈m = {!!} 

Я чувствую, что это должно быть легко, но мне трудно. Одним из вариантов было бы использовать мое понятие эквивалентности для AVL-деревьев, в котором говорится, что два дерева равны, если они имеют одинаковое изображение toList и используют коммутативный моноид над A, определяющий

n ∈ m = ≈-AVL ≈ м (ℕ-AVL.unionWith _ ∨ м (ℕ-AVL.singleton _ п ⊥))

Это по существу говорит, что т содержит п тогда и только тогда одноплодной карте (п, ⊥) является "ниже" m в частичном порядке, индуцированном коммутативным моноидом (технически нам нужно, чтобы идемпотентность для этой интерпретации имела смысл). Однако, учитывая такое определение, я совсем не уверен, как реализовать get.

Я также экспериментировал с определением собственного индуктивного отношения, но обнаружил, что трудно, поскольку мне казалось, что я должен знать о сложных внутренних показателях, используемых Data.AVL.

Наконец, я также попытался использовать значение типа n ∈? m ≡ true, где ∈? определяется в Data.AVL, но также не имел большого успеха. Буду признателен за любые предложения.

Answer 1

Я думаю, что лучше всего определить _∈_ как индуктивное отношение. Да, это требует, чтобы вы знали внутренности Data.AVL, но я уверен, что это будет самое приятное представление для работы.

Внутренняя структура Data.AVL на самом деле довольно проста. У нас есть тип Indexed.Tree, который индексируется тремя значениями: нижней границей, верхней границей и высотой. Учитывая дерево t : Indexed.Tree lb ub h, все значения внутри t находятся в диапазоне (lb, ub).

Существует небольшое отклонение от этого: поскольку нам нужно иметь дерево, которое может содержать произвольные значения, нам необходимо искусственно расширить отношение _<_, заданное isStrictTotalOrder, с двумя новыми значениями - вы можете думать об этом как о отрицательном и положительная бесконечность. В модуле Data.AVL они называются ⊥⁺ и ⊤⁺. Деревья, которые могут содержать произвольные значения, тогда имеют тип Tree ⊥⁺ ⊤⁺ h.

Последний элемент - балансировка: каждый узел требует высоты своих поддеревьев не более чем на один уровень. На самом деле нам не нужно прикасаться к балансировке, но сигнатуры функций могут упоминать об этом.

В любом случае, я работаю непосредственно с этим необработанным (индексированным) вариантом.Непрозрачный, проиндексированные версия только что-то вроде:

data Tree : Set ? where 
    tree : ∀ {h} → Indexed.Tree ⊥⁺ ⊤⁺ h 

---

Некоторые шаблонного первый:

open import Data.Empty 
open import Data.Product 
open import Level 
open import Relation.Binary 
open import Relation.Binary.PropositionalEquality as P using (_≡_) 
open import Relation.Nullary 

import Data.AVL 

module Membership 
    {k v ℓ} 
    {Key : Set k} (Value : Key → Set v) 
    {_<_ : Rel Key ℓ} 
    (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where 

open Data.AVL Value isStrictTotalOrder public 
open Extended-key      public 
open Height-invariants     public 

open IsStrictTotalOrder isStrictTotalOrder 

Вот _∈_ как индуктивной связи:

data _∈_ {lb ub} (K : Key) : 
    ∀ {n} → Indexed.Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where 
    here : ∀ {hˡ hʳ} V 
    {l : Indexed.Tree lb [ K ] hˡ} 
    {r : Indexed.Tree [ K ] ub hʳ} 
    {b : hˡ ∼ hʳ} → 
    K ∈ Indexed.node (K , V) l r b 
    left : ∀ {hˡ hʳ K′} {V : Value K′} 
    {l : Indexed.Tree lb [ K′ ] hˡ} 
    {r : Indexed.Tree [ K′ ] ub hʳ} 
    {b : hˡ ∼ hʳ} → 
    K < K′ → 
    K ∈ l → 
    K ∈ Indexed.node (K′ , V) l r b 
    right : ∀ {hˡ hʳ K′} {V : Value K′} 
    {l : Indexed.Tree lb [ K′ ] hˡ} 
    {r : Indexed.Tree [ K′ ] ub hʳ} 
    {b : hˡ ∼ hʳ} → 
    K′ < K → 
    K ∈ r → 
    K ∈ Indexed.node (K′ , V) l r b 

Это своего рода индуктивного определения, которое вы ожидаете: либо ключ находится в этом внутреннем узле, либо он находится в одном из подпунктов деревья. Мы могли бы также обойтись без доказательств, но это более удобно - если вы хотите показать, что дерево делает , а не содержит определенный элемент, вам нужно только отслеживать путь lookup, а вместо этого поиска всего дерева.

Как интерпретировать эти l и r неявные аргументы? Обратите внимание, что это имеет смысл: у нас есть ключ K и, естественно, мы требуем, чтобы значения, содержащиеся в l осенью между lb и K (это на самом деле [ K ], так как мы используем расширенный _<_) и значения в r падения между K и ub , Балансировка (b : hˡ ∼ hʳ) существует только для того, чтобы мы могли построить фактический узел дерева.

Ваш get функция тогда очень просто:

get : ∀ {h lb ub n} {m : Indexed.Tree lb ub h} → n ∈ m → Value n 
get (here V) = V 
get (left _ p) = get p 
get (right _ p) = get p 

---

Ну, я сказал вам, что это представление довольно удобно работать, и я собираюсь доказать это. Одним из свойств, которые мы хотели _∈_ иметь это разрешимость: то есть, мы можем построить программу, которая говорит нам, принадлежит ли элемент в дереве или нет:

find : ∀ {h lb ub} n (m : Indexed.Tree lb ub h) → Dec (n ∈ m) 

find будет возвращать либо yes p, где p является доказательством того, что n находится внутри m (n ∈ m), или no ¬p, где ¬p является опровержением n ∈ m, n ∈ m → ⊥. Нам понадобится одна лемма:

lem : ∀ {lb ub hˡ hʳ K′ n} {V : Value K′} 
    {l : Indexed.Tree lb [ K′ ] hˡ} 
    {r : Indexed.Tree [ K′ ] ub hʳ} 
    {b : hˡ ∼ hʳ} → 
    n ∈ Indexed.node (K′ , V) l r b → 
    (n ≯ K′ → n ≢ K′ → n ∈ l) × (n ≮ K′ → n ≢ K′ → n ∈ r) 
lem (here V) = 
    (λ _ eq → ⊥-elim (eq P.refl)) , (λ _ eq → ⊥-elim (eq P.refl)) 
lem (left x p) = (λ _ _ → p) , (λ ≮ _ → ⊥-elim (≮ x)) 
lem (right x p) = (λ ≯ _ → ⊥-elim (≯ x)) , (λ _ _ → p) 

Это говорит нам о том, что если мы знаем, n содержится в t и мы знаем, n меньше, чем ключ корня t, то n должен быть в левом поддереве (и аналогично для правого поддерева).

Вот реализация find функции:

find : ∀ {h lb ub} n (m : Indexed.Tree lb ub h) → Dec (n ∈ m) 
find n (Indexed.leaf _) = no λ() 
find n (Indexed.node (k , v) l r _) with compare n k 
find n (Indexed.node (k , v) l r _) | tri< a ¬b ¬c with find n l 
... | yes p = yes (left a p) 
... | no ¬p = no λ ¬∈l → ¬p (proj₁ (lem ¬∈l) ¬c ¬b) 
find n (Indexed.node (k , v) l r _) | tri≈ ¬a b ¬c 
    rewrite (P.sym b) = yes (here v) 
find n (Indexed.node (k , v) l r _) | tri> ¬a ¬b c with find n r 
... | yes p = yes (right c p) 
... | no ¬p = no λ ¬∈r → ¬p (proj₂ (lem ¬∈r) ¬a ¬b) 

Реализация довольно проста, но я хотел бы предложить загружая его в Emacs, пытаясь заменить некоторые из правой руки сторон с отверстиями и посмотреть, что типы. И, наконец, вот несколько тестов:

open import Data.Nat 
open import Data.Nat.Properties 

open Membership 
    (λ _ → ℕ) 
    (StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 

un-tree : Tree → ∃ λ h → Indexed.Tree ⊥⁺ ⊤⁺ h 
un-tree (tree t) = , t 

test : Indexed.Tree _ _ _ 
test = proj₂ (un-tree 
    (insert 5 55 (insert 7 77 (insert 4 44 empty)))) 

Extract : ∀ {p} {P : Set p} → Dec P → Set _ 
Extract {P = P} (yes _) = P 
Extract {P = P} (no _) = ¬ P 

extract : ∀ {p} {P : Set p} (d : Dec P) → Extract d 
extract (yes p) = p 
extract (no ¬p) = ¬p 

∈-test₁ : ¬ (2 ∈ test) 
∈-test₁ = extract (find 2 test) 

∈-test₂ : 4 ∈ test 
∈-test₂ = extract (find 4 test)