Mercurial > hg > Gears > GearsAgda

changeset 832:01658441313e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RTtoTI0 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 Mar 2024 18:14:41 +0900
parents 0b0a54d7d683
children 9ec2b7f8e5a7
files hoareBinaryTree1.agda
diffstat 1 files changed, 32 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Mar 14 17:12:11 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Mar 14 18:14:41 2024 +0900
@@ -67,8 +67,8 @@
     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₄
+       → 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₄))
@@ -532,17 +532,39 @@
 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 a b tt tt ti (t-single key value)
 RTtoTI0 (node key₁ _ (node _ _ left₀ right₀) (node key₂ _ left₁ right₁)) (node key₁ _ (node _ _ left₂ right₂) (node key₃ _ left₃ right₃)) 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₂) a b (rr00 ri c) ?  ti (RTtoTI0 _ _ key value ti₁ ri) where
-         rr00 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₂ left₁ → tr> key₃ left₃
+      t-node _ _ _ x₁ (subst (λ k → key₁ < k ) (rt-property-key ri) x₂) a b (rr00 ri c) (rr02 ri d) ti (RTtoTI0 _ _ key value ti₁ ri) where
+         rr00 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ left₁ → tr> key₁ left₃
          rr00 r-node tb = tb
          rr00 (r-right x₃ ri) tb = tb
-         rr00 (r-left x₃ ri) tb = ri-tr> _ _ _ _ _ ri ? tb
+         rr00 (r-left x₃ ri) tb = ri-tr> _ _ _ _ _ ri x tb
+         rr02 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ right₁ → tr> key₁ right₃
+         rr02 r-node tb = tb
+         rr02 (r-right x₃ ri) tb = ri-tr> _ _ _ _ _ ri x tb
+         rr02 (r-left x₃ ri) tb = tb
 -- 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₁ 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₂  ? ? c d (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 tt tt (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₁ tt tt a b (t-single key value) ti 
+RTtoTI0 (node key₃ _ (node key₂ _ left₁ right₁) leaf) (node key₃ _ (node key₁ value₁ left₂ right₂) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) =
+      t-left _ _ (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (rr00 ri a) (rr02 ri b) (RTtoTI0 _ _ key value ti ri) where -- key₁ < key₃ 
+         rr00 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ left₁ → tr< key₃ left₂
+         rr00 r-node tb = tb
+         rr00 (r-right x₂ ri) tb = tb
+         rr00 (r-left x₂ ri) tb = ri-tr< _ _ _ _ _ ri x tb
+         rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ right₁ → tr< key₃ right₂
+         rr02 r-node tb = tb
+         rr02 (r-right x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb
+         rr02 (r-left x₃ ri) tb = tb 
+RTtoTI0 (node key₁ _ (node key₂ _ left₂ right₂) (node key₃ _ left₃ right₃)) (node key₁ _ (node key₄ _ left₄ right₄) (node key₅ _ left₅ right₅)) 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₂  (rr00 ri a) (rr02 ri b) c d (RTtoTI0 _ _ key value ti ri) ti₁ where
+         rr00 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ left₂ → tr< key₁ left₄
+         rr00 r-node tb = tb
+         rr00 (r-right x₃ ri) tb = tb
+         rr00 (r-left x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb
+         rr02 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ right₂ → tr< key₁ right₄
+         rr02 r-node tb = tb
+         rr02 (r-right x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb 
+         rr02 (r-left x₃ ri) tb = tb 
 
 -- RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
 --      → replacedTree key value tree repl → treeInvariant tree