Mercurial > hg > Gears > GearsAgda

changeset 883:9ec8c2f6b92d

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 Fri, 10 May 2024 17:50:38 +0900
parents 9f62da6d787c
children cff51057ddd8
files hoareBinaryTree1.agda
diffstat 1 files changed, 25 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat May 04 21:48:04 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri May 10 17:50:38 2024 +0900
@@ -1312,22 +1312,31 @@
         rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
         rr03 = proj1 (proj2 rr01)
         rr04 = proj2 (proj2 rr01)
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) (node key₂ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₂ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) (node key₂ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₂ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₂ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₂ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₃ t₅ t₇))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₂ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₂ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) (node key₃ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₃ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₄ value₃ t₅ t₇))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) (node key₃ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₃ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node kn ⟪ Red , _ ⟫ leaf leaf) leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt ⟪ <-trans lt2 x₃ , ⟪ <-tr> x₄ lt2 , <-tr> x₅ lt2 ⟫ ⟫  (t-single _ _) (t-right _ _ x₃ x₄ x₅ ti) 
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt tt ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫  (t-single _ _) (t-right _ _ x₄ x₇ x₈ ti₁) where
+        rr00 : (kg < kn) ∧ ⊤ ∧ ⊤
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁
+        rr01 : (kn < kp) ∧ ⊤ ∧ ⊤
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-left key₂ .kp x₃ x₄ x₅ ti)) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb
+... | t-left .key₁ .kn x₆ x₇ x₈ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₆ , ⟪ x₇ , x₈ ⟫ ⟫ tt tt  (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-single _ _) where
+        rr00 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁
+        rr02 = proj1 (proj2 rr00)
+        rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₄ , x₅ ⟫ ⟫
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) .(node key₃ _ _ _))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-node key₂ .kp key₃ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) with RB-repl→ti _ _ _ _ ti trb
+... | t-left .key₁ .kn x₉ x₁₀ x₁₁ t = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt ⟪ x₉ , ⟪ x₁₀ , x₁₁ ⟫ ⟫ tt ⟪ <-trans (proj1 rr01) x₄  , ⟪ <-tr> x₇ (proj1 rr01)  , <-tr> x₈ (proj1 rr01) ⟫ ⟫   (t-right _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) t) (t-right _ _ x₄ x₇ x₈ ti₁) where
+        rr00 : (kg < kn) ∧ ((kg < key₁) ∧ tr> kg t₂ ∧ tr> kg t₃) ∧ ⊤
+        rr00 = RB-repl→ti> _ _ _ _ _ trb lt1 x₁
+        rr02 = proj1 (proj2 rr00)
+        rr01 : (kn < kp) ∧ ((key₁ < kp) ∧ tr< kp t₂ ∧ tr< kp t₃) ∧ ⊤
+        rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 ⟪ x₃ , ⟪ x₅ , x₆ ⟫ ⟫
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ t₅)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl t₂ .leaf kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ t₅)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl t₂ .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ t₅)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl t₂ .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster