# HG changeset patch # User Shinji KONO # Date 1637647916 -32400 # Node ID 7421e5c7e56c07d53be438a9357bf56e25d1522a # Parent b5fde972783094cb94fa3adb7604e35945595166 ... diff -r b5fde9727830 -r 7421e5c7e56c hoareBinaryTree.agda --- a/hoareBinaryTree.agda Mon Nov 22 22:59:08 2021 +0900 +++ b/hoareBinaryTree.agda Tue Nov 23 15:11:56 2021 +0900 @@ -108,7 +108,7 @@ -- stack always contains original top at end -- data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where - s-single : {tree0 : bt A} → ¬ ( tree0 ≡ leaf ) → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} @@ -123,7 +123,7 @@ → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t) replFromStack : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → bt A -replFromStack (s-single {tree} _ ) = tree +replFromStack (s-single {tree} ) = tree replFromStack (s-right {tree} x st) = tree replFromStack (s-left {tree} x st) = tree @@ -150,22 +150,22 @@ stack-last (x ∷ s) = stack-last s stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right (add< 2) (s-single (λ ())) +stackInvariantTest1 = s-right (add< 2) (s-single ) si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] ) -si-property0 (s-single _ ) () +si-property0 (s-single ) () si-property0 (s-right x si) () si-property0 (s-left x si) () si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack) → tree1 ≡ tree -si-property1 (s-single _ ) = refl +si-property1 (s-single ) = refl si-property1 (s-right _ si) = refl si-property1 (s-left _ si) = refl si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack → stack-last stack ≡ just tree0 -si-property-last key t t0 (t ∷ []) (s-single _) = refl +si-property-last key t t0 (t ∷ []) (s-single ) = refl si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with si-property1 si ... | refl = si-property-last key x t0 (x ∷ st) si si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 si @@ -185,7 +185,7 @@ stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A)) → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub -stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single _) = ti +stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single ) = ti stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ) = ti-right (si1 si) where si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub ) si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si @@ -280,21 +280,27 @@ → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t -replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen -replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ {!!} -- tree0 ≡ leaf -... | eq = exit {!!} (node key value leaf leaf) ⟪ {!!} , r-leaf ⟫ +replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen +replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf +... | eq = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , {!!} ⟫ replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where - repl01 : node key₁ value₁ tree right ≡ {!!} - repl01 with si-property-last _ _ _ _ {!!} - ... | eq = {!!} +... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , {!!} ⟫ where + repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right) + repl01 = ? ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫ replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen -replaceP key value {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₁ tree right ) st {!!} ≤-refl -... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl +replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre) +... | tri< a ¬b ¬c | refl = 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 x t = {!!} + ... | s-left lt si with si-property1 si + ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si ; ri = {!!} ; ci = lift tt } where + repl02 : replacedTree key value (replFromStack si) (node key₁ value₁ repl right) + repl02 = {!!} +... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen +... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) → (r : Index) → (p : Invraiant r)