Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 919:4d379ebc53c8

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, 04 Jun 2024 17:29:33 +0900
parents 1d34a752add0
children 368b9be0b312
comparison
equal deleted inserted replaced
918:1d34a752add0 919:4d379ebc53c8
1729 → treeInvariant tree0 1729 → treeInvariant tree0
1730 → (tree1 : bt (Color ∧ A)) 1730 → (tree1 : bt (Color ∧ A))
1731 → (stack : List (bt (Color ∧ A))) 1731 → (stack : List (bt (Color ∧ A)))
1732 → stackInvariant key tree1 tree0 stack 1732 → stackInvariant key tree1 tree0 stack
1733 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 1733 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )
1734 → (exit : (r : RBI key value tree0 stack ) → t ) → t 1734 → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t
1735 replaceRBTNode {n} {m} {A} {t} key value orig rbi ti leaf stack si (case1 refl) exit with stackToPG leaf orig stack si 1735 replaceRBTNode {n} {m} {A} {t} key value orig rbi ti leaf stack si (case1 refl) exit with stackToPG leaf orig stack si
1736 ... | case1 x = ? 1736 ... | case1 x = ?
1737 ... | case2 (case1 x) = ? 1737 ... | case2 (case1 x) = ?
1738 ... | case2 (case2 pg) = rp00 where 1738 ... | case2 (case2 pg) = rp00 where
1739 buildCase : t 1739 rb00 : stackInvariant key leaf orig (leaf ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
1740 buildCase = ? 1740 rb00 = subst (λ k → stackInvariant key leaf orig k) (PG.stack=gp pg) si
1741 rotateCase : t 1741 treerb : RBtreeInvariant (PG.parent pg)
1742 rotateCase = exit record { 1742 treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
1743 tree = ? 1743 pti : treeInvariant (PG.parent pg)
1744 ; repl = ? 1744 pti = siToTreeinvariant _ _ _ _ ti (popStackInvariant _ _ _ _ _ rb00)
1745 ; origti = ti
1746 ; origrb = rbi
1747 ; treerb = ?
1748 ; replrb = ?
1749 ; si = ?
1750 ; state = rotate ? ? ? ? }
1751 rp00 : t 1745 rp00 : t
1752 rp00 with PG.pg pg 1746 rp00 with PG.pg pg
1753 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? 1747 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with proj1 vp in pcolor
1754 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} 1748 ... | Red = rotateCase1 where
1755 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} 1749 rotateCase1 : t
1756 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} 1750 rotateCase1 = exit (PG.grand pg ∷ PG.rest pg) record {
1757 replaceRBTNode {n} {m} {A} key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record { 1751 tree = PG.grand pg
1752 ; repl = to-red ( node kg vg (to-black (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)) n2 )
1753 ; origti = ti
1754 ; origrb = rbi
1755 ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
1756 ; replrb = rb-red _ ? ? ? ? ? ?
1757 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
1758 ; state = rotate ? ? ? ? }
1759 ... | Black = buildCase1 where
1760 rb01 : bt (Color ∧ A)
1761 rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1
1762 rb03 : 1 ≡ black-depth n1
1763 rb03 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
1764 rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1)
1765 rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))
1766 rb04 : proj1 vp ≡ Black → ⟪ Black , proj2 vp ⟫ ≡ vp
1767 rb04 refl = refl
1768 rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
1769 rb05 = begin
1770 black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩
1771 black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl ⟩
1772 black-depth (node kp ⟪ Black , proj2 vp ⟫ leaf n1 ) ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩
1773 black-depth (node kp vp leaf n1) ≡⟨ cong black-depth (sym x) ⟩
1774 black-depth (PG.parent pg) ∎ where
1775 open ≡-Reasoning
1776 rb07 : key < kp
1777 rb07 = si-property-< ? (subst (λ k → treeInvariant k) x pti) (subst₂ (λ j k → stackInvariant key j orig k) refl (trans (PG.stack=gp pg) ? ) si)
1778 rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)
1779 rb06 = subst₂ (λ j k → replacedRBTree key value k (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor)
1780 (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
1781 buildCase1 : t
1782 buildCase1 = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
1783 tree = PG.parent pg
1784 ; repl = rb01
1785 ; origti = ti
1786 ; origrb = rbi
1787 ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
1788 ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k (node key ⟪ Red , value ⟫ leaf leaf) n1) (rb04 pcolor)) rb02
1789 ; si = popStackInvariant _ _ _ _ _ rb00
1790 ; state = rebuild (cong color x) rb05 rb06 }
1791 rp00 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
1792 rp00 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
1793 rp00 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
1794 replaceRBTNode {n} {m} {A} key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit ? record {
1758 tree = tree 1795 tree = tree
1759 ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right 1796 ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
1760 ; origti = ti 1797 ; origti = ti
1761 ; origrb = rbi 1798 ; origrb = rbi
1762 ; treerb = PGtoRBinvariant1 tree orig rbi stack si 1799 ; treerb = PGtoRBinvariant1 tree orig rbi stack si