Mercurial > hg > Gears > GearsAgda

changeset 933:f2a3f5707075

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 Wed, 12 Jun 2024 22:46:57 +0900
parents 0cf53f1e0055
children d413fa12685f
files ModelChecking.agda hoareBinaryTree.agda hoareBinaryTree1.agda
diffstat 3 files changed, 30 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- 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
--- 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 }
 
--- 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₃