Mercurial > hg > Gears > GearsAgda

changeset 688:c916adcfd3be

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 Wed, 01 Dec 2021 06:47:47 +0900
parents 5af178095ac8
children 25f89e4bc160
files hoareBinaryTree.agda
diffstat 1 files changed, 25 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 30 15:58:52 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 06:47:47 2021 +0900
@@ -296,9 +296,32 @@
 ... | 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 
-    ... | s-right lt t =  {!!}  -- can't happen
+    ... | s-right {_} {_} {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 tree₁ (node key₁ value₁ left right) 
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        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 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
+        repl02 with repl09 | <-cmp key key₂
+        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
+        ... | refl | tri≈ ¬a b ¬c = {!!}
+        ... | refl | tri> ¬a ¬b c = refl
+        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 tree₁ (node key₁ value₁ left right) ) ≡⟨ 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)) 
     ... | 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 : 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