Mercurial > hg > Gears > GearsAgda

changeset 937:a452a969c910

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... flip almost done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Jun 2024 18:01:03 +0900
parents e055f9354ea4
children cf9de6f45d50
files hoareBinaryTree1.agda
diffstat 1 files changed, 30 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Jun 13 19:10:35 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jun 14 18:01:03 2024 +0900
@@ -1305,20 +1305,43 @@
        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
+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 _ _ _ x₁ x₂ x₃ rr00 x₅ x₆ (t-node _ _ _ x₇ (proj1 rr01) x₉ x₁₀ (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) 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₄
+        rr01 : (key₂ < key₅) ∧ tr> key₂ t₄ ∧ tr> key₂ t₆
+        rr01 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫
 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
-      (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x y lt lt2 trb) = ? where
-        rr00 : tr> key₁ t₄
+RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ t₂ leaf)) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node key₃ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) .leaf)) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rl x y lt lt2 trb) 
+   = t-node _ _ _ x₁ x₂ x₃ x₄ rr00 tt (replaceTree1 _ _ _ ti) (t-left _ _ (proj1 rr01) (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) (RB-repl→ti _ _ _ _ (treeLeftDown _ _ ti₁) trb)) where
+        rr00 : (key₁ < key₄) ∧ tr> key₁ t₄ ∧ tr> key₁ t₅
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₅
+        rr01 : (key₄ < key₃) ∧ tr< key₃ t₄ ∧ tr< key₃ t₅
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 (proj1 (ti-property1 ti₁))
+RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ .leaf (node key₅ value₂ t₃ t₆))) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node key₃ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) .(node key₅ value₂ t₃ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-right .key₃ .key₅ x₇ x₈ x₉ ti₁)) (rbr-flip-rl x y lt lt2 trb) = t-node _ _ _ x₁ x₂ x₃ x₄ rr00 rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ (proj1 rr01) x₇ (proj1 (proj2 rr01)) (proj2 (proj2 rr01)) x₈ x₉ (RB-repl→ti _ _ _ _ t-leaf trb) ti₁) where
+        rr00 : (key₁ < key₄) ∧ tr> key₁ t₄ ∧ tr> key₁ t₅
         rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₅
-        rr02 : treeInvariant (node key₃ ⟪ Red , v3 ⟫ t₄ t₃)
-        rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-left ? lt2 trb)
+        rr01 : (key₄ < key₃) ∧ tr< key₃ t₄ ∧ tr< key₃ t₅
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 tt
+        rr02 : (key₁ < key₅) ∧ tr> key₁ t₃ ∧ tr> key₁ t₆
+        rr02 = ⟪ <-trans x₂ x₇ , ⟪ <-tr> x₈ x₂  , <-tr> x₉ x₂ ⟫ ⟫
+RB-repl→ti (node _ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node _ ⟪ Red , v3 ⟫ .(node key₆ _ _ _) (node key₅ value₂ t₃ t₆))) (node key₁ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node key₃ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) .(node key₅ value₂ t₃ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node key₆ .key₃ .key₅ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-flip-rl x y lt lt2 trb) 
+   = t-node _ _ _ x₁ x₂ x₃ x₄ rr00 rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ (proj1 rr01) x₈ (proj1 (proj2 rr01))  (proj2 (proj2 rr01))  x₁₁ x₁₂ (RB-repl→ti _ _ _ _ ti₁ trb) ti₂) where
+        rr00 : (key₁ < key₄) ∧ tr> key₁ t₄ ∧ tr> key₁ t₅
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt x₅
+        rr01 : (key₄ < key₃ ) ∧ tr< key₃  t₄ ∧ tr< key₃ t₅
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫
+        rr02 : (key₁ < key₅) ∧ tr> key₁ t₃ ∧ tr> key₁ t₆
+        rr02 = ⟪ proj1 x₆ , ⟪  <-tr> x₁₁ x₂ , <-tr> x₁₂ x₂  ⟫ ⟫
 RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ t t₁)) (node _ ⟪ Red , _ ⟫ .(to-black leaf) (node _ ⟪ Black , v2 ⟫ t t₂)) key value
     (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rr x () lt trb) 
-RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ leaf t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .leaf t₄)) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) = ?
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ leaf t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .leaf (node key₄ value₁ t₄ t₅))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) 
+     = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr01 (replaceTree1 _ _ _ ti) (t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ (treeRightDown _ _ ti₁) trb)) where
+        rr00 : (key₃ < key₄) ∧ tr> key₃ t₄ ∧ tr> key₃ t₅
+        rr00 = ?
+        rr01 : (key₁ < key₄) ∧ tr> key₁ t₄ ∧ tr> key₁ t₅ 
+        rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆
 RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ (node key₄ value₁ t₂ t₅) .leaf)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .(node key₄ value₁ t₂ t₅) (node key₅ value₂ t₄ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left .key₄ .key₃ x₇ x₈ x₉ ti₁)) (rbr-flip-rr x y lt trb) = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ x₇ (proj1 rr00) x₈ x₉ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti₁ (RB-repl→ti _ _ _ _ t-leaf trb)) where
         rr00 : (key₃ < key₅) ∧ tr> key₃ t₄ ∧ tr> key₃ t₆
         rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt