Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 747:70ed4cbeaafb

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 09:05:03 +0900
parents 4edec19e8356
children 1d7803a2c4c0
comparison
equal deleted inserted replaced
746:4edec19e8356 747:70ed4cbeaafb
572 572
573 -- This one can be very difficult 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 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) 575 -- rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf)
576 576
577 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where 577 color : {n : Level} (A : Set n) → (rb : bt (Color ∧ A)) → Color
578 rb-leaf : (key : ℕ) → RBTree A key Black 0 578 color {n} A rb = ?
579 rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1 579
580 t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d 580 RB→bt : {n : Level} (A : Set n) → (rb : bt (Color ∧ A)) → bt A
581 t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d
582 → RBTree A key Black (suc d)
583 t-left-red : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d
584 → RBTree A key₁ Red d
585 t-left-black : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ} → RBTree A key c d
586 → RBTree A key₁ Black (suc d)
587 t-node-red : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {d : ℕ}
588 → RBTree A key Black d
589 → RBTree A key₂ Black d
590 → RBTree A key₁ Red d
591 t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ}
592 → RBTree A key c d
593 → RBTree A key₂ c1 d
594 → RBTree A key₁ Black (suc d)
595
596 color : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → Color
597 color {n} A {k} {d} {c} rb = ?
598
599 RB→bt : {n : Level} (A : Set n) → (rb : bt (A ∧ Color)) → bt A
600 RB→bt {n} A leaf = leaf 581 RB→bt {n} A leaf = leaf
601 RB→bt {n} A (node key ⟪ c , value ⟫ x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 582 RB→bt {n} A (node key ⟪ c , value ⟫ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁)
602 583
603 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where 584 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
604 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 585 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
605 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent grand 586 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent grand
606 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 587 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
617 -- b c d a 598 -- b c d a
618 -- d e e c 599 -- d e e c
619 rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A} 600 rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
620 → ka < kb 601 → ka < kb
621 → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁ 602 → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
622 → rotatedTree (node ka va (node kb vb d e) tc) (node kb vb d₁ (node ka va e₁ c₁) ) 603 → rotatedTree (node ka va (node kb vb d e) c) (node kb vb d₁ (node ka va e₁ c₁) )
623 -- b a 604 -- b a
624 -- d a b c 605 -- d a b c
625 -- e c d e 606 -- e c d e
626 rr-left : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A} 607 rr-left : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
627 → ka < kb 608 → ka < kb
669 650
670 rbsi-len : {n : Level} {A : Set n} {orig parent grand : bt A} 651 rbsi-len : {n : Level} {A : Set n} {orig parent grand : bt A}
671 → ParentGrand orig parent grand → ℕ 652 → ParentGrand orig parent grand → ℕ
672 rbsi-len {n} {A} {s} {p} {g} st = ? 653 rbsi-len {n} {A} {s} {p} {g} st = ?
673 654
674 findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (orig : RBTree A key1 c1 d1 ) 655 -- findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (orig : RBTree A key1 c1 d1 )
675 → (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack 656 -- → (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack
676 → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack → rbt-depth A tree1 < rbt-depth A tree → t ) 657 -- → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack → rbt-depth A tree1 < rbt-depth A tree → t )
677 → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack 658 -- → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack
678 → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key ) → t ) → t 659 -- → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key ) → t ) → t
679 findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ? 660 --findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ?
680 661
681 rotateRight : ? 662 rotateRight : ?
682 rotateRight = ? 663 rotateRight = ?
683 664
684 rotateLeft : ? 665 rotateLeft : ?
685 rotateLeft = ? 666 rotateLeft = ?
686 667
687 insertCase5 : {n m : Level} {A : Set n} {t : Set m} 668 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
688 → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} 669 → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}
689 → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 ) 670 → (orig tree repl : bt (Color ∧ A) )
690 → (si : ParentGrand ? ? ?) 671 → (si : ParentGrand ? ? ?)
691 → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl)) 672 → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
692 → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 673 → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 repl1 : bt (Color ∧ A))
693 → (si1 : ParentGrand ? ? ?) 674 → (si1 : ParentGrand ? ? ?)
694 → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1)) 675 → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
695 → rbsi-len si1 < rbsi-len si → t ) 676 → rbsi-len si1 < rbsi-len si → t )
696 → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 677 → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 repl1 : bt (Color ∧ A))
697 → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1)) 678 → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
698 → t ) → t 679 → t ) → t
699 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where 680 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
700 insertCase51 : (key1 : ℕ) (si : ParentGrand ? ? ? ) → t 681 insertCase51 : (key1 : ℕ) (si : ParentGrand ? ? ? ) → t
701 insertCase51 = ? 682 insertCase51 = ?
702 683
703 replaceRBP : {n m : Level} {A : Set n} {t : Set m} 684 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
704 → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color} 685 → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color}
705 → (orig : RBTree A key0 c0 d0 ) → (tree : RBTree A key1 c1 d1 ) 686 → (orig tree : bt (Color ∧ A))
706 → (stack : List (bt A)) → (si : stackInvariant key (RB→bt A tree) (RB→bt A orig) stack ) 687 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
707 → (next : {key2 d2 : ℕ} {c2 : Color} → (tree2 : RBTree A key2 c2 d2 ) 688 → (next : {key2 d2 : ℕ} {c2 : Color}
708 → {tr to : bt A} → RB→bt A tree2 ≡ tr → RB→bt A orig ≡ to 689 → (to tr : bt (Color ∧ A))
709 → (stack1 : List (bt A)) → stackInvariant key tr to stack1 690 → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1
710 → length stack1 < length stack → t ) 691 → length stack1 < length stack → t )
711 → (exit : {k1 d1 : ℕ} {c1 : Color} → (repl1 : RBTree A k1 c1 d1 ) → (rot : bt A ) 692 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
712 → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1) → t ) → t 693 → (ri : rotatedTree (RB→bt A orig) (RB→bt A rot) ) → replacedTree key value (RB→bt A rot) (RB→bt A repl) → t ) → t
713 replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where 694 replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = ? where
714 insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) 695 insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree parent grand : bt (Color ∧ A))
715 → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) 696 → (stack : List (bt (Color ∧ A))) → (tr to : bt (Color ∧ A)) → (si : stackInvariant key tr to stack )
716 → (stack : List (bt A)) → (tr to pt gt : bt A) → RB→bt A tree ≡ tr → RB→bt A parent ≡ pt → RB→bt A grand ≡ gt → RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 697 → (pg : ParentGrand tree parent grand ) → t
717 → (pg : ParentGrand tr pt gt ) → t 698 insertCase2 tree parent grand stack tr to = ?
718 insertCase2 tree parent grand stack tr to treq toeq si pg = ? 699 insertCase1 : (stack : List (bt (Color ∧ A))) → (to tr : bt (Color ∧ A)) → (si : stackInvariant key tr to stack ) → t
719 insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr → RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t 700 insertCase1 stack to tr si with stackToPG tr to stack si
720 insertCase1 stack tr to eqt eqo si with stackToPG tr to stack si
721 ... | case1 eq = ? 701 ... | case1 eq = ?
722 ... | case2 (case1 eq ) = ? 702 ... | case2 (case1 eq ) = ?
723 ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? ? ? ? ? ? ? (PG.pg pg) where 703 ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? (PG.pg pg) where
724 si00 : stackInvariant key ? ? ? 704 si00 : stackInvariant key ? ? ?
725 si00 = ? 705 si00 = ?
726 706
727 707