Mercurial > hg > Gears > GearsAgda

changeset 828:c9850c226195

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 Thu, 29 Feb 2024 17:35:40 +0900
parents 8ebf6fcc353b
children 2a19292edd88
files hoareBinaryTree1.agda
diffstat 1 files changed, 32 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Feb 28 10:05:56 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Feb 29 17:35:40 2024 +0900
@@ -43,11 +43,11 @@
 
 tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
 tr< {_} {A} key leaf = ⊤
-tr< {_} {A} key (node key₁ value tr tr₁) = key < key₁ → tr< key tr  ∧  tr< key tr₁
+tr< {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr< key tr  ∧  tr< key tr₁
 
 tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
 tr> {_} {A} key leaf = ⊤
-tr> {_} {A} key (node key₁ value tr tr₁) = key₁ < key → tr> key tr  ∧  tr> key tr₁
+tr> {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr> key tr  ∧  tr> key tr₁
 
 --
 --
@@ -65,10 +65,10 @@
        → treeInvariant (node key value t₁ t₂)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
     t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
-       → tr< key₁ t₁ 
-       → tr< key₁ t₂ 
-       → tr> key₁ t₃
-       → tr> key₁ t₄
+       → tr> key₁ t₁ 
+       → tr> key₁ t₂ 
+       → tr< key₁ t₃
+       → tr< key₁ t₄
        → treeInvariant (node key value t₁ t₂)
        → treeInvariant (node key₂ value₂ t₃ t₄)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
@@ -103,7 +103,9 @@
 treeTest2  =  node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
 
 treeInvariantTest1  : treeInvariant treeTest1
-treeInvariantTest1  = t-right (m≤m+n _ 2) ? ? (t-node (add< 0) (add< 1) ? ? ? ? (t-left (add< 0) ? ? (t-single 1 7)) (t-single 5 5) )
+treeInvariantTest1  = t-right (m≤m+n _ 2) 
+    ⟪ (add< _) , ⟪ ⟪ (add< _) , _ ⟫ , _ ⟫ ⟫
+    ⟪ (add< _) , ⟪ _ , _ ⟫ ⟫ (t-node (add< 0) (add< 1) ⟪ (add< _) , ⟪ _ , _ ⟫ ⟫  _ _ _ (t-left (add< 0) _ _ (t-single 1 7)) (t-single 5 5) )
 
 stack-top :  {n : Level} {A : Set n} (stack  : List (bt A)) → Maybe (bt A)
 stack-top [] = nothing
@@ -143,16 +145,16 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
-Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
-Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
-Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ?
-Diffkey A tree0 key leaf .(leaf ∷ _) (s-right .leaf .tree0 tree₁ x si) = ?
-Diffkey A tree0 key (node key₁ value tree tree₂) .(node key₁ value tree tree₂ ∷ _) (s-right .(node key₁ value tree tree₂) .tree0 tree₁ x si) = ?
-Diffkey A tree0 key tree .(tree ∷ _) (s-left .tree .tree0 tree₁ x si) = ?
+-- Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
+-- Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
+-- Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ?
+-- Diffkey A tree0 key leaf .(leaf ∷ _) (s-right .leaf .tree0 tree₁ x si) = ?
+-- Diffkey A tree0 key (node key₁ value tree tree₂) .(node key₁ value tree tree₂ ∷ _) (s-right .(node key₁ value tree tree₂) .tree0 tree₁ x si) = ?
+-- Diffkey A tree0 key tree .(tree ∷ _) (s-left .tree .tree0 tree₁ x si) = ?
 
-si-property-ne :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
-   → length stack > 1 → ¬ ( node-key tree ≡ just key )
-si-property-ne = ?
+-- si-property-ne :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
+--    → length stack > 1 → ¬ ( node-key tree ≡ just key )
+-- si-property-ne = ?
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
@@ -223,9 +225,9 @@
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
-replaceTree1 k v1 value (t-right x a b t) = t-right x ? ? t
-replaceTree1 k v1 value (t-left x a b t) = t-left x ? ? t
-replaceTree1 k v1 value (t-node x x₁ a b c d t t₁) = t-node x x₁ ? ? ? ? t t₁
+replaceTree1 k v1 value (t-right x a b t) = t-right x a b t
+replaceTree1 k v1 value (t-left x a b t) = t-left x a b t
+replaceTree1 k v1 value (t-node x x₁ a b c d t t₁) = t-node x x₁ a b c d t t₁
 
 open import Relation.Binary.Definitions
 
@@ -496,9 +498,9 @@
      → replacedTree key value tree repl → treeInvariant repl
 RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value
 RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single key value
-RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x ? ? ti
-RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x ? ? ti
-RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ ? ? ? ? ti ti₁
+RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti
+RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti
+RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁
 -- r-right case
 RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x ? ? (t-single key value)
 RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ a b ti) (r-right x ri) = t-single key₁ value₁
@@ -508,35 +510,35 @@
 RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ a b ti) (r-right x r-leaf) =
       t-node x₁ x ? ? ? ? ti (t-single key value)
 RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) =
-      t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ? ? ? ?  ti (RTtoTI0 _ _ key value ti₁ ri)
+      t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) a b ? ?  ti (RTtoTI0 _ _ key value ti₁ ri)
 -- r-left case
 RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left x ? ? (t-single _ _ )
 RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ a b ti) (r-left x r-leaf) = t-node x x₁ ? ? ? ? (t-single key value) ti
 RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
       t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
-RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  ? ? ? ? (RTtoTI0 _ _ key value ti ri) ti₁
+RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂  ? ? c d (RTtoTI0 _ _ key value ti ri) ti₁
 
 RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
      → replacedTree key value tree repl → treeInvariant tree
 RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
 RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
-RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x ? ? ti
-RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x ? ? ti
-RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ ? ? ? ? ti ti₁
+RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti
+RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti
+RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁
 -- r-right case
 RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁
 RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) =
    t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ?  (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
 RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) =
     t-left x₁ ? ? ti
-RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) ? ? ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
+RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
 -- r-left case
 RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁
 RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) =
    t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
-RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ ? ? ti₁
+RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ c d ti₁
 RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) =
-    t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? ? ? (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
+    t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
 
 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
      → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t