Mercurial > hg > Gears > GearsAgda

changeset 827:8ebf6fcc353b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add tr< and tr>
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Feb 2024 10:05:56 +0900
parents cfdb145f1581
children c9850c226195
files hoareBinaryTree1.agda
diffstat 1 files changed, 62 insertions(+), 67 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jan 29 18:15:54 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Feb 28 10:05:56 2024 +0900
@@ -41,43 +41,38 @@
 
 open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
 
+tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
+tr< {_} {A} key leaf = ⊤
+tr< {_} {A} key (node key₁ value tr tr₁) = key < key₁ → tr< key tr  ∧  tr< key tr₁
+
+tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
+tr> {_} {A} key leaf = ⊤
+tr> {_} {A} key (node key₁ value tr tr₁) = key₁ < key → tr> key tr  ∧  tr> key tr₁
+
 --
 --
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
     t-leaf : treeInvariant leaf
     t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
-    t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key₁ value₁ t₁ t₂)
+    t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ 
+       → tr< key t₁
+       → tr< key t₂
+       → treeInvariant (node key₁ value₁ t₁ t₂)
        → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
-    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key value t₁ t₂)
+    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ 
+       → tr> key t₁
+       → tr> key t₂
+       → treeInvariant (node key value t₁ t₂)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
     t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
+       → tr< key₁ t₁ 
+       → tr< key₁ t₂ 
+       → tr> key₁ t₃
+       → tr> key₁ t₄
        → treeInvariant (node key value t₁ t₂)
        → treeInvariant (node key₂ value₂ t₃ t₄)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
 
---
--- treeInvraiant is not enough to show that a tree is sorted
---
-max-key-in-left : {n : Level} {A : Set n} → (key : ℕ) → bt A → ℕ
-max-key-in-left {_} {A} key tr = ?
-
-min-key-in-right : {n : Level} {A : Set n} → (key : ℕ) →  bt A → ℕ
-min-key-in-right {_} {A} key tr = ?
-
-data treeInvariantSorted {n : Level} {A : Set n} : (tree : bt A) → Set n where
-    st-leaf : treeInvariantSorted leaf
-    st-single : (key : ℕ) → (value : A) →  treeInvariantSorted (node key value leaf leaf)
-    st-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariantSorted (node key₁ value₁ t₁ t₂)
-       → treeInvariantSorted (node key value leaf (node key₁ value₁ t₁ t₂))
-    st-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariantSorted (node key value t₁ t₂)
-       → treeInvariantSorted (node key₁ value₁ (node key value t₁ t₂) leaf )
-    st-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {left right : bt A} 
-       → (tl : treeInvariantSorted left )
-       → (tr : treeInvariantSorted right )
-       → max-key-in-left key left < key →  key < min-key-in-right key right 
-       → treeInvariantSorted (node key value₁ left right)
-
-
 
 --
 --  stack always contains original top at end (path of the tree)
@@ -108,7 +103,7 @@
 treeTest2  =  node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
 
 treeInvariantTest1  : treeInvariant treeTest1
-treeInvariantTest1  = t-right (m≤m+n _ 2) (t-node (add< 0) (add< 1) (t-left (add< 0) (t-single 1 7)) (t-single 5 5) )
+treeInvariantTest1  = t-right (m≤m+n _ 2) ? ? (t-node (add< 0) (add< 1) ? ? ? ? (t-left (add< 0) ? ? (t-single 1 7)) (t-single 5 5) )
 
 stack-top :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
 stack-top [] = nothing
@@ -200,17 +195,17 @@
       → treeInvariant (node k v1 tree tree₁)
       →      treeInvariant tree
 treeLeftDown {n} {A} {_} {v1} leaf leaf (t-single k1 v1) = t-leaf
-treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = t-leaf
-treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = ti
-treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti
+treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x _ _ ti) = t-leaf
+treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x _ _ ti) = ti
+treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ _ _ _ _ ti ti₁) = ti
 
 treeRightDown  : {n : Level} {A : Set n} {k : ℕ} {v1 : A}  → (tree tree₁ : bt A )
       → treeInvariant (node k v1 tree tree₁)
       →      treeInvariant tree₁
 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
-treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti
-treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
-treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
+treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x _ _ ti) = ti
+treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x _ _ ti) = t-leaf
+treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ _ _ _ _ ti ti₁) = ti₁
 
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack
@@ -228,9 +223,9 @@
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
-replaceTree1 k v1 value (t-right x t) = t-right x t
-replaceTree1 k v1 value (t-left x t) = t-left x t
-replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁
+replaceTree1 k v1 value (t-right x a b t) = t-right x ? ? t
+replaceTree1 k v1 value (t-left x a b t) = t-left x ? ? t
+replaceTree1 k v1 value (t-node x x₁ a b c d t t₁) = t-node x x₁ ? ? ? ? t t₁
 
 open import Relation.Binary.Definitions
 
@@ -501,47 +496,47 @@
      → replacedTree key value tree repl → treeInvariant repl
 RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value
 RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single key value
-RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
-RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
-RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁
+RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x ? ? ti
+RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x ? ? ti
+RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ ? ? ? ? ti ti₁
 -- r-right case
-RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x (t-single key value)
-RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ ti) (r-right x ri) = t-single key₁ value₁
-RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) =
-      t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri)
-RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ ti) (r-right x ())
-RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ ti) (r-right x r-leaf) =
-      t-node x₁ x ti (t-single key value)
-RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) =
-      t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ti (RTtoTI0 _ _ key value ti₁ ri)
+RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x ? ? (t-single key value)
+RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ a b ti) (r-right x ri) = t-single key₁ value₁
+RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
+      t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri)
+RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ a b ti) (r-right x ())
+RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ a b ti) (r-right x r-leaf) =
+      t-node x₁ x ? ? ? ? ti (t-single key value)
+RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) =
+      t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ? ? ? ?  ti (RTtoTI0 _ _ key value ti₁ ri)
 -- r-left case
-RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left x (t-single _ _ )
-RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ ti) (r-left x r-leaf) = t-node x x₁ (t-single key value) ti
-RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ ti) (r-left x ri) =
-      t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
-RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  (RTtoTI0 _ _ key value ti ri) ti₁
+RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left x ? ? (t-single _ _ )
+RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ a b ti) (r-left x r-leaf) = t-node x x₁ ? ? ? ? (t-single key value) ti
+RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
+      t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
+RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  ? ? ? ? (RTtoTI0 _ _ key value ti ri) ti₁
 
 RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
      → replacedTree key value tree repl → treeInvariant tree
 RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
 RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
-RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
-RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
-RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁
+RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x ? ? ti
+RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x ? ? ti
+RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ ? ? ? ? ti ti₁
 -- r-right case
-RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ ti) (r-right x r-leaf) = t-single key₁ value₁
-RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) =
-   t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁)  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
-RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x r-leaf) =
-    t-left x₁ ti
-RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
+RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁
+RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
+   t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ?  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
+RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) =
+    t-left x₁ ? ? ti
+RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) ? ? ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
 -- r-left case
-RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ ti) (r-left x ri) = t-single key₁ value₁
-RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ ti) (r-left x ri) =
-   t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
-RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x r-leaf) = t-right x₂ ti₁
-RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) =
-    t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
+RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁
+RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
+   t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
+RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ ? ? ti₁
+RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) =
+    t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? ? ? (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
 
 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t