--- a/hoareRedBlackTree.agda	Sun Nov 03 09:27:51 2019 +0900
+++ b/hoareRedBlackTree.agda	Thu Nov 07 21:08:14 2019 +0900
@@ -6,12 +6,14 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
 open import Data.Maybe
+open import Data.Maybe.Properties
 -- open import Data.Bool
 open import Data.Empty
 open import Data.List
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
 open import logic
 
 
@@ -63,17 +65,113 @@
     root : Maybe (Node a )
     nodeStack : SingleLinkedStack  (Node a )
     -- compare : k → k → Tri A B C
-    -- <-cmp 
+    -- <-cmp
 
 open RedBlackTree
 
+-- record datum {n : Level} (a : Set n) : Set n where
+--   field
+--     key : ℕ
+--     val : a
+
+data BTree {n : Level} (a : Set n) : Set n where
+  leaf : BTree a
+  node : (left : BTree a) → (datum : ℕ) → (right : BTree a) → BTree a
+
+
+
+findT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t
+findT leaf sd st next = next leaf st
+findT (node ltree datum rtree) sd st  next with <-cmp sd datum
+findT tree@(node ltree datum rtree) sd st  next | tri≈ ¬a b ¬c = next tree st
+findT tree@(node ltree datum rtree) sd st  next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findT ltree sd st2 next)
+findT tree@(node ltree datum rtree) sd st  next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findT rtree sd st2 next)
+
+
+testTreeType : {n : Level} {a : Set n} → BTree {n} a
+testTreeType = (node (node leaf 1 leaf) 2 (node leaf 3 leaf))
+
+-- findT testTreeType 44 [] (λ t st → t)
+-- leaf
+
+-- findT testTreeType 44 [] (λ t st → st)
+-- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
+
+
+-- findT testTreeType 3 [] (λ t st → t)
+-- node leaf 3 leaf
+
+-- findT testTreeType 3 [] (λ t st → st)
+-- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []
+
+
+replaceT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
+replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf)
+replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree
+
+replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next
+
+
+replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum
+replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c =  replaceT tree n0 rstack next
+replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next
+replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c =  replaceT (node x datum (node leaf n0 leaf)) n0 rstack next
+
+
+
+replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next
+
+-- bad some code
+replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum
+replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next
+         | tri≈ ¬a b ¬c = replaceT tree n0 rstack next
+replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
+         | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next
+replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
+         | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next
+
+insertT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
+insertT tree n0 st next =  findT tree n0 st ( λ new st2 → replaceT new n0 st2 next )
+
+
+c1 : {n : Level} {a : Set n} → BTree {n} a
+c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t))))
+
+c2 : {n : Level} {a : Set n} → BTree {n} a
+c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t))))
+
+
+getkey : {n : Level } {a : Set n} → BTree {n} a → Maybe ℕ
+getkey leaf = nothing
+getkey (node tree₁ datum tree₂) = just datum
+
+find-insert : {n m  : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (just key ≡  (getkey {n} return))))
+find-insert leaf key with <-cmp key key
+find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a )
+find-insert leaf key | tri≈ ¬a b ¬c = refl
+find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c )
+find-insert tr@(node any₁ datum any₂) key with <-cmp key datum
+find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!}
+find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!}
+find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum
+find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!}
+find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!}
+find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!}
+
+-- where
+-- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t
+-- find-lemma leaf ke st nt = nt leaf st
+-- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum
+-- find-lemma tt@(node tr datum tr₁) ke st nt | tri< a ¬b ¬c = find-lemma tr ke (tt ∷ st) nt
+-- find-lemma tt@(node tr datum tr₁) ke st nt | tri≈ ¬a b ¬c = nt tt st
+-- find-lemma tt@(node tr datum tr₁) ke st nt | tri> ¬a ¬b c = find-lemma tr₁ ke (tt ∷ st) nt
 
 ----
 -- find node potition to insert or to delete, the path will be in the stack
 --
 
 {-# TERMINATING #-}
-findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
+findNode : {n m  : Level } {a : Set n} {t : Set m} → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
 findNode {n} {m} {a}  {t} tree n0 next with root tree
 findNode {n} {m} {a}  {t} tree n0 next | nothing = next tree
 findNode {n} {m} {a}  {t} tree n0 next | just x with <-cmp (key x) (key n0)
@@ -82,6 +180,7 @@
 findNode {n} {m} {a}  {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
 
 
+
 findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
 findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
   module FindNode where
@@ -92,11 +191,11 @@
     ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
     ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)
 
-node001 : Node  ℕ 
+node001 : Node  ℕ
 node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
-node002 : Node  ℕ 
+node002 : Node  ℕ
 node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
-node003 : Node  ℕ 
+node003 : Node  ℕ
 node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }
 
 test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
@@ -112,10 +211,10 @@
 replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
   module FindNodeR where
       replaceNode1 : (Maybe (Node a )) → Node a
-      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  } 
-      replaceNode1 (just x)  = record n0 { left = left x ; right = right x } 
+      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  }
+      replaceNode1 (just x)  = record n0 { left = left x ; right = right x }
       replaceNode2 : SingleLinkedStack (Node a ) → (Node a  → t)  → t
-      replaceNode2 [] next = next ( replaceNode1 (root tree) ) 
+      replaceNode2 [] next = next ( replaceNode1 (root tree) )
       replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
       replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
       replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
@@ -125,7 +224,7 @@
 insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
 
 createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
-     → RedBlackTree {n}  a 
+     → RedBlackTree {n}  a
 createEmptyRedBlackTreeℕ a b = record {
         root = nothing
      ;  nodeStack = emptySingleLinkedStack
@@ -133,33 +232,50 @@
 
 findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
 findNodeLeft x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
-findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h))
+findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) -- stack の top と比較するのはたぶん replace ...?
+
 findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
 findNodeRight x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
 findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))
 
+findNodeLoop : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
+findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))
+
+
+
 data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
-   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now 
+   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now
    fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st record { root = nothing ; nodeStack = st }
    fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
       →  FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st →  FindNodeInvariant st original
    fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
       →  FindNodeInvariant ( x ∷ st ) original → findNodeRight x st →  FindNodeInvariant st original
+   -- fni-loop  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → FindNodeInvariant st original
 
 
 findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
-     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) 
+     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t )
      → ( FindNodeInvariant (nodeStack tree)  tree) → t
-findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
+findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev
   module FindNodeH where
-    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
-    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!}
-    findNode2h (just x) st prev with <-cmp (key n0) (key x)
-    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
-    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
-    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
+    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree  → t
+    findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev
+    findNode2h (just x) st n0 prev with <-cmp (key n0) (key x)
+    ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
+    ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) )
+        where
+          nextInvaliant : ({!!})
+          nextInvaliant = {!!}
+          lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a)
+          lproof ns [] with left ns | right ns
+          lproof ns [] | just x | just x₁ = {!!}
+          lproof ns [] | just x | nothing =  {!!}
+          lproof ns [] | nothing | just x = {!!}
+          lproof ns [] | nothing | nothing = {!!}
+          lproof ns (x ∷ ss) = {!!}
+
+    ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) )
 
 
 -- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
 -- replaceNodeH = {!!}
-