Mercurial > hg > Gears > GearsAgda

changeset 650:11388cab162f

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, 20 Nov 2021 08:34:59 +0900
parents cc62eb4758b0
children 7b9d35f7c033
files hoareBinaryTree.agda
diffstat 1 files changed, 16 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sat Nov 20 06:36:02 2021 +0900
+++ b/hoareBinaryTree.agda	Sat Nov 20 08:34:59 2021 +0900
@@ -113,9 +113,9 @@
     r-leaf : replacedTree key value leaf (node key value leaf leaf)
     r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
     r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k > key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t t1) (node k v1 t t2) 
+          → k < key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t t1) (node k v1 t t2) 
     r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 
+          → k > key →  replacedTree key value t1 t2 →  replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 
 
 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
 add<  {i} j = begin
@@ -188,7 +188,7 @@
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
 
 depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
-depth-2< {i} {j} = s≤s (m≤n⊔m _ i)
+depth-2< {i} {j} = s≤s (m≤n⊔m j i)
 
 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
 depth-3< {zero} = s≤s ( z≤n )
@@ -238,6 +238,8 @@
 
 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
 nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
 lemma3 refl ()
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
@@ -266,23 +268,25 @@
     repl3 (s-right x ())
     repl3 (s-left x ())
 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) (node key₁ value₁ left tree ∷ st)
-                  ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-right a (proj2 (proj2 Pre))  ⟫ ⟫ {!!} where
-    repl5 :  stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 (node key₁ value₁ left tree ∷ st )
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st)
+                  ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre))  ⟫ ⟫ ≤-refl where
+    repl5 :  stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
     repl5 (s-right x si) with  si-property1 _ _ _ _ si
-    ... | refl = ⊥-elim ( nat-≤> a {!!} )
+    ... | refl = ⊥-elim (nat-<> a x)
     repl5 (s-left x si) with  si-property1 _ _ _ _ si
-    ... | refl = {!!} -- suc key ≤ key₁  , suc key ≤ key₁
+    ... | refl = si 
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
 ... | tri> ¬a ¬b c = next key value  (node key₁ value₁ repl right ) st {!!}  ≤-refl
 ... | tri≈ ¬a b ¬c = next key value  (node key value left right ) st {!!}  ≤-refl where -- this case won't happen
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl)  st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) ,  r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   where
-    repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right )  st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) ,  r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   where
+    repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 st
     repl2 (s-single .(node key₁ value₁ left right)) = {!!}
-    repl2 (s-right _ si) = {!!}
-    repl2 (s-left _ si) = {!!}
+    repl2 (s-right x si) with si-property1 _ _ _ _ si
+    ... | eq = {!!}
+    repl2 (s-left x si) with si-property1 _ _ _ _ si
+    ... | eq = ?
 
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)