Mercurial > hg > Gears > GearsAgda

changeset 766:bc9063c6fef3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 May 2023 21:33:42 +0900
parents 292aaf8e3b0f
children 9cdf272ca38c
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat May 06 19:21:16 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat May 06 21:33:42 2023 +0900
@@ -537,11 +537,11 @@
     rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ →  {c : Color}
        → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
        → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) 1
-    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
+    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → (d : ℕ)
        → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
        → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
        → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
-    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
+    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → (d : ℕ)
        → {c c₁ : Color}
        → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
@@ -668,18 +668,18 @@
      →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → replacedRBTree key value  (child-replaced key rot) repl
      → (next : {key2 d2 : ℕ} {c2 : Color} 
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
         → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → replacedRBTree key value (child-replaced key rot) rr
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+        → (ri : rotatedTree orig rot ) → replacedRBTree key  value rot repl → t ) → t
 rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where
     rotateLeft1 : t
     rotateLeft1 with stackToPG tree orig stack si
@@ -694,18 +694,18 @@
      →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → replacedRBTree key value  (child-replaced key rot) repl
      → (next : {key2 d2 : ℕ} {c2 : Color}  
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
         → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → replacedRBTree key value  (child-replaced key rot) rr
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+        → (ri : rotatedTree orig rot ) → replacedRBTree key value  rot repl → t ) → t
 rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where
     rotateRight1 : t
     rotateRight1 with stackToPG tree orig stack si
@@ -720,18 +720,18 @@
      →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → rotatedTree tree rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → replacedRBTree key value  (child-replaced key rot) repl
      → (next : {key2 d2 : ℕ} {c2 : Color}   
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
         → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → replacedRBTree key value  (child-replaced key rot) rr
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+        → (ri : rotatedTree orig rot ) → replacedRBTree key value  rot repl → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where
     insertCase51 : t
     insertCase51 with stackToPG tree orig stack si
@@ -756,19 +756,19 @@
      →  {d  : ℕ} → RBtreeInvariant tr d →  {dr : ℕ} → RBtreeInvariant rr dr 
      → (stack : List (bt (Color ∧ A))) → stackInvariant key tr to stack
      → rotatedTree tr rot
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → replacedRBTree key value  (child-replaced key rot) rr
      → (next : {key2 d2 : ℕ} {c2 : Color}   
         → (to tr rot rr : bt (Color ∧ A)) 
         →  RBtreeInvariant to d0 
         →  {d : ℕ} → RBtreeInvariant tr d →  {dr : ℕ} → RBtreeInvariant rr dr 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
         → rotatedTree tr rot
-        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → replacedRBTree key  value  (child-replaced key rot) rr
         → length stack1 < length stack  → t )
      → (exit : (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti {c} ri next exit = ? where
+        → (ri : rotatedTree to rot ) → replacedRBTree key  value  (child-replaced key rot) repl → t ) → t
+replaceRBP {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti ri next exit = ? where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent uncle grand ) → t
@@ -810,33 +810,37 @@
           → stack ≡ tree ∷ to ∷ [] → t
         insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node k2 ⟪ Black , v2 ⟫ t1 t2)) (rb-right-red x₁ ro) eq (s-right x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 ? ins13 ins12 where
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ d ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 rrb ins13 ins12 where
              rot1 : bt (Color ∧ A)
              rot1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)
              repl1 : bt (Color ∧ A)
-             repl1 = ?
-             ins12 : replacedTree key ⟪ ? , value ⟫ (child-replaced key rot1) repl1
+             repl1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) repl 
+             ins12 : replacedRBTree key value  (child-replaced key rot1) repl1
              ins12 = ?
              ins13 : rotatedTree (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) rot1
-             ins13 = rr-node
+             ins13 = rr-node 
+             rrb : RBtreeInvariant repl1 d
+             rrb with repl | rbir 
+             ... | r1 | r2 = ?
+             -- -subst (λ k → RBtreeInvariant k d ) ? (rb-node-red ? ? d ro (subst₂ (λ j k → RBtreeInvariant j k) ? ? rbir ))
 
         -- exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?)
         --   (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti))
-        --   (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri)) 
+        --   (subst (λ k → replacedRBTree key value  ? ?) ? (r-right ? ri)) 
            -- k1 < key
            --     ⟪ red , k1 ⟫
            --   t1            tree → rot → repl
         insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-right x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-right x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-right x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq (s-right x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x₁ ro) eq (s-left x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x₁ ro) eq (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ d1 ro ro₁) eq (s-left x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-left x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-left x s-nil) refl = ?
         insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-left x s-nil) refl = ?
-        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
+        insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq (s-left x s-nil) refl = ?
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)