Mercurial > hg > Gears > GearsAgda

changeset 687:5af178095ac8

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 Tue, 30 Nov 2021 15:58:52 +0900
parents 4efb74d28d6a
children c916adcfd3be
files hoareBinaryTree.agda
diffstat 1 files changed, 32 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 30 09:35:22 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 30 15:58:52 2021 +0900
@@ -120,7 +120,7 @@
     r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
           → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
     r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k > key →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
+          → key < k →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
 
 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
 add<  {i} j = begin
@@ -255,19 +255,19 @@
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
 lemma5 (s≤s z≤n) ()
 
-child-replaced :  {n : Level} {A : Set n} (key : ℕ) (value : A) (stack : List (bt A)) (tree tree0 : bt A) → stackInvariant key tree tree0 stack  → bt A
-child-replaced key value .(tree ∷ []) tree .tree s-single = tree
-child-replaced key value .(leaf ∷ _) leaf tree0 (s-right x si) = leaf
-child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-right x si) = tree
-child-replaced key value .(leaf ∷ _) leaf tree0 (s-left x si) = leaf
-child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-left x si) = tree₁
+child-replaced :  {n : Level} {A : Set n} (key : ℕ)   (tree : bt A) → bt A
+child-replaced key leaf = leaf
+child-replaced key (node key₁ value left right) with <-cmp key key₁
+... | tri< a ¬b ¬c = left
+... | tri≈ ¬a b ¬c = node key₁ value left right
+... | tri> ¬a ¬b c = right
 
 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
    field
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant key tree tree0 stack
-     ri : replacedTree key value (child-replaced key value stack tree tree0 si) repl
+     ri : replacedTree key value (child-replaced key tree ) repl
      ci : C tree repl stack     -- data continuation
    
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
@@ -286,9 +286,8 @@
 replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
 ... | refl  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  r-leaf ⟫
 replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
-    repl06 : child-replaced key value  (node key₁ value₁ left right ∷ []) tree (replacePR.tree0 Pre) (replacePR.si Pre)  ≡ node key₁ value₁ left right
-    repl06 with replacePR.si Pre
-    ... | s-single = refl
+    repl06 : child-replaced key  tree  ≡ node key₁ value₁ left right
+    repl06 = {!!}
     repl01 : replacedTree key value (replacePR.tree0 Pre) repl  
     repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
     repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
@@ -296,25 +295,32 @@
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
-    Post with replacePR.si Pre | inspect replacePR.si Pre | replacePR.ri Pre
-    ... | s-left x t | record { eq = refl } | ri = {!!}  -- can't happen
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si | record { eq = refl } | ri = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
-        repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
+    Post with replacePR.si Pre 
+    ... | s-right lt t =  {!!}  -- can't happen
+    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
         repl10 with si-property1 si
         ... | refl = si
-        repl12 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
-        repl12 with repl09 | repl10 
-        ... | refl | s-single =  {!!} where -- key ≡ key₂ → ⊥ -- child-replaced ≡ leaf
-            repl03 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) s-single   ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
-            repl03 = refl
-        ... | refl | s-right lt2 si2 =  {!!} where -- key₂ < key, key₂ < key₁, key < key₁ -- child-replaced ≡ right
-            repl04 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) (s-right lt2 si2) ≡ tree₁
-            repl04 = refl
-        ... | refl | s-left lt2 si2 = r-left a (replacePR.ri Pre) where
-            repl05 : child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) (s-left lt2 si2)  ≡ node key₁ value₁ left right
-            repl05 = refl
+        repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
+        repl03 with <-cmp key key₁ 
+        ... | tri< a1 ¬b ¬c = refl
+        ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
+        ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
+        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
+        repl02 with repl09 | <-cmp key key₂
+        ... | refl | tri< a ¬b ¬c = refl
+        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+        repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
+        repl04  = begin
+            node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03  ⟩
+            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+            child-replaced key tree1 ∎  where open ≡-Reasoning
+        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ repl right)
+        repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04  (r-left a (replacePR.ri Pre)) 
 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl