Mercurial > hg > Gears > GearsAgda
changeset 849:71d06dae15a4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 28 Mar 2024 09:44:27 +0900 |
| parents | ad97032da3c8 |
| children | 8647f4c5797c |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 19 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Thu Mar 28 09:28:57 2024 +0900 +++ b/hoareBinaryTree1.agda Thu Mar 28 09:44:27 2024 +0900 @@ -799,19 +799,19 @@ -- case2 both parent and uncle are red (should we check uncle color?), flip color and up rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → replacedRBTree key value t₁ t₂ + → color t₂ ≡ Red → key < kp → replacedRBTree key value t₁ t₂ → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) rbr-flip-lr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → replacedRBTree key value t₁ t₂ + → color t₂ ≡ Red → key < kp → replacedRBTree key value t₁ t₂ → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) rbr-flip-rl : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → replacedRBTree key value t₁ t₂ + → color t₂ ≡ Red → kp < key → replacedRBTree key value t₁ t₂ → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → replacedRBTree key value t₁ t₂ + → color t₂ ≡ Red → kp < key → replacedRBTree key value t₁ t₂ → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) @@ -899,15 +899,15 @@ = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ -RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x rbt) lt tr +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ rbt) lt tr = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr)) , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr)))) , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫ , tr>-to-black (proj2 (proj2 tr)) ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value - (rbr-flip-lr x rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr>-to-black tr5 ⟫ ⟫ + (rbr-flip-lr x _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr>-to-black tr5 ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value - (rbr-flip-rl x rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ + (rbr-flip-rl x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value - (rbr-flip-rr x rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ + (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value (rbr-rotate-ll x rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr4 , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫ RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value @@ -937,15 +937,15 @@ = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ -RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x rbt) lt tr +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ rbt) lt tr = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr)) , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr)))) , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫ , tr<-to-black (proj2 (proj2 tr)) ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value - (rbr-flip-lr x rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr<-to-black tr5 ⟫ ⟫ + (rbr-flip-lr x _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr<-to-black tr5 ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value - (rbr-flip-rl x rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ + (rbr-flip-rl x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value - (rbr-flip-rr x rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ + (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value (rbr-rotate-ll x rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr4 , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫ RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value @@ -1040,15 +1040,15 @@ rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫ RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , value₂ ⟫ t t₁) .(to-black leaf)) key value - (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where + (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x lt trb) = t-left _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where rr00 : tr< key₂ t - rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂ + rr00 = RB-repl→ti< _ _ _ _ _ trb (<-trans lt x₁) x₂ rr02 : treeInvariant (node key₁ ⟪ Red , value₂ ⟫ t t₁) - rr02 = RB-repl→ti _ _ _ _ ti (rbr-left ? trb) -RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) (node key₃ _ _ _)) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black (node key₃ _ _ _))) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x trb) = ? -RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ? -RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x trb) = ? -RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rr x trb) = ? + rr02 = RB-repl→ti _ _ _ _ ti (rbr-left lt trb) +RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) (node key₃ _ _ _)) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black (node key₃ _ _ _))) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x lt trb) = ? +RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x lt trb) = ? +RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x lt trb) = ? +RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rr x lt trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key value ti (rbr-rotate-ll x trb) = ? RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x 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) = ?