Mercurial > hg > Gears > GearsAgda

changeset 585:42e8cf963c5c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add 'non inductiove record' tree, findT, replaceT, and insertT
author ryokka
date Thu, 07 Nov 2019 21:08:14 +0900
parents 7e551cef35d7
children 0ddfa505d612
files hoareRedBlackTree.agda
diffstat 1 files changed, 136 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}
-