# HG changeset patch
# User ryokka
# Date 1522054204 -32400
# Node ID 7d9af1d4b5af2114bbb6f97f799878cd6fe34c45
# Parent  5f4c5a66321969a6eec8aa79cdc5537795978803
add compareTri

diff -r 5f4c5a663219 -r 7d9af1d4b5af Todo.txt
--- a/Todo.txt	Thu Jan 18 10:38:55 2018 +0900
+++ b/Todo.txt	Mon Mar 26 17:50:04 2018 +0900
@@ -1,3 +1,10 @@
+Mon Mar 26 17:43:06 JST 2018
+
+    Decidable を使って Compare の場合分けを行う
+    Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
+    場合分けには Trichotomous を使う
+    compareTri を完成させる               
+
 Fri Jan  5 16:43:26 JST 2018
 
     unbalanced binary search tree の動作を調べる
diff -r 5f4c5a663219 -r 7d9af1d4b5af redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Thu Jan 18 10:38:55 2018 +0900
+++ b/redBlackTreeTest.agda	Mon Mar 26 17:50:04 2018 +0900
@@ -4,7 +4,10 @@
 open import stack
 open import Level hiding (zero)
 
+open import Data.Empty
+
 open import Data.Nat
+open import Relation.Nullary
 
 open Tree
 open Node
@@ -125,6 +128,26 @@
 -- compare2  zero (suc _) = LT
 -- compare2  (suc x) (suc y) = compare2 x y
 
+compareTri1 : (n : ℕ) -> zero < ℕ.suc n 
+compareTri1 zero = {!!}
+compareTri1 (suc n) = {!!}
+
+compareTri :  Trichotomous  _≡_ _<_
+compareTri zero zero = tri≈ (\()) refl (\())
+compareTri zero (suc n) = tri< {!!} (\()) (\())
+compareTri (suc n) zero = tri> (\()) (\()) {!!}
+compareTri (suc n) (suc m) with compareTri n m
+... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!}
+... | tri< p q r = tri<  {!!} {!!} {!!}
+... | tri> p q r = tri> {!!} {!!} {!!}
+
+compareDecTest : (n n1 : Node ℕ ℕ) -> key n ≡ key n1
+compareDecTest n n1 with (key n) ≟ (key n1)
+...  | yes p = p
+...  | no ¬p  = {!!}
+
+
+
 putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
 putTest1Lemma2 zero = refl
 putTest1Lemma2 (suc k) = putTest1Lemma2 k
@@ -173,7 +196,7 @@
      lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
          GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
      lemma2 s with compare2 k (key n1)
-     ... |  EQ = lemma3 ?
+     ... |  EQ = lemma3 {!!}
         where 
            lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black