Mercurial > hg > Gears > GearsAgda

changeset 572:eb75d9971451

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use lemma5 to follow stack
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 27 Apr 2018 19:53:44 +0900
parents 1eccf1f18a59
children 8777baeb90f8
files redBlackTreeTest.agda
diffstat 1 files changed, 9 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Fri Apr 27 19:19:40 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Apr 27 19:53:44 2018 +0900
@@ -160,32 +160,24 @@
    where
      tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
      tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
+     -- we should develop findNode/replaceNode/getRedBlackTree all at once
      lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
               (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
      lemma2 s with compTri k (key n1)
-     ... |  tri≈ le refl gt = lemma5 s
+     ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
         where 
            open stack.SingleLinkedStack
            open stack.Element
-           lemma6 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → (n2 : Element (Node ℕ ℕ) )
-              → ReplaceNode.replaceNode1 (tree0 s) s (record n1 { key = k ; value = x } ) (λ t →
-                 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))
-                        (record { top = Element.next n2 }) (Just (Element.datum n2))
-           lemma6 s n2 with (top s )
-           ...         | Just n3 with compTri (key (datum n2)) (key (datum n3))
-           ...            | tri< _ neq _ =  {!!} -- lemma6 ( record {top = next n3} ) {!!}
-           ...            | tri> _ neq _ =  {!!} -- lemma6 ( record {top = next n3} ) {!!}
-           ...            | tri≈  _ eq _  = {!!}
-           lemma6 s n2 | Nothing  = {!!}
-           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → popSingleLinkedStack ( record { top = Just (cons n1 (SingleLinkedStack.top s)) }  )
-               ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
-                   GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
-           lemma5 s with (top s)
+           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  )
+                 → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
+                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
+                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
+           lemma5 s t n with (top s)
            ...      | Just n2  with compTri k k
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
            ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri≈  _ refl _  = lemma6 s n2
-           lemma5 s | Nothing with compTri k k
+           ...            | tri≈  _ refl _  = lemma5 {!!} {!!} {!!}
+           lemma5 s t n | Nothing with compTri k k
            ...            | tri≈  _ refl _  = checkEQ x _ refl
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
            ...            | tri> _ neq _ =  ⊥-elim (neq refl)