Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 746:4edec19e8356

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, 25 Apr 2023 08:16:02 +0900
parents 9b7d706e7d0f
children 70ed4cbeaafb
comparison
equal deleted inserted replaced
745:9b7d706e7d0f 746:4edec19e8356
542 542
543 data Color : Set where 543 data Color : Set where
544 Red : Color 544 Red : Color
545 Black : Color 545 Black : Color
546 546
547 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where 547 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
548 rb-leaf : RBtreeInvariant leaf 548 rb-leaf : RBtreeInvariant leaf 0
549 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 549 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 1
550 550 rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
551 data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where 551 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
552 r-leaf : replacedRBTree key ⟪ ? , value ⟫ leaf (node key ⟪ ? , value ⟫ leaf leaf) 552 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) d
553 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 553 rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
554 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 554 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) d
555 → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 555 → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) (suc d)
556 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 556 rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
557 → key < k → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 557 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
558 → RBtreeInvariant (node key₁ ⟪ Red , value ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) d
559 rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
560 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) d
561 → RBtreeInvariant (node key₁ ⟪ Black , value ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) (suc d)
562 rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
563 → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
564 → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
565 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
566 rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
567 → {c c₁ : Color}
568 → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) d
569 → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
570 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
571
572
573 -- This one can be very difficult
574 -- data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where
575 -- rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf)
558 576
559 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where 577 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
560 rb-leaf : (key : ℕ) → RBTree A key Black 0 578 rb-leaf : (key : ℕ) → RBTree A key Black 0
561 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1 579 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1
562 t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d 580 t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
573 t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ} 591 t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ}
574 → RBTree A key c d 592 → RBTree A key c d
575 → RBTree A key₂ c1 d 593 → RBTree A key₂ c1 d
576 → RBTree A key₁ Black (suc d) 594 → RBTree A key₁ Black (suc d)
577 595
578 color : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → Color 596 color : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → Color
579 color {n} A {k} {d} {c} rb = c 597 color {n} A {k} {d} {c} rb = ?
580 598
581 rb-key : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → ℕ 599 RB→bt : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → bt A
582 rb-key {n} A {k} {d} {c} rb = k 600 RB→bt {n} A leaf = leaf
583 601 RB→bt {n} A (node key ⟪ c , value ⟫ x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
584 RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
585 RB→bt {n} A (rb-leaf _) = leaf
586 RB→bt {n} A (rb-single key value _) = node key value leaf leaf
587 RB→bt {n} A (t-right-red key value x rb) = node key value leaf (RB→bt A rb)
588 RB→bt {n} A (t-right-black key value x rb) = node key value leaf (RB→bt A rb)
589 RB→bt {n} A (t-left-red key value x rb) = node key value (RB→bt A rb) leaf
590 RB→bt {n} A (t-left-black key value x rb) = node key value (RB→bt A rb) leaf
591 RB→bt {n} A (t-node-red key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
592 RB→bt {n} A (t-node-black key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
593
594 rbt-depth : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → ℕ
595 rbt-depth A (rb-leaf _) = zero
596 rbt-depth A (rb-single _ value _) = 1
597 rbt-depth A (t-right-red _ value x ab) = suc ( rbt-depth A ab)
598 rbt-depth A (t-right-black _ value x ab) = suc ( rbt-depth A ab)
599 rbt-depth A (t-left-red _ value x ab) = suc ( rbt-depth A ab)
600 rbt-depth A (t-left-black _ value x ab) = suc ( rbt-depth A ab)
601 rbt-depth A (t-node-red _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ ))
602 rbt-depth A (t-node-black _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ ))
603
604 rbt-key : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → Maybe ℕ
605 rbt-key {n} A (rb-leaf _) = nothing
606 rbt-key {n} A (rb-single key value _) = just key
607 rbt-key {n} A (t-right-red key value x rb) = just key
608 rbt-key {n} A (t-right-black key value x rb) = just key
609 rbt-key {n} A (t-left-red key value x rb) = just key
610 rbt-key {n} A (t-left-black key value x rb) = just key
611 rbt-key {n} A (t-node-red key value x x₁ rb rb₁) = just key
612 rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
613 602
614 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where 603 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
615 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 604 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
616 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent grand 605 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent grand
617 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 606 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
619 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 608 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
620 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 609 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent grand
621 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 610 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
622 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 611 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent grand
623 612
613 -- with color
624 data rotatedTree {n : Level} {A : Set n} : (before after : bt A ) → Set n where 614 data rotatedTree {n : Level} {A : Set n} : (before after : bt A ) → Set n where
625 rr-node : {t : bt A} → rotatedTree t t 615 rr-node : {t : bt A} → rotatedTree t t
626 -- a b 616 -- a b
627 -- b c d a 617 -- b c d a
628 -- d c 618 -- d e e c
629 rr-right : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A} 619 rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
630 → ka < kb 620 → ka < kb
631 → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1 621 → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
632 → rotatedTree (node ka va (node kb vb ta tb) tc) (node kb vb ta1 (node ka va tb1 tc1) ) 622 → rotatedTree (node ka va (node kb vb d e) tc) (node kb vb d₁ (node ka va e₁ c₁) )
633 -- b a 623 -- b a
634 -- d a b c 624 -- d a b c
635 -- c d 625 -- e c d e
636 rr-left : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A} 626 rr-left : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
637 → ka < kb 627 → ka < kb
638 → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1 628 → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
639 → rotatedTree (node kb vb ta (node ka va tb tc) ) (node ka va (node kb vb ta1 tb1) tc1) 629 → rotatedTree (node kb vb d (node ka va e c) ) (node ka va (node kb vb d₁ e₁) c₁)
640 630
641 record PG {n : Level } (A : Set n) (stack : List (bt A)) : Set n where 631 record PG {n : Level } (A : Set n) (stack : List (bt A)) : Set n where
642 field 632 field
643 self parent grand : bt A 633 self parent grand : bt A
644 pg : ParentGrand self parent grand 634 pg : ParentGrand self parent grand