Mercurial > hg > Gears > GearsAgda

changeset 830:1cce147edddb

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, 05 Mar 2024 16:25:47 +0900
parents 2a19292edd88
children 0b0a54d7d683
files hoareBinaryTree1.agda
diffstat 1 files changed, 19 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Mar 05 14:23:33 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Mar 05 16:25:47 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₁
 
 --
 --
@@ -55,20 +55,20 @@
     t-leaf : treeInvariant leaf
     t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf)
     t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ 
-       → tr< key t₁
-       → tr< key t₂
+       → tr> key t₁
+       → tr> key t₂
        → treeInvariant (node key₁ value₁ t₁ t₂)
        → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
     t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ 
-       → tr> key t₁
-       → tr> key t₂
+       → tr< key₁ t₁
+       → tr< key₁ t₂
        → 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₄))
@@ -104,8 +104,8 @@
 
 treeInvariantTest1  : treeInvariant treeTest1
 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) )
+    ⟪ 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
@@ -505,7 +505,13 @@
 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₁
 RTtoTI0 (node key₁ _ leaf right@(node key₂ _ left₁ right₁)) (node key₁ value₁ leaf right₃@(node key₃ _ left₂ right₂)) key value (t-right x₁ a b ti) (r-right x ri) =
-      t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri)
+      t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) rr00 ? (RTtoTI0 _ _ key value ti ri) where
+         rr00 : tr> key₁ left₂
+         rr00 with RTtoTI0 _ _ key value ti ri
+         ... | t-single key₃ value = tt
+         ... | t-right x x₁ x₂ t = tt
+         ... | t-left x₃ x₄ x₅ t = ?
+         ... | t-node x x₁ x₂ x₃ x₄ x₅ t t₁ = ?
 RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ a b ti) (r-right x ())
 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)