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-trees 的等价概念，它表示如果两棵树具有相同的toList 图像，则它们是相等的，并利用 A 上的可交换幺半群，定义

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

这实质上是说 m 包含 n 当且仅当单例映射 (n, ⊥) 在由可交换幺半群诱导的偏序中“低于” 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 ]，因为我们使用的是扩展的 @987654347 @) 和 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)