AVL树的成员证明
我正努力想出一个关于Data.AVL树成员资格证明的概念。我希望能够传递一个n ∈ m类型的值，这意味着n在AVL树中显示为一个键，这样get n m就可以成功地产生一个与n相关的值。您可以假设我的AVL树总是包含从一个连接半格(A，≈)上提取的值，尽管在idempotence下面是左隐式的。
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≈m(ℕ-AVL AVL.unionWith_∨m(ℕ-AVL AVL.singleton_n⊥))
这实质上说m包含n当且仅当单例映射(n，⊥)“低于”m是由交换幺半群引起的偏序(从技术上讲，我们需要幂等性才能使这种解释有意义)。但是，考虑到这样的定义，我根本不确定如何实现get。
我也尝试过定义我自己的归纳Data.AVL关系，但是我发现虽然我最终不得不知道∈所使用的复杂的内部索引，但这是很困难的。
最后，我还尝试使用一个类型为n ∈? m ≡ true的值，∈在哪里？是用Data.AVL定义的，但在那里也没有取得多大的成功。如有任何建议，我将不胜感激。
回答 1
Stack Overflow用户
发布于 2014-01-13 03:58:57
我认为你最好的选择是将_∈_定义为一种归纳关系。是的，这要求您了解Data.AVL的内部结构，但我确信这将是最适合使用的表示形式。
Data.AVL的内部结构实际上相当简单。我们有一个类型Indexed.Tree，它由三个值索引:下界、上界和高度。给定一个树t : Indexed.Tree lb ub h，t中的所有值都在(lb, ub)范围内。
但是，它有一个细微的转折:因为我们需要一棵可以包含任意值的树，我们需要人为地用两个新值扩展isStrictTotalOrder给出的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)https://stackoverflow.com/questions/21081583
复制相似问题
腾讯云开发者
