Mercurial > hg > Gears > GearsAgda

changeset 802:6f27c2c18035

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
12/4
author mori
date Mon, 04 Dec 2023 18:05:05 +0900
parents 772a6bb0b614
children 0eee181bd715
files hoareBinaryTree1.agda work.agda
diffstat 2 files changed, 69 insertions(+), 59 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Nov 20 18:17:48 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Dec 04 18:05:05 2023 +0900
@@ -1,4 +1,3 @@
-
 module hoareBinaryTree1 where
 
 open import Level hiding (suc ; zero ; _⊔_ )
@@ -545,17 +544,17 @@
 black-depth (node key ⟪ Red , value ⟫  t t₁) = black-depth t  ⊔ black-depth t₁
 black-depth (node key ⟪ Black , value ⟫  t t₁) = suc (black-depth t  ⊔ black-depth t₁ )
 
-pro1 : { m : ℕ } → zero ≡ suc m → ⊥
-pro1 ()
-pro2 : {m : ℕ } → suc m ≡ zero → ⊥ 
-pro2 ()
+zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥
+zero≢suc ()
+suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ 
+suc≢zero ()
 {-# TERMINATING #-}
 DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n
 DepthCal zero zero zero  = refl 
-DepthCal zero zero (suc n)  = ⊥-elim (pro1 (DepthCal zero zero (suc n)))
-DepthCal zero (suc m) zero  = ⊥-elim (pro1 (DepthCal zero (suc m) zero))
-DepthCal zero (suc m) (suc n)  = ⊥-elim (pro1 (DepthCal zero (suc m) (suc n)))
-DepthCal (suc l) zero zero  = ⊥-elim (pro2 (DepthCal (suc l) zero zero ))
+DepthCal zero zero (suc n)  = ⊥-elim (zero≢suc (DepthCal zero zero (suc n)))
+DepthCal zero (suc m) zero  = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero))
+DepthCal zero (suc m) (suc n)  = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n)))
+DepthCal (suc l) zero zero  = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero ))
 DepthCal (suc l) zero (suc n)  with <-cmp (suc l) (suc n)
 ... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
 ... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
@@ -564,7 +563,7 @@
 ... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
 ... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
 ... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
-DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n )
+DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) 
 
 
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
@@ -692,16 +691,6 @@
     rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
           → k < key →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2)
 
