Mercurial > hg > Gears > GearsAgda

changeset 578:7bacba816277

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use list base simple stack
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Nov 2019 16:37:27 +0900
parents ac2293378d7a
children 821d04c0770b
files Todo.txt hoareRedBlackTree.agda redBlackTreeTest.agda
diffstat 3 files changed, 188 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/Todo.txt	Fri Nov 01 20:02:55 2019 +0900
+++ b/Todo.txt	Sat Nov 02 16:37:27 2019 +0900
@@ -1,5 +1,17 @@
+<<<<<<< working copy
+Thu May 17 15:26:56 JST 2018
+
+    findNode -> replaceNode -> getRedBlackTree だが
+
+        findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree 
+
+   という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。
+
+||||||| base
+=======
 
 
+>>>>>>> destination
 Sun May  6 17:54:50 JST 2018
 
     do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?
--- a/hoareRedBlackTree.agda	Fri Nov 01 20:02:55 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 16:37:27 2019 +0900
@@ -8,13 +8,11 @@
 open import Data.Maybe
 open import Data.Bool
 open import Data.Empty
+open import Data.List
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
-open import stack
-
-
 
 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
   field
@@ -33,66 +31,100 @@
 
 open Tree
 
+SingleLinkedStack = List
+
+emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
+emptySingleLinkedStack = []
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next ( datum ∷ stack )
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack [] cs = cs [] nothing
+popSingleLinkedStack (data1 ∷ s)  cs = cs s (just data1)
+
 data Color {n : Level } : Set n where
   Red   : Color
   Black : Color
 
-
-record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
+record Node {n : Level } (a : Set n) : Set n where
   inductive
   field
     key   : ℕ
     value : a
-    right : Maybe (Node a k)
-    left  : Maybe (Node a k)
+    right : Maybe (Node a )
+    left  : Maybe (Node a )
     color : Color {n}
 open Node
 
-record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
+record RedBlackTree {n m : Level } (a : Set n) : Set (m Level.⊔ n) where
   field
-    root : Maybe (Node a k)
-    nodeStack : SingleLinkedStack  (Node a k)
+    root : Maybe (Node a )
+    nodeStack : SingleLinkedStack  (Node a )
     -- compare : k → k → Tri A B C
     -- <-cmp 
 
 open RedBlackTree
 
-open SingleLinkedStack
-
-
 
 ----
 -- find node potition to insert or to delete, the path will be in the stack
 --
 
 {-# TERMINATING #-}
-findNode : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
-findNode {n} {m} {a} {k} {t} tree n0 next with root tree
-findNode {n} {m} {a} {k} {t} tree n0 next | nothing = next tree
-findNode {n} {m} {a} {k} {t} tree n0 next | just x with <-cmp (key x) (key n0)
-findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
-findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
-findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
+findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  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)
+findNode {n} {m} {a}  {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
+findNode {n} {m} {a}  {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
+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} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
-findNode1 {n} {m} {a} {k} {t} tree n0 next = pushSingleLinkedStack (nodeStack tree) n0 (λ st → findNode3 st n0)
+findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  a  → t) → t
+findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
   module FindNode where
-    findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → t
-    findNode2 nothing st = next tree
-    findNode2 (just x) st = findNode1 (record {root = just x ; nodeStack = st}) x next
+    findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
+    findNode2 nothing st = next record { root = nothing ; nodeStack = st }
+    findNode2 (just x) st with <-cmp (key n0) (key x)
+    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
+    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
+    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)
 
-    findNode3 : SingleLinkedStack (Node a k) → Node a k → t
-    findNode3 s1 n1 with (<-cmp (key n0) (key n1))
-    findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
-    findNode3 s1 n1 | tri< a ¬b ¬c = findNode2 (right n1) s1
-    findNode3 s1 n1 | tri> ¬a ¬b c = findNode2 (left n1) s1
+node001 : Node  ℕ 
+node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
+node002 : Node  ℕ 
+node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
+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 } )
+   node001 ( λ tree → tree )
+test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
+   node001 ( λ tree → tree )
+test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
+   node001 ( λ tree → tree )
+test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
+   node001 ( λ tree → tree )
 
 createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
-     → RedBlackTree {n} {m} {t} a b
+     → RedBlackTree {n} {m}  a 
 createEmptyRedBlackTreeℕ a b = record {
         root = nothing
      ;  nodeStack = emptySingleLinkedStack
    }
 
+popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → Maybe (Node a)
+popAllnode {n} {m} {a} tree = popAllNode1 (nodeStack tree) where
+    popAllNode1 : SingleLinkedStack (Node a ) →  Maybe (Node a)
+    popAllNode1 [] = nothing
+    popAllNode1 (x ∷ t) = just {!!}
+
+record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (ordinal now :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
+   field
+     tree+stack : popAllnode now ≡ root ordinal
+
+
+
+
+
--- a/redBlackTreeTest.agda	Fri Nov 01 20:02:55 2019 +0900
+++ b/redBlackTreeTest.agda	Sat Nov 02 16:37:27 2019 +0900
@@ -158,6 +158,14 @@
 open stack.SingleLinkedStack
 open stack.Element
 
+
+insertP :  { a : Set } { t : Set } {P : Set }   → ( f : ( a  → t )  → t )  ( g : a  → t ) ( g' :  P  → a  → t )
+   → ( p : P )
+   → ( g ≡ g' p )
+   →  f ( λ x → g' p x ) ≡ f ( λ x → g x )  
+insertP f g g' p refl = refl
+
+
 {-# TERMINATING #-}
 inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool
 inStack {l} n s with ( top s )
@@ -168,13 +176,117 @@
 ...            | tri≈  _ refl _  = false
 
 record StackTreeInvariant  ( n : Node ℕ ℕ )
+<<<<<<< working copy
+        ( s : SingleLinkedStack (Node  ℕ ℕ) )  : Set where
+||||||| base
+        ( s : SingleLinkedStack (Node  ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
+=======
         ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
+>>>>>>> destination
   field
+<<<<<<< working copy
+    -- sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
+    notInStack : inStack n s ≡ True  → ⊥
+||||||| base
+    sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
+    notInStack : inStack n s ≡ True  → ⊥
+=======
     sti : {m : Level} → replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT {m} x1 (value n)  ≡ true)
     notInStack : {m : Level} → inStack {m} n s ≡ true  → ⊥
+>>>>>>> destination
 
 open StackTreeInvariant
 
+<<<<<<< working copy
+putTest1 : (n : Maybe (Node ℕ ℕ))
+         → (k : ℕ) (x : ℕ)
+         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
+putTest1 n k x with n
+...  | Just n1 = lemma0
+   where
+     tree0 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
+     tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
+     lemma2 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s 
+         → findNode (tree0 n1 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
+              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
+     lemma2 n1 s STI with compTri k (key n1)
+     ... |  tri> le eq gt with (right n1) 
+     ...                  | Just rightNode = {!!} -- ( lemma2 rightNode  ( record { top = Just ( cons n1 (top s)  ) }   )  (record {notInStack = {!!}  } ) )
+     ...                  | Nothing with compTri k k
+     ...                           | tri≈  _ refl _ = {!!}
+     ...                           | tri< _ neq _ =  ⊥-elim (neq refl)
+     ...                           | tri> _ neq _ =  ⊥-elim (neq refl)
+     lemma2 n1 s STI |  tri< le eq gt = {!!}
+     lemma2 n1 s STI |  tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1
+        where 
+           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
+                   ( \ s1  _ -> (replaceNode (tree0 n1 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 _  =  ⊥-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)
+     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 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 n1 (record {top = Nothing}) ( record { notInStack = {!!} } )
+...  | 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 → compareT x₁ y  } ) k
+        ( λ  t x1 → checkT x1 x  ≡ True) 
+     lemma1 with compTri k k 
+     ... | tri≈  _ refl _ = checkEQ x _ refl
+     ... | tri< _ neq _ =  ⊥-elim (neq refl)
+     ... | tri> _ neq _ =  ⊥-elim (neq refl)
+||||||| base
+putTest1 : (n : Maybe (Node ℕ ℕ))
+         → (k : ℕ) (x : ℕ)
+         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
+putTest1 n k x with n
+...  | Just n1 = lemma0
+   where
+     tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
+     tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
+     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 STI with compTri k (key n1)
+     ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
+        where 
+           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 _  =  ⊥-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 = 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}) ( record { sti = {!!}  ; notInStack = {!!} } )
+...  | 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 → compareT x₁ y  } ) k
+        ( λ  t x1 → checkT x1 x  ≡ True) 
+     lemma1 with compTri k k 
+     ... | tri≈  _ refl _ = checkEQ x _ refl
+     ... | tri< _ neq _ =  ⊥-elim (neq refl)
+     ... | tri> _ neq _ =  ⊥-elim (neq refl)
+=======
 
 -- testn :  {!!}
 -- testn  =  putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2
@@ -371,3 +483,4 @@
 -- stack+tree が just だって言えたらよい
 -- {}2 は orig の どっちかのNode
 
+>>>>>>> destination