Mercurial > hg > Gears > GearsAgda
changeset 761:6ae130db4c5b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 04 May 2023 19:30:35 +0900 |
| parents | 927c02120a73 |
| children | 3b4e31a7ccfe |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 6 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Thu May 04 18:40:10 2023 +0900 +++ b/hoareBinaryTree1.agda Thu May 04 19:30:35 2023 +0900 @@ -639,12 +639,6 @@ → stack ≡ orig ∷ [] → tree ≡ orig stackCase1 s-nil refl = refl -stackCase2 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } - → {stack : List (bt A)} → stackInvariant key tree orig stack - → stack ≡ tree ∷ orig ∷ [] → {k1 : ℕ} {v1 : A} → (orig ≡ node k1 v1 tree leaf) ∨ (orig ≡ node k1 v1 leaf tree ) -stackCase2 (s-right x s-nil) refl = case2 ? -stackCase2 (s-left x si) refl = ? - PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) ) → RBtreeInvariant orig d0 → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) @@ -802,10 +796,12 @@ insertCase1 : t insertCase1 with stackToPG tree orig stack si ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri - ... | case2 (case1 eq ) = ? where - insertCase12 : t - insertCase12 = ? - -- exit rot repl rbir ? ? + ... | case2 (case1 eq ) = insertCase12 orig si eq where + insertCase12 : (orig : bt (Color ∧ A)) → (si : stackInvariant key tree orig stack) → (eq : stack ≡ tree ∷ orig ∷ [] ) → t + insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ? + insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-right x s-nil) refl = exit rot repl rbir ? ? + insertCase12 (node k1 ⟪ Red , v1 ⟫ t1 tree) (s-left x s-nil) refl = exit rot repl rbir ? ? + insertCase12 (node k1 ⟪ Black , v1 ⟫ t1 tree) (s-left x s-nil) refl = exit rot repl rbir ? ? ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)