Mercurial > hg > Gears > GearsAgda

changeset 700:adb7c2101f67

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 Sun, 05 Dec 2021 07:21:42 +0900
parents 59f80c1049e9
children 690da797cf40
files hoareBinaryTree.agda
diffstat 1 files changed, 24 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sat Dec 04 19:51:58 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Dec 05 07:21:42 2021 +0900
@@ -267,6 +267,8 @@
 lemma3 refl ()
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
 lemma5 (s≤s z≤n) ()
+¬x<x : {x : ℕ} → ¬ (x < x)
+¬x<x (s≤s lt) = ¬x<x lt
 
 child-replaced :  {n : Level} {A : Set n} (key : ℕ)   (tree : bt A) → bt A
 child-replaced key leaf = leaf
@@ -531,7 +533,11 @@
       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₂ ti ti₁) (r-right x ri) =
       t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ti (RTtoTI0 _ _ key value ti₁ ri)
-RTtoTI0 .(node _ _ _ _) .(node _ _ _ _) key value ti (r-left x ri) = {!!}
+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 _ _ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ ti) (r-left x r-leaf) = {!!}
+RTtoTI0 .(node _ _ (node key _ _ _) _) .(node _ _ (node key value _ _) _) key value ti (r-left x r-node) = {!!}
+RTtoTI0 .(node _ _ (node _ _ _ _) _) .(node _ _ (node _ _ _ _) _) key value ti (r-left x (r-right x₁ ri)) = {!!}
+RTtoTI0 .(node _ _ (node _ _ _ _) _) .(node _ _ (node _ _ _ _) _) key value ti (r-left x (r-left x₁ ri)) = {!!}
 
 RTtoTI1  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
      → replacedTree key value tree repl → treeInvariant tree
@@ -633,8 +639,8 @@
    findP2 | r-right x ri | node key value t t₁ | record { eq = refl } = record { tree1 = t₁ ; ci =  ri }
    findP2 | r-leaf | leaf | record { eq = eq } = ⊥-elim ( nat-≤> c ≤-refl )
 
-containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
-containsTree {n} {m} {A} {t} tree tree1 key value P RT =
+containsTree : {n : Level} {A : Set n} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
+containsTree {n}  {A}  tree tree1 key value P RT =
    TerminatingLoopS (bt A ∧ List (bt A) )
      {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) 
               ⟪ tree , tree ∷ []  ⟫ record { tree0 = tree ; ti0 = RTtoTI0 _ _ _ _ P RT ; ti = RTtoTI0 _ _ _ _ P RT ; si = s-single
@@ -643,11 +649,23 @@
        $ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where
            lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value )) → top-value t1 ≡ just value
            lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1  (findPR.ci P2)) (findPC.ci  (findPR.ci P2)) (findPR.si P2) found? where
+              lemma8 : {tree1 t1 : bt A } → replacedTree key  value tree1 t1 → node-key t1 ≡ just key → top-value t1 ≡ just value
+              lemma8 {.leaf} {node key value .leaf .leaf} r-leaf refl = refl
+              lemma8 {.(node key _ t1 t2)} {node key value t1 t2} r-node refl = refl
+              lemma8 {.(node key value t1 _)} {node key value t1 t2} (r-right x ri) refl = ⊥-elim (¬x<x x)
+              lemma8 {.(node key value _ t2)} {node key value t1 t2} (r-left x ri) refl = ⊥-elim (¬x<x x)
               lemma7 :  (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A)
                  → replacedTree key  value tree1 t1 → stackInvariant key t1 tree0 s1
                  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →   top-value t1 ≡ just value
               lemma7 .leaf (.leaf ∷ []) .leaf tree1 () s-single (case1 refl)
-              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ []) .(node key value t1 t2) tree1 ri s-single (case2 x) = {!!}
-              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) (case2 x₂) = {!!}
-              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) (case2 x₂) = {!!}
+              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ []) .(node key value t1 t2) tree1 ri s-single (case2 x) = lemma8 ri x
+              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) (case2 x₂) = lemma8 ri x₂
+              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) (case2 x₂) = lemma8 ri x₂
+
 
+containsTree1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
+containsTree1 {n} {A} tree key value ti =
+       insertTreeP tree key value ti
+     $ λ tree0 tree1 P → containsTree tree1 tree0 key value (RTtoTI1 _ _ _ _ (proj1 P) (proj2 P) ) (proj2 P) -- (proj1 P) (proj2 P)
+
+