Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 796:e1737f00a7aa

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, 26 Oct 2023 18:11:17 +0900
parents e9ba6a5bc64b
children 03831d974342
comparison
equal deleted inserted replaced
795:e9ba6a5bc64b 796:e1737f00a7aa
698 rotated : rotatedTree tree rot 698 rotated : rotatedTree tree rot
699 ri : replacedRBTree key value (child-replaced key rot ) repl 699 ri : replacedRBTree key value (child-replaced key rot ) repl
700 repl-red : color repl ≡ Red 700 repl-red : color repl ≡ Red
701 repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl 701 repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
702 702
703 -- r (b , b) inserting a node into black node does not change the black depth, but color may change
704 -- → b (b , r ) ∨ b (r , b)
705 -- b (b , b)
706 -- → b (b , r ) ∨ b (r , b)
707 -- b (r , b) inserting to right → b (r , r )
708 -- b (r , b) inserting to left may increse black depth, need rotation
709 -- find b in left and move the b to the right (one down or two down)
710 --
711 rbi-case1 : {n : Level} {A : Set n} → {key d : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
712 → RBtreeInvariant parent
713 → RBtreeInvariant repl
714 → {left right : bt (Color ∧ A) } → parent ≡ node key ⟪ Black , value ⟫ left right
715 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) )
716 ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
717 rbi-case1 {n} {A} {key} = {!!}
718
719 rbi-case31 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
720 → RBtreeInvariant grand
721 → RBtreeInvariant repl
722 → {uncle left right : bt (Color ∧ A) }
723 → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent
724 → parent ≡ node kp ⟪ Red , vp ⟫ left right
725 → color uncle ≡ Red
726 → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) )
727 ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) )
728 rbi-case31 {n} {A} {key} = {!!}
729
730 --
731 -- case4 increase the black depth
732 --
733 rbi-case41 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
734 → RBtreeInvariant grand
735 → RBtreeInvariant repl
736 → {uncle left right : bt (Color ∧ A) }
737 → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent
738 → parent ≡ node kp ⟪ Red , vp ⟫ left right
739 → color uncle ≡ Black
740 → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) )
741 ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) )
742 rbi-case41 {n} {A} {key} = {!!}
743
744 rbi-case51 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) )
745 → RBtreeInvariant grand
746 → RBtreeInvariant repl
747 → {uncle left right : bt (Color ∧ A) }
748 → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent
749 → parent ≡ node kp ⟪ Red , vp ⟫ left right
750 → color uncle ≡ Black
751 → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) )
752 ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) )
753 rbi-case51 {n} {A} {key} = {!!}
754
755 --... | Black = record {
756 -- d = ? ; od = RBI.od rbi ; rd = ?
757 -- ; tree = ? ; rot = ? ; repl = ?
758 -- ; treerb = ? ; replrb = ?
759 -- ; d=rd = ? ; si = ? ; rotated = ? ; ri = ?
760 -- ; origti = RBI.origti rbi ; origrb = RBI.origrb rbi
761 -- }
762 --... | Red = ?
763
764 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) 703 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
765 → (stack : List (bt A)) → stackInvariant key tree orig stack 704 → (stack : List (bt A)) → stackInvariant key tree orig stack
766 → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack 705 → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
767 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl 706 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
768 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl) 707 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl)
957 -- 896 --
958 -- B => B B => B 897 -- B => B B => B
959 -- / \ / \ / \ rotate L / \ 898 -- / \ / \ / \ rotate L / \
960 -- L L1 L R3 L R -- bad B B 899 -- L L1 L R3 L R -- bad B B
961 -- / \ / \ / \ 1 : child-replace 900 -- / \ / \ / \ 1 : child-replace
962 --- L L2 L B L L 2: child-replace ( unbrance ) 901 --- L L2 L B L L 2: child-replace ( unbalanced )
963 -- / \ 3: child-replace ( rotated / balanced ) 902 -- / \ 3: child-replace ( rotated / balanced )
964 -- L L 903 -- L L
965 -- 904 --
966 rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r 905 rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
967 rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl 906 rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl