# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1516090469 -32400
# Node ID bc3208d510cdf548f15af3ecb586af1c88a40159
# Parent  c304869ac43907144cdac4e51a93013a0ab372ed
add some

diff -r c304869ac439 -r bc3208d510cd RedBlackTree.agda
--- a/RedBlackTree.agda	Sun Jan 14 17:57:38 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 16 17:14:29 2018 +0900
@@ -166,7 +166,7 @@
     insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
 
 ----
--- find node potition to insert or to delete, the pass will be in the stack
+-- find node potition to insert or to delete, the path will be in the stack
 -- 
 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
 findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
@@ -215,11 +215,17 @@
 ... | equal _ = EQ
 ... | greater _ _ = GT
 
+compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
+compare2 zero zero = EQ
+compare2 (suc _) zero = GT
+compare2  zero (suc _) = LT
+compare2  (suc x) (suc y) = compare2 x y
+
 
 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
      ;  nodeStack = emptySingleLinkedStack
-     ;  compare = compareℕ
+     ;  compare = compare2
    }
  
diff -r c304869ac439 -r bc3208d510cd redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Sun Jan 14 17:57:38 2018 +0900
+++ b/redBlackTreeTest.agda	Tue Jan 16 17:14:29 2018 +0900
@@ -29,13 +29,19 @@
 ...  | equal _ = True
 ...  | _ = False
 
-test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True   ))
+check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check2 Nothing _ = False
+check2 (Just n)  x with compare2 (value n)  x
+...  | EQ = True
+...  | _ = False
+
+test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
 test1 = refl
 
 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
     \t -> putTree1 t 2 2 (
     \t -> getRedBlackTree t 1 (
-    \t x -> check1 x 1 ≡ True   )))
+    \t x -> check2 x 1 ≡ True   )))
 test2 = refl
 
 open ≡-Reasoning
@@ -44,9 +50,9 @@
     $ \t -> putTree1 t 3 3
     $ \t -> putTree1 t 4 4    
     $ \t -> getRedBlackTree t 1
-    $ \t x -> check1 x 1 ≡ True  
+    $ \t x -> check2 x 1 ≡ True  
 test3 = begin
-    check1 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
+    check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
   ≡⟨ refl ⟩
     True
   ∎
@@ -94,13 +100,13 @@
     $ \t -> putTree1 t 2 2 (\ t -> root t)
 
 
-test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True   ))
+test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
 test9 = refl
 
 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
     \t -> putRedBlackTree t 2 2 (
     \t -> getRedBlackTree t 1 (
-    \t x -> check1 x 1 ≡ True   )))
+    \t x -> check2 x 1 ≡ True   )))
 test10 = refl
 
 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
@@ -111,13 +117,13 @@
 
 
 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
-redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ }
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
 
-compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
-compare2 zero zero = EQ
-compare2 (suc _) zero = GT
-compare2  zero (suc _) = LT
-compare2  (suc x) (suc y) = compare2 x y
+-- compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
+-- compare2 zero zero = EQ
+-- compare2 (suc _) zero = GT
+-- compare2  zero (suc _) = LT
+-- compare2  (suc x) (suc y) = compare2 x y
 
 putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
 putTest1Lemma2 zero = refl
@@ -147,21 +153,24 @@
 putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 
 
+compareLemma1 : (x  y : ℕ)  -> compareℕ x y ≡ EQ -> x  ≡ y
+compareLemma1 x y eq with compareℕ x y  | eq 
+... | EQ | refl = ?
+
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          -> (k : ℕ) (x : ℕ) 
          -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-         (\ t -> getRedBlackTree t k (\ t x1 -> check1 x1 x  ≡ True)) 
+         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True)) 
 putTest1 n k x with n
 ...  | Just n1 = {!!}
-...  | Nothing = {!!}
+...  | Nothing =  lemma1  
+   where 
+     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red 
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
+        ( \ t x1 -> check2 x1 x  ≡ True) 
+     lemma1 = {!!}
 
 
--- with Data.Nat.compare k (key (leafNode k x))
--- ...            | Data.Nat.equal _ = ?
 
--- begin
---     ?
---   ≡⟨ ? ⟩
---     True
---   ∎