Mercurial > hg > Gears > GearsAgda

changeset 863:5a34330bc850

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 Tue, 02 Apr 2024 12:29:30 +0900
parents 28e3ea66e4da
children d181dd606877
files hoareBinaryTree1.agda
diffstat 1 files changed, 12 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 02 10:23:48 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 02 12:29:30 2024 +0900
@@ -508,6 +508,13 @@
 ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr< _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫
 ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪  ri-tr< _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt)  ⟫ ⟫
 
+<-tr>  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr> key₁ tree → key₂ < key₁  → tr> key₂ tree
+<-tr> {n} {A} {leaf} {key₁} {key₂} tr lt = tt
+<-tr> {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans lt (proj1 tr) , ⟪ <-tr> (proj1 (proj2 tr)) lt , <-tr> (proj2 (proj2 tr)) lt ⟫ ⟫
+
+>-tr<  : {n : Level} {A : Set n}  → {tree : bt A} → {key₁ key₂ : ℕ} → tr< key₁ tree → key₁ < key₂  → tr< key₂ tree
+>-tr<  {n} {A} {leaf} {key₁} {key₂} tr lt = tt
+>-tr<  {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans (proj1 tr) lt , ⟪ >-tr< (proj1 (proj2 tr)) lt , >-tr< (proj2 (proj2 tr)) lt ⟫ ⟫
 
 RTtoTI0  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → replacedTree key value tree repl → treeInvariant repl
@@ -1116,14 +1123,16 @@
 RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-single .key₂ .(⟪ Red , c2 ⟫)) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? ? ?
 RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .leaf .(node key₅ _ _ _)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₅ _ _ _) (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-right .key₂ key₅ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? ? ?
 RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) .leaf) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .leaf (node key₃ _ _ _))) key value (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ (t-left key₅ .key₂ x₇ x₈ x₉ ti) ti₁) (rbr-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ? ? ? ?
-RB-repl→ti (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) (node key₆ value₆ t₆ t₇)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₃ _ _ _))) 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-rotate-ll x lt trb) = t-node _ _ _ ? x₁ ? ? ⟪ ? , ⟪ ? , ? ⟫ ⟫  ? rr02 rr03 where
+RB-repl→ti {_} {A} (node key₁ ⟪ Black , c1 ⟫ (node key₂ ⟪ Red , c2 ⟫ .(node key₅ _ _ _) (node key₆ value₆ t₆ t₇)) (node key₃ v3 t₂ t₃)) (node _ ⟪ Black , _ ⟫ (node key₄ value₁ t₄ t₅) (node _ ⟪ Red , _ ⟫ .(node key₆ _ _ _) (node key₃ _ _ _))) 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-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr00) x₁ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫  ⟪ <-trans x₁ x₂ , ⟪ rr05 , <-tr> x₆ x₁ ⟫ ⟫ rr02 rr03 where
         rr00 : (key₄ < key₂) ∧ tr< key₂ t₄ ∧ tr< key₂ t₅
         rr00 = RB-repl→ti< _ _ _ _ _ trb lt ⟪ x₇ , ⟪ x₉ , x₁₀ ⟫ ⟫
         rr02 : treeInvariant (node key₄ value₁ t₄ t₅)
         rr02 = RB-repl→ti _ _ _ _ ti trb
         rr03 : treeInvariant (node key₁ ⟪ Red , c1 ⟫ (node key₆ value₆ t₆ t₇) (node key₃ v3 t₂ t₃))
-        rr03 = RTtoTI0 _ _ _ _(t-node _ _ _ ? ? ? ? ? ? ti₂ ti₁) r-node
+        rr03 = RTtoTI0 _ _ _ _(t-node _ _ _ {_} {value₁} {_} {_} {_} {_} {_} (proj1 x₄) x₂ (proj1 (proj2 x₄)) (proj2 (proj2 x₄)) x₅ x₆ ti₂ ti₁) r-node
+        rr05 : tr> key₂ t₂
+        rr05 = <-tr> x₅ x₁
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x lt trb) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-lr t₂ t₃ kg kp kn trb) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-rl t₂ t₃ kg kp kn trb) = ?