# HG changeset patch # User Shinji KONO # Date 1718200017 -32400 # Node ID f2a3f5707075074d6d2b89727cebfa94ad8876f0 # Parent 0cf53f1e0055605e2f12f3608649079c45740e83 ... diff -r 0cf53f1e0055 -r f2a3f5707075 ModelChecking.agda --- a/ModelChecking.agda Tue Jun 11 22:37:13 2024 +0900 +++ b/ModelChecking.agda Wed Jun 12 22:46:57 2024 +0900 @@ -15,7 +15,7 @@ open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import logic -open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) +open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) open import Relation.Binary.Definitions record AtomicNat : Set where diff -r 0cf53f1e0055 -r f2a3f5707075 hoareBinaryTree.agda --- a/hoareBinaryTree.agda Tue Jun 11 22:37:13 2024 +0900 +++ b/hoareBinaryTree.agda Wed Jun 12 22:46:57 2024 +0900 @@ -7,7 +7,7 @@ open import Data.Maybe -- open import Data.Maybe.Properties open import Data.Empty -open import Data.List +open import Data.List hiding ( find ) open import Data.Product open import Function as F hiding (const) @@ -107,7 +107,7 @@ found? (leaf ∷ st) tree = empty tree found? (node key value x x₁ ∷ st) tree = next value tree -open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) +open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where t-leaf : treeInvariant leaf @@ -235,7 +235,7 @@ depth-1< {i} {j} = s≤s (m≤m⊔n _ j) depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) -depth-2< {i} {j} = s≤s {! !} +depth-2< {i} {j} = s≤s (m≤n⊔m j i) depth-3< : {i : ℕ } → suc i ≤ suc (suc i) depth-3< {zero} = s≤s ( z≤n ) @@ -542,7 +542,7 @@ → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) -... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) @@ -721,19 +721,23 @@ findext01 : {key₂ : ℕ} {tree₁ : bt A} {tree₂ : bt A} {st : List (bt A)} {v1 : A} → (Pre : findPR key (node key₂ v1 tree₁ tree₂) st (findPC value) ) → key < key₂ → findPC value key tree₁ (tree₁ ∷ st) - findext01 Pre a with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre) | inspect findPC.tree1 (findPR.ci Pre) - ... | r-leaf | leaf | record { eq = refl } = ⊥-elim ( nat-≤> a ≤-refl) - ... | r-node | node key value t1 t3 | record { eq = refl } = ⊥-elim ( nat-≤> a ≤-refl ) - ... | r-right x t | t1 | t2 = ⊥-elim (nat-<> x a) - ... | r-left x ri | node key value t1 t3 | record { eq = refl } = record { tree1 = t1 ; ci = ri } + findext01 Pre a with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre) in eqp + ... | r-leaf | leaf = ⊥-elim ( nat-≤> a ≤-refl) + ... | r-node | node key value t1 t3 = ⊥-elim ( nat-≤> a ≤-refl ) + ... | r-right x t | t1 = ⊥-elim (nat-<> x a) + ... | r-left {key₂} {v1} {_} {t2} {tree₂} x ri | node key value t1 t3 = record { tree1 = t1 ; ci = subst (λ k → replacedTree _ _ k _) (lemma01 eqp) ri } where + lemma01 : {t2 : bt A} → node key₂ v1 t2 tree₂ ≡ node key value t1 t3 → t2 ≡ t1 + lemma01 refl = refl findext02 : {key₂ : ℕ} {tree₁ : bt A} {tree₂ : bt A} {st : List (bt A)} {v1 : A} → (Pre : findPR key (node key₂ v1 tree₁ tree₂) st (findPC value) ) → key > key₂ → findPC value key tree₂ (tree₂ ∷ st) - findext02 Pre c with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre) | inspect findPC.tree1 (findPR.ci Pre) - ... | r-leaf | leaf | record { eq = refl } = ⊥-elim ( nat-≤> c ≤-refl) - ... | r-node | node key value t1 t3 | record { eq = refl } = ⊥-elim ( nat-≤> c ≤-refl ) - ... | r-left x t | t1 | t2 = ⊥-elim (nat-<> x c) - ... | r-right x ri | node key value t1 t3 | record { eq = refl } = record { tree1 = t3 ; ci = ri } + findext02 Pre c with findPC.ci (findPR.ci Pre) | findPC.tree1 (findPR.ci Pre) in eqp + ... | r-leaf | leaf = ⊥-elim ( nat-≤> c ≤-refl) + ... | r-node | node key value t1 t3 = ⊥-elim ( nat-≤> c ≤-refl ) + ... | r-left x t | t1 = ⊥-elim (nat-<> x c) + ... | r-right {key₂} {v1} {_} {tree₂} x ri | node key value t1 t3 = record { tree1 = t3 ; ci = subst (λ k → replacedTree _ _ k _) (lemma01 eqp) ri } where + lemma01 : {t2 : bt A} → node key₂ v1 tree₂ t2 ≡ node key value t1 t3 → t2 ≡ t3 + lemma01 refl = refl findext : findExt key (findPC value ) findext = record { c1 = findext01 ; c2 = findext02 } diff -r 0cf53f1e0055 -r f2a3f5707075 hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Tue Jun 11 22:37:13 2024 +0900 +++ b/hoareBinaryTree1.agda Wed Jun 12 22:46:57 2024 +0900 @@ -1290,15 +1290,17 @@ rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-left ? lt2 trb) RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ leaf (node key₂ ⟪ Red , v2 ⟫ t t₁)) (node _ ⟪ Red , _ ⟫ .(to-black leaf) (node _ ⟪ Black , v2 ⟫ t t₂)) key value (t-right _ _ x₁ x₂ x₃ ti) (rbr-flip-rr x () lt trb) -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ t₂ leaf)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ t₂ t₄)) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) = t-node _ _ _ ? ? ? ? ? ? (replaceTree1 _ _ _ ti) (replaceTree1 _ _ _ ?) -RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ t₂ (node key₄ value₁ t₃ t₅))) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ t₂ t₄)) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) = t-node _ _ _ ? ? ? ? ? ? (replaceTree1 _ _ _ ti) (replaceTree1 _ _ _ ?) where - -- treeInvariant (node key₁ ⟪ Red , v1 ⟫ (node key₂ ⟪ Black , v2 ⟫ t t₁) (node key₃ ⟪ Black , c3 ⟫ t₂ t₄)) - rr00 : tr> key₁ t₄ - rr00 = RB-repl→ti> _ _ _ _ _ trb (<-trans x₂ lt) x₆ - rr02 : treeInvariant (node key₃ ⟪ Red , c3 ⟫ t₂ t₄) - rr02 = RB-repl→ti _ _ _ _ ti₁ (rbr-right ? lt trb) - rr03 : treeInvariant t₄ - rr03 = RB-repl→ti _ _ _ _ (treeRightDown _ _ ti₁) trb +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ leaf t₃)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .leaf t₄)) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-rr x y lt trb) = ? +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ (node key₄ value₁ t₂ t₅) .leaf)) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .(node key₄ value₁ t₂ t₅) (node key₅ value₂ t₄ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-left .key₄ .key₃ x₇ x₈ x₉ ti₁)) (rbr-flip-rr x y lt trb) = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ x₇ (proj1 rr00) x₈ x₉ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti₁ (RB-repl→ti _ _ _ _ t-leaf trb)) where + rr00 : (key₃ < key₅) ∧ tr> key₃ t₄ ∧ tr> key₃ t₆ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt tt + rr02 : (key₁ < key₅) ∧ tr> key₁ t₄ ∧ tr> key₁ t₆ + rr02 = ⟪ <-trans x₂ (proj1 rr00) , ⟪ <-tr> (proj1 (proj2 rr00)) x₂ , <-tr> (proj2 (proj2 rr00)) x₂ ⟫ ⟫ +RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ c2 , v2 ⟫ t t₁) (node key₃ ⟪ Red , c3 ⟫ (node key₄ value₁ t₂ t₅) .(node key₆ _ _ _))) (node _ ⟪ Red , _ ⟫ .(to-black (node key₂ ⟪ c2 , v2 ⟫ t t₁)) (node _ ⟪ Black , c3 ⟫ .(node key₄ value₁ t₂ t₅) (node key₅ value₂ t₄ t₆))) key value (t-node key₂ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti (t-node .key₄ .key₃ key₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ ti₁ ti₂)) (rbr-flip-rr x y lt trb) = t-node _ _ _ x₁ x₂ x₃ x₄ x₅ rr02 (replaceTree1 _ _ _ ti) (t-node _ _ _ x₇ (proj1 rr00) x₉ x₁₀ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti₁ (RB-repl→ti _ _ _ _ ti₂ trb)) where + rr00 : (key₃ < key₅) ∧ tr> key₃ t₄ ∧ tr> key₃ t₆ + rr00 = RB-repl→ti> _ _ _ _ _ trb lt ⟪ x₈ , ⟪ x₁₁ , x₁₂ ⟫ ⟫ + rr02 : (key₁ < key₅) ∧ tr> key₁ t₄ ∧ tr> key₁ t₆ + rr02 = ⟪ <-trans x₂ (proj1 rr00) , ⟪ <-tr> (proj1 (proj2 rr00)) x₂ , <-tr> (proj2 (proj2 rr00)) x₂ ⟫ ⟫ RB-repl→ti {_} {A} (node k1 ⟪ Black , c1 ⟫ (node k2 ⟪ Red , c2 ⟫ .leaf .leaf) leaf) (node _ ⟪ Black , _ ⟫ (node key₁ value₁ t₂ t₃) (node _ ⟪ Red , _ ⟫ .leaf leaf)) key value (t-left _ _ x₁ x₂ x₃ (t-single .k2 .(⟪ Red , c2 ⟫))) (rbr-rotate-ll x lt trb) = t-node _ _ _ (proj1 rr10) x₁ (proj1 (proj2 rr10)) (proj2 (proj2 rr10)) tt tt (RB-repl→ti _ _ _ _ t-leaf trb) (t-single _ _ ) where rr10 : (key₁ < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