Mercurial > hg > Gears > GearsAgda

changeset 792:5c6945d527a5

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 Sat, 21 Oct 2023 10:37:07 +0900
parents 846663e9858b
children 08e04ed15468
files hoareBinaryTree1.agda
diffstat 1 files changed, 24 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Oct 19 16:41:11 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Oct 21 10:37:07 2023 +0900
@@ -936,33 +936,43 @@
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 eq  = exit repl stack eq r
-    ... | case2 (case1 eq) = rb02 orig refl (RBI.si r)  where
+    ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r)  where
         rb01 : stackInvariant key (RBI.tree r) orig stack
         rb01 = RBI.si r
-        rb02 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
+        insertCase12 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
            → stackInvariant key (RBI.tree r) orig stack
            → t
-        rb02 leaf eq1 si = ? -- can't happen
-        rb02  (node key₁ value₁ left right) eq1 si with <-cmp key key₁
+        insertCase12 leaf eq1 si = ? -- can't happen
+        insertCase12  tr0@(node key₁ value₁ left right) eq1 si with <-cmp key key₁
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a b ¬c = ? -- can't happen
-        ... | tri> ¬a ¬b c = rb03 value₁ refl where
-           rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → right ≡ RBI.tree r
-           rb04 (s-right tree ty tree₁ x s-nil) refl = ?
-           rb04 (s-left tree₁ ty tree x si) refl = ?
-           rb03 : (v : Color ∧ A ) → v ≡ value₁ → t
-           rb03 ⟪ Black , value₄ ⟫ eq2 = exit (node key₁ value₁ left (RBI.tree r)) (orig ∷ [])  refl record {
+        ... | tri> ¬a ¬b c = insertCase13 value₁ refl where
+           rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
+           rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
+           rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
+           ... | refl = ⊥-elim ( nat-<> x c  )
+           insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
+           insertCase13 ⟪ Black , value₄ ⟫ eq2 = exit (node key₁ value₁ left (RBI.tree r)) (orig ∷ [])  refl record {
              tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
              ; treerb = RBI.origrb r
-             ; replrb = ?
+             ; replrb = rb05
              ; si = s-nil
              ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
-                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq))) eq1) (rtt-node rtt-unit (RBI.rotated r))
+                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq eq1))) eq1) (rtt-node rtt-unit (RBI.rotated r))
              ; ri = {!!} 
-             }
-           rb03 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
+             } where
+               rb05 : RBtreeInvariant (node key₁ value₁ left (RBI.tree r))
+               rb05 with RBI.origrb r
+               ... | rb-single key value = ?
+               ... | rb-right-red x x₁ t = ?
+               ... | rb-right-black x x₁ t = ?
+               ... | rb-left-red x x₁ t = ?
+               ... | rb-left-black x x₁ t = ?
+               ... | rb-node-red x x₁ x₂ t x₃ t₁ = ?
+               ... | rb-node-black x x₁ x₂ t x₃ t₁ = ?
+           insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit ? ? ? ? 
            ... | Red = exit ? ? ? ?
            --       r = orig                            RBI.tree b