-RBtreeCopy : {n m : Level} {A : Set n} {t : Set m} {key : ℕ} {value : A} {c : Color} → (tree tree0 : bt (Color ∧ A) )
-   → (stack : List  (bt (Color ∧ A)) )
-   → ( treeInvariant tree ∧  stackInvariant key tree tree0 stack)
-   → ( next : (tree tree0 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
-     → ( treeInvariant tree ∧  stackInvariant key tree tree0 stack )
-     → replacedRBTree key value tree0 tree → t ) 
-   → ( exit : (repl : bt (Color ∧ A)) → replacedRBTree key value tree0 repl → t ) → t
-RBtreeCopy = {!!}
-
-
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
         → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
@@ -781,12 +770,7 @@
 ... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
-{-
-ReplRBI : {n : Level} {A : Set n } {key : ℕ} {value : A } (c : Color ) → { tree1 : bt (Color ∧ A)} → (repl tree : bt (Color ∧ A)) → RBtreeInvariant tree → RBtreeInvariant tree1 → RBtreeInvariant repl
- → RBtreeInvariant (node key ⟪ c , value ⟫ tree tree1 ) → RBtreeInvariant (node key ⟪ c , value  ⟫ tree repl)
-ReplRBI Red leaf leaf rbt rbt1 rbrepl rbtt1 = {!!} --⊥-elim ( ¬(Red ≡ Black))
-ReplRBI Black (node key ⟪ c , value ⟫ t t1) (node key1 value1 l r) rbt rbt1 rbrepl rbtt1 = {!!}
--}
+
 -- findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
 --           → (stack : List (bt (Color ∧ A)))           → treeInvariant tree0 ∧  stackInvariant key tree tree0 stack
 --           → {d : ℕ} →  RBtreeInvariant tree0
@@ -912,17 +896,6 @@
       -- tree is right of parent, parent is right of grand
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
-    -- replaced done, clear stack and reconstruct tree
-    --    we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next
-    --    this means we have to check prime simple case such as replaced not is exactly the same value / color / key.
-    insertCase11 : {!!}
-    insertCase11 = {!!}
-    insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t
-    insertCase10 leaf eq refl = exit repl stack {!!} r     -- no stack, replace top node
-    insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ 
-    ... | tri< a ¬b ¬c = {!!}
-    ... | tri≈ ¬a b ¬c = next {!!} {!!} {!!} {!!}
-    ... | tri> ¬a ¬b c = {!!}
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
@@ -945,7 +918,7 @@
            --
            --     B  =>   B             B      =>         B
            --    / \     / \           / \    rotate L   / \
-           --   L   L0  L   R3        L   R  -- bad     B   B
+           --   L   L1  L   R3        L   R  -- bad     B   B
            --              / \           / \               / \      1 : child-replace
            ---            L   L2        L   B             L   L     2:  child-replace ( unbalanced )
            --                              / \                      3:  child-replace ( rotated / balanced )
@@ -974,19 +947,24 @@
                ... | tri< a ¬b ¬c = DepthCal (black-depth (left)) (black-depth left) (black-depth repl) 
                ... | tri≈ ¬a b ¬c = DepthCal (black-depth (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (black-depth left) (black-depth repl)
                ... | tri> ¬a ¬b c = DepthCal (black-depth (RBI.rot r)) (black-depth left) (black-depth repl)
-               -- rb05 should more general
+          
+               rb09 : {n : Level} {A : Set n} →  {key key1 key2 : ℕ}  {value value1  : A} {t1 t2  : bt (Color ∧ A)}
+                → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2))
+                → key < key1 
+               rb09 (rb-right-red x x1 x2) = x
+               -- rb05 should more general     
                rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree key value
                     (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
-               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl
-               ... | rb-single key₂ value₂ | refl | rb-single key₃ value₃ = ⟪ rb-right-red {!!} refl (RBI.replrb r) , {!!} ⟫
-               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = {!!}
-               ... | rb-right-black x x₁ t | refl | rb = ⟪ {!!}  , {!!} ⟫
-               ... | rb-left-black x x₁ t | refl | rb = {!!}
+               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl 
+               ... | rb-single key₂ value₂ | refl | rb-single key value = ⟪ rb-right-red (rb09 (proj1 rb05)) refl (RBI.replrb r) , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = {!!} -- cant happen ? red - red
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = {!!} --⟪ rb-right-red {!!} {!!} (RBI.replrb r) , {!!}  ⟫ -- if c₁ is Black , Cant happen . Red-leaf-leaf
+               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = {!!} --red -red
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ⟪ rb-right-red (rb09 (proj1 rb05)) {!!} (RBI.replrb r) , {!!} ⟫ -- if c₁ is Black , Cant happen . Red-leaf-leaf
+               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = {!!}-- red -red
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ⟪ rb-right-red (rb09 (proj1 rb05)) {!!} {!!} , {!!} ⟫
+               ... | rb-right-black x x₁ t | refl | rb = ⟪ proj1 {!!} , {!!} ⟫
+               ... | rb-left-black x x₁ t | refl | rb = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
                ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = {!!}
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit {!!} {!!} {!!} {!!} 
--- a/work.agda	Mon Nov 20 18:17:48 2023 +0900
+++ b/work.agda	Mon Dec 04 18:05:05 2023 +0900
@@ -16,6 +16,28 @@
 open import Relation.Nullary
 open import logic
 
+zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥
+zero≢suc ()
+suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ 
+suc≢zero ()
+{-# TERMINATING #-}
+DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n
+DepthCal zero zero zero  = refl 
+DepthCal zero zero (suc n)  = ⊥-elim (zero≢suc (DepthCal zero zero (suc n)))
+DepthCal zero (suc m) zero  = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero))
+DepthCal zero (suc m) (suc n)  = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n)))
+DepthCal (suc l) zero zero  = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero ))
+DepthCal (suc l) zero (suc n)  with <-cmp (suc l) (suc n)
+... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
+... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
+... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
+DepthCal (suc l) (suc m) zero  with <-cmp (suc l) (suc m)
+... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
+... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
+... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
+DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) 
+
+
 data bt {n : Level} (A : Set n) : Set n where
   leaf : bt A
   node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A
@@ -51,7 +73,7 @@
 testdb : ℕ
 testdb = bt-depth treeTest1 -- 4
 
-import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
+import Data.Unit --hiding ( _≟_ ;  _≤?_ ; _≤_)
 
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
   t-leaf : treeInvariant leaf
@@ -71,6 +93,12 @@
    → treeInvariant (node key2 value2 t3 t4)
    → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4))
 
+{-
+treekey : {n : Level} {A : Set n} →  {key key1 : ℕ} {value value1 : A} {t1 t2 : bt A} → treeInvariant (node key value (node key1 value1 t1 t2) leaf) → key1 < key 
+treekey (t-left x x₁) = x  -- normal level
+--treekey t-single key value  = {!!}
+-}
+
 data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A)
  → (stack : List (bt A)) → Set n where
  s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] )
@@ -162,6 +190,8 @@
 black-depth (node key ⟪ Red , value ⟫  t t₁) = black-depth t  ⊔ black-depth t₁ 
 black-depth (node key ⟪ Black , value ⟫  t t₁) = suc (black-depth t  ⊔ black-depth t₁ )
 
+
+
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
     rb-leaf :  RBtreeInvariant leaf
     rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
@@ -332,17 +362,21 @@
              ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
 rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫
 
-blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A))
+blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
   → RBtreeInvariant tree1
   → RBtreeInvariant tree2
   → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
   → black-depth tree1 ≡ black-depth tree2
-  
-blackdepth≡ leaf leaf ri1 ri2 rip = refl
-blackdepth≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru  RBinvariant kara toreruka
-blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!}
-blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!}
-
+blackdepth≡ leaf leaf ri1 ri2 rip = refl 
+blackdepth≡ {n} {A}  leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) =  DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0
+blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) =  DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) 
+blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) =  DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3))  (black-depth {n} {A} leaf)  0
+blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
+blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
+blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
+rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)}
+ →  black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄)
+rb08 = {!!}
 
 {-
 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )                        
@@ -354,5 +388,3 @@
            
 rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
 -}
-
-