Mercurial > hg > Gears > GearsAgda

changeset 936:e055f9354ea4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Jun 2024 19:10:35 +0900
parents 59aac5d681c3
children a452a969c910
files hoareBinaryTree1.agda
diffstat 1 files changed, 29 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Jun 13 10:54:31 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Jun 13 19:10:35 2024 +0900
@@ -254,6 +254,14 @@
 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₁
 
+ti-property1 :  {n : Level} {A : Set n} {key₁ : ℕ} {value₂ : A} {left right : bt A} → treeInvariant (node key₁ value₂  left right ) →   tr< key₁ left ∧  tr> key₁ right
+ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.leaf} (t-single .key₁ .value₂) = ⟪ tt , tt ⟫
+ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.(node key₂ _ _ _)} (t-right .key₁ key₂ x x₁ x₂ t) = ⟪ tt , ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ ⟫
+ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.leaf} (t-left key .key₁ x x₁ x₂ t) = ⟪ ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ , tt ⟫
+ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.(node key₂ _ _ _)} (t-node key .key₁ key₂ x x₁ x₂ x₃ x₄ x₅ t t₁) 
+     = ⟪ ⟪ x , ⟪ x₂ , x₃ ⟫ ⟫ , ⟪ x₁ , ⟪ x₄ , x₅ ⟫ ⟫ ⟫
+
+
 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
            → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
@@ -1266,10 +1274,9 @@
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
 RB-repl→ti .(node key₂ ⟪ Black , value₁ ⟫ (node key₁ ⟪ Red , value₂ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , value₂ ⟫ t t₁) .(to-black leaf)) key value (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x () lt trb)
-RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ leaf) (node key₃ ⟪ c1 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₄ value₃ t t₁) .leaf) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x y lt trb) 
-    = t-node _ _ _ ? ? ? ? ? ? (t-left _ _ ? ? ? (RB-repl→ti _ _ _ _ ? trb)) (replaceTree1 _ _ _ ti₁) where
+RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ leaf) (node key₃ ⟪ c1 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₄ value₃ t t₁) .leaf) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x y lt trb) = t-node _ _ _ x₁ x₂ ⟪ <-trans (proj1 rr00) x₁  , ⟪ >-tr< (proj1 (proj2 rr00)) x₁ , >-tr< (proj2 (proj2 rr00)) x₁ ⟫ ⟫ tt x₅ x₆ (t-left _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ (treeLeftDown _ _ ti) trb)) (replaceTree1 _ _ _ ti₁) where
         rr00 : (key₄ < key₁) ∧ tr< key₁ t ∧ tr< key₁ t₁
-        rr00 = RB-repl→ti< _ _ _ _ _ trb lt ?
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt (proj1 (ti-property1 ti))
 RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ .leaf (node key₄ value₃ t₁ t₂)) (node key₃ ⟪ c0 , v1 ⟫ left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ (node key₅ value₄ t t₃) .(node key₄ value₃ t₁ t₂)) (node key₃ ⟪ Black , v1 ⟫ left right)) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₁ .key₄ x₇ x₈ x₉ ti) ti₁) (rbr-flip-ll x y lt trb) 
     = t-node _ _ _ x₁ x₂ ⟪ <-trans (proj1 rr00) x₁ , ⟪ >-tr< (proj1 (proj2 rr00)) x₁  , >-tr< (proj2 (proj2 rr00)) x₁  ⟫ ⟫  x₄ x₅ x₆ (t-node _ _ _ (proj1 rr00) x₇ (proj1 (proj2 rr00)) (proj2 (proj2 (rr00))) x₈ x₉ (RB-repl→ti _ _ _ _ t-leaf trb) ti) (replaceTree1 _ _ _ ti₁) where
         rr00 : (key₅ < key₁) ∧ tr< key₁ t ∧ tr< key₁ t₃
@@ -1281,12 +1288,26 @@
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫
 RB-repl→ti (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ left right) leaf) (node key₂ ⟪ Red , v1 ⟫ (node key₃ ⟪ Black , v2 ⟫ left right₁) leaf) key value
       (t-left _ _ x₁ x₂ x₃ ti) (rbr-flip-lr x () lt lt2 trb) 
-RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ t t₁) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₄) .(to-black (node key₃ ⟪ c3 , _ ⟫ _ _))) key value
-      (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x y lt lt2 trb) = ? where
-        rr00 : tr< key₁ t₄
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ leaf leaf) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ .leaf (node key₄ value₁ t₄ t₅)) .(to-black (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x y lt lt2 trb) 
+  = t-node _ _ _ x₁ x₂ tt rr00 x₅ x₆ (t-right _ _ (proj1 rr01) (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) (RB-repl→ti _ _ _ _ t-leaf trb)) (replaceTree1 _ _ _ ti₁) where
+       rr00 : (key₄ < key₁) ∧ tr< key₁ t₄ ∧ tr< key₁ t₅
+       rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 tt 
+       rr01 : (key₂ < key₄) ∧ tr> key₂ t₄ ∧ tr> key₂ t₅
+       rr01 = RB-repl→ti> _ _ _ _ _ trb lt tt 
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ leaf (node key₅ value₂ t₁ t₆)) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ .leaf (node key₄ value₁ t₄ t₅)) .(to-black (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₂ .key₅ x₇ x₈ x₉ ti) ti₁) (rbr-flip-lr x y lt lt2 trb) = t-node _ _ _ x₁ x₂ tt rr00 x₅ x₆ (t-right _ _ (proj1 rr01) (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) (RB-repl→ti _ _ _ _ ti trb)) (replaceTree1 _ _ _ ti₁) where
+       rr00 : (key₄ < key₁) ∧ tr< key₁ t₄ ∧ tr< key₁ t₅
+       rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₄
+       rr01 : (key₂ < key₄) ∧ tr> key₂ t₄ ∧ tr> key₂ t₅
+       rr01 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₈ , x₉ ⟫ ⟫
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ (node key₄ value₁ t t₅) .leaf) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ .(node key₄ value₁ t t₅) (node key₅ value₂ t₄ t₆)) .(to-black (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-left .key₄ .key₂ x₇ x₈ x₉ ti) ti₁) (rbr-flip-lr x y lt lt2 trb) 
+    = t-node _ _ _ x₁ x₂ x₃ rr00 x₅ x₆ (t-node _ _ _ x₇ (proj1 rr01) x₈ x₉ (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) ti (RB-repl→ti _ _ _ _ t-leaf trb)) (replaceTree1 _ _ _ ti₁) where
+       rr00 : (key₅ < key₁) ∧ tr< key₁ t₄ ∧ tr< key₁ t₆
+       rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 tt
+       rr01 : (key₂ < key₅) ∧ tr> key₂ t₄ ∧ tr> key₂ t₆
+       rr01 = RB-repl→ti> _ _ _ _ _ trb lt tt
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ (node key₄ value₁ t t₅) .(node key₆ _ _ _)) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ .(node key₄ value₁ t t₅) (node key₅ value₂ t₄ t₆)) .(to-black (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-node .key₄ .key₂ key₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti ti₂) ti₁) (rbr-flip-lr x y lt lt2 trb) = t-node _ _ _ ? ? ? ? ? ? (t-node _ _ _ ? ? ? ? ? ? ti (RB-repl→ti _ _ _ _ ti₂ trb)) (replaceTree1 _ _ _ ti₁) where
+        rr00 : (key₅ < key₁) ∧ tr< key₁ t₄ ∧ tr< key₁ t₆
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₄
-        rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₄)
-        rr02 = RB-repl→ti _ _ _ _ ti (rbr-right ? lt trb)
 RB-repl→ti (node _ ⟪ Black , _ ⟫ leaf (node _ ⟪ Red , _ ⟫ t t₁)) (node key₁ ⟪ Red , v1 ⟫ .(to-black leaf) (node key₂ ⟪ Black , v2 ⟫ t₂ t₁)) key value
       (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rl x () lt lt2 trb) 
 RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , _ ⟫  _ _)) (node key₃ ⟪ Black , _ ⟫ t₄ t₃)) key value