Agda：_≦_（または、バイナリ検索ツリーを実装する方法）を推測する方法

Question

Agdaと特にAgda標準ライブラリがまだ非常に新しい私に。私は、バイナリ検索ツリーの概念を実装しようとしています。

Iは、二分木二分木から最大値と最小値を抽出

data BTree (A : Set) : ℕ → Set where 
    Leaf : A → BTree A 1 
    Node : ∀ {n m} → A → BTree A n → BTree A m → BTree A (1 + n + m) 

ならびに二つの機能bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕとbt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕの簡単な定義を有します。

私は今、特定のツリーがバイナリ検索ツリーであることを証明するデータ型を定義しようとしています。ここに私がこれまで持っているものがあります。

data BST : {n : ℕ} → BTree ℕ n → Set where 
    sortL : {x : ℕ} → BST (Leaf x) 
    sortN : ∀ {n m} → {a : ℕ} → {l : BTree ℕ n} → {r : BTree ℕ m} 
          → (sl : BST l) → (sr : BST r) 
          → {cl : a ≥ (bt-⊔ l)} → {cr : a < (bt-⊓ r)} 
          → BST (Node a l r) 

ノードBSTコンストラクタのための私の直感は、ノード（a）に格納された値、2つのサブツリー（lとr）、2つのサブツリーが分探索木（slとsr）と証明されている証明を取ることです現在の値aは、左側のサブツリーのすべてよりも大きく、右側のすべての値よりも小さい（clおよびcr）ことを確認してください。

これは多かれ少なかれ動作しているようで、次の単純なツリーとBSTプルーフを構築できます。

T₂ : BTree ℕ 3 
T₂ = Node 5 (Leaf 3) (Leaf 7) 

bst₂ : BST T₂ 
bst₂ = sortN sortL sortL {s≤s (s≤s (s≤s z≤n))} {s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))} 

はしかし、私は彼らが非常に面倒であるため、Agdaはclとcrのための証拠を推測したいです。もし私がbst₂の定義でそれらを指定しなければ、Agdaはコードに穴があると思って、clとcrに関連するアンダースコア変数を与えます。

これについてはどうすればいいのか分かりませんし、標準ライブラリのこの部分も正しく使用しているわけではありません。私はこれをもっと簡単にするための提案や解決策にはオープンです。

Answer 1

あなたは関数としてあまりまたは-等しい関係を定義することができます

open import Data.Empty 
open import Data.Unit.Base using (⊤; tt) 
open import Data.Nat.Base 

_≤⊤_ : ℕ -> ℕ -> Set 
0  ≤⊤ m  = ⊤ 
suc n ≤⊤ 0  = ⊥ 
suc n ≤⊤ suc m = n ≤⊤ m 

test : 10 ≤⊤ 20 
test = tt 

をそして、それは、元の証明を具体化することも可能です：

≤⊤→≤ : ∀ n m -> n ≤⊤ m -> n ≤ m 
≤⊤→≤ 0  m  _ = z≤n 
≤⊤→≤ (suc n) 0  () 
≤⊤→≤ (suc n) (suc m) p = s≤s (≤⊤→≤ n m p) 

test-test : 10 ≤ 20 
test-test = ≤⊤→≤ _ _ test 

test-testはs≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))に評価されます。二分木から最大値と最小値を抽出

ならびに二つの機能bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕとbt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ。

抽出するのではなく保存する方がいいです。順序付きデータ型を定義する方法について詳細に説明されているHow to Keep Your Neighbours in Orderの文書をチェックしてください（このコードのコードはAgdaの最新バージョンでタイプチェックしません。一部のヒントhereを参照してください）。

しかし、私は彼ら が非常に面倒であるため、Agdaはclとcrのための証拠を推測したいです。

これらのsortNおよびsortLも面倒です。

open import Relation.Nullary 

ordered? : ∀ {n} -> (b : BTree ℕ n) -> Dec (BST b) 
ordered? = ... 

ordered?はツリーが注文されているかどうかを決定する定義することが可能なはずです。その後、のヘルプをRelation.Nullary.Decidable.from-yesから削除することができます。しかし、まず論文を読み、BSTのより適切な表現を選択してください。