# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1525602938 -32400
# Node ID 8777baeb90f86d80c11ae3d13befe8cfe07ea65a
# Parent  eb75d99714512045d14fced90ade747892671ecf
...

diff -r eb75d9971451 -r 8777baeb90f8 Todo.txt
--- a/Todo.txt	Fri Apr 27 19:53:44 2018 +0900
+++ b/Todo.txt	Sun May 06 19:35:38 2018 +0900
@@ -1,9 +1,19 @@
+Sun May  6 17:54:50 JST 2018
+
+    do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?
+
+
+Mon Apr 30 17:15:16 JST 2018
+
+    Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
+    やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい
+
 Mon Mar 26 17:43:06 JST 2018
 
-    Decidable を使って Compare の場合分けを行う
+    Decidable を使って Compare の場合分けを行う    
     Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
     場合分けには Trichotomous を使う
-    compareTri を完成させる               
+    compareTri を完成させる    Done
 
 Fri Jan  5 16:43:26 JST 2018
 
diff -r eb75d9971451 -r 8777baeb90f8 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Fri Apr 27 19:53:44 2018 +0900
+++ b/redBlackTreeTest.agda	Sun May 06 19:35:38 2018 +0900
@@ -151,7 +151,27 @@
 ---  search -> checkEQ
 ---  findNode -> search
 
-putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
+open stack.SingleLinkedStack
+open stack.Element
+
+{-# TERMINATING #-}
+inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool {l}
+inStack  n s with ( top s )
+... | Nothing = True
+... | Just n1 with  compTri (key n) (key (datum n1))
+...            | tri> _ neq _ =  inStack  n ( record { top = next n1 } )
+...            | tri< _ neq _ =  inStack  n ( record { top = next n1 } )
+...            | tri≈  _ refl _  = False
+
+record StackTreeInvariant  ( n : Node ℕ ℕ )
+        ( s : SingleLinkedStack (Node  ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
+  field
+    sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
+    notInStack : inStack n s ≡ True  → ⊥
+
+open StackTreeInvariant
+
+putTest1 : (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)
          → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
            (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
@@ -160,32 +180,29 @@
    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
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
+         → 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)
+     lemma2 s STI with compTri k (key n1)
      ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
         where 
-           open stack.SingleLinkedStack
-           open stack.Element
-           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  )
-                 → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.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
+           ...          | Just n2  with compTri k k
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
            ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri≈  _ refl _  = lemma5 {!!} {!!} {!!}
+           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
            lemma5 s t n | Nothing with compTri k k
            ...            | tri≈  _ refl _  = checkEQ x _ refl
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
            ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-     ... |  tri> le eq gt = {!!}
+     ... |  tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!}  } )
      ... |  tri< le eq gt = {!!}
      lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → 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))))
-     lemma0 = lemma2 (record {top = Nothing})              
+     lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!}  ; notInStack = {!!} } )
 ...  | Nothing = lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {