Mercurial > hg > Gears > GearsAgda

changeset 562:9df8103bc493

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dec ≤′ done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Mar 2018 10:52:51 +0900
parents 1bbbd787472e
children 8634f448e699
files redBlackTreeTest.agda
diffstat 1 files changed, 77 insertions(+), 68 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Fri Mar 30 10:17:07 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Mar 30 10:52:51 2018 +0900
@@ -16,44 +16,44 @@
 
 -- tests
 
-putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t
 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
 ...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (λ  s → findNode tree s (leafNode k1 value) n2 (λ  tree1 s n1 → replaceNode tree1 s n1 next))
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
 open import Function
 
 
-check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
 check1 Nothing _ = False
 check1 (Just n)  x with Data.Nat.compare (value n)  x
 ...  | equal _ = True
 ...  | _ = False
 
-check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
 check2 Nothing _ = False
 check2 (Just n)  x with compare2 (value n)  x
 ...  | EQ = True
 ...  | _ = False
 
-test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
+test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True   ))
 test1 = refl
 
 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
-    \t -> putTree1 t 2 2 (
-    \t -> getRedBlackTree t 1 (
-    \t x -> check2 x 1 ≡ True   )))
+    λ t → putTree1 t 2 2 (
+    λ t → getRedBlackTree t 1 (
+    λ t x → check2 x 1 ≡ True   )))
 test2 = refl
 
 open ≡-Reasoning
 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
-    $ \t -> putTree1 t 2 2
-    $ \t -> putTree1 t 3 3
-    $ \t -> putTree1 t 4 4    
-    $ \t -> getRedBlackTree t 1
-    $ \t x -> check2 x 1 ≡ True  
+    $ λ t → putTree1 t 2 2
+    $ λ t → putTree1 t 3 3
+    $ λ t → putTree1 t 4 4    
+    $ λ t → getRedBlackTree t 1
+    $ λ t x → check2 x 1 ≡ True  
 test3 = begin
     check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
   ≡⟨ refl ⟩
@@ -61,29 +61,29 @@
   ∎
 
 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
-    $ \t -> putTree1 t 2 2
-    $ \t -> putTree1 t 3 3
-    $ \t -> putTree1 t 4 4
-    $ \t -> getRedBlackTree t 4
-    $ \t x -> x
+    $ λ t → putTree1 t 2 2
+    $ λ t → putTree1 t 3 3
+    $ λ t → putTree1 t 4 4
+    $ λ t → getRedBlackTree t 4
+    $ λ t x → x
 
 -- test5 : Maybe (Node ℕ ℕ)
 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 
-    $ \t -> putTree1 t 6 6
-    $ \t0 ->  clearSingleLinkedStack (nodeStack t0)
-    $ \s -> findNode1 t0 s (leafNode 3 3) ( root t0 )
-    $ \t1 s n1 -> replaceNode t1 s n1 
-    $ \t -> getRedBlackTree t 3
-    -- $ \t x -> SingleLinkedStack.top (stack s)
-    -- $ \t x -> n1
-    $ \t x -> root t
+    $ λ t → putTree1 t 6 6
+    $ λ t0 →  clearSingleLinkedStack (nodeStack t0)
+    $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
+    $ λ t1 s n1 → replaceNode t1 s n1 
+    $ λ t → getRedBlackTree t 3
+    -- $ λ t x → SingleLinkedStack.top (stack s)
+    -- $ λ t x → n1
+    $ λ t x → root t
   where
-     findNode1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
+     findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
      findNode1 t s n1 Nothing next = next t s n1
      findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
 
--- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t ->
---   putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
+-- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t →
+--   putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
 -- test51 = refl
 
 test6 : Maybe (Node ℕ ℕ)
@@ -91,7 +91,7 @@
 
 
 test7 : Maybe (Node ℕ ℕ)
-test7 = clearSingleLinkedStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t))
+test7 = clearSingleLinkedStack (nodeStack tree2) (λ  s → replaceNode tree2 s n2 (λ  t → root t))
   where
     tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
     k1 = 1
@@ -100,62 +100,71 @@
 
 test8 : Maybe (Node ℕ ℕ)
 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
-    $ \t -> putTree1 t 2 2 (\ t -> root t)
+    $ λ t → putTree1 t 2 2 (λ  t → root t)
 
 
-test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True   ))
+test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True   ))
 test9 = refl
 
 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
-    \t -> putRedBlackTree t 2 2 (
-    \t -> getRedBlackTree t 1 (
-    \t x -> check2 x 1 ≡ True   )))
+    λ t → putRedBlackTree t 2 2 (
+    λ t → getRedBlackTree t 1 (
+    λ t x → check2 x 1 ≡ True   )))
 test10 = refl
 
 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
-    $ \t -> putRedBlackTree t 2 2
-    $ \t -> putRedBlackTree t 3 3
-    $ \t -> getRedBlackTree t 2
-    $ \t x -> root t
+    $ λ t → putRedBlackTree t 2 2
+    $ λ t → putRedBlackTree t 3 3
+    $ λ t → getRedBlackTree t 2
+    $ λ t x → root t
 
 
-redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
+redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ 
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
 
--- compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
+-- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
 -- compare2 zero zero = EQ
 -- compare2 (suc _) zero = GT
 -- compare2  zero (suc _) = LT
 -- compare2  (suc x) (suc y) = compare2 x y
 
-compareTri1 : (n : ℕ) -> zero <′ suc n 
+contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
+contraposition f = λ x y → x (f y)
+ 
+compareTri1 : (n : ℕ) → zero <′ suc n 
 compareTri1 zero =   ≤′-refl 
 compareTri1 (suc n) =  ≤′-step ( compareTri1 n )
 
-compareTri2 : (n m : ℕ) -> n ≤′ m -> suc n ≤′ suc m
+compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
 compareTri2 _ _  ≤′-refl = ≤′-refl 
 compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc n }  ( compareTri2 n m p )
 
 <′dec : Set
 <′dec = ∀ m n → Dec ( m ≤′ n )
- 
+
+compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+
 is≤′ :  <′dec
 is≤′  zero zero = yes ≤′-refl
-is≤′  zero (suc n) = yes {!!}
-is≤′  (suc m) (zero) = no ( \ () )
+is≤′  zero (suc n) = yes (lemma n)
+  where
+     lemma :  (n : ℕ) → zero ≤′ suc n
+     lemma zero =   ≤′-step  ≤′-refl
+     lemma (suc n) =  ≤′-step (lemma n)
+is≤′  (suc m) (zero) = no ( λ () )
 is≤′  (suc m) (suc n) with is≤′ m n
-... | yes p = yes {!!}
-... | no p = no {!!}
+... | yes p = yes ( compareTri2 _ _ p )
+... | no p = no ( compareTri6 _ p )
 
-compareTri20 : {n : ℕ} -> ¬ suc n ≤′ zero
+compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
 compareTri20 () 
 
 
-compareTri21 : (n m : ℕ) -> suc n ≤′ suc m ->  n ≤′ m
+compareTri21 : (n m : ℕ) → suc n ≤′ suc m →  n ≤′ m
 compareTri21 _ _  ≤′-refl = ≤′-refl
 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
   where
-        compareTri23 : (n : ℕ) -> suc n ≤′ suc zero -> suc n ≤′ zero ->  n ≤′ zero
+        compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero →  n ≤′ zero
         compareTri23 zero ( ≤′-step p ) _ =   ≤′-refl
         compareTri23 zero ≤′-refl _ =   ≤′-refl
         compareTri23 (suc n1) ( ≤′-step p ) ()
@@ -172,7 +181,7 @@
 ... | yes refl  = λ x y → x refl
 ... | no  p  = λ x y → p ( cong pred y )
 
-compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+-- compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
 compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)
 
 compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
@@ -187,65 +196,65 @@
 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
 
-compareDecTest : (n n1 : Node ℕ ℕ) -> ( key n ≡ key n1 ) ∨ ( ¬  key n ≡ key n1 )
+compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬  key n ≡ key n1 )
 compareDecTest n n1 with (key n) ≟ (key n1)
 ...  | yes p  = pi1  p
 ...  | no ¬p  = pi2 ¬p
 
 
-putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
+putTest1Lemma2 : (k : ℕ)  → compare2 k k ≡ EQ
 putTest1Lemma2 zero = refl
 putTest1Lemma2 (suc k) = putTest1Lemma2 k
 
-putTest1Lemma1 : (x y : ℕ)  -> compareℕ x y ≡ compare2 x y
+putTest1Lemma1 : (x y : ℕ)  → compareℕ x y ≡ compare2 x y
 putTest1Lemma1 zero    zero    = refl
 putTest1Lemma1 (suc m) zero    = refl
 putTest1Lemma1 zero    (suc n) = refl
 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
 putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
  where
-    lemma1 : (m :  ℕ) -> LT  ≡ compare2 m (ℕ.suc (m + k)) 
+    lemma1 : (m :  ℕ) → LT  ≡ compare2 m (ℕ.suc (m + k)) 
     lemma1  zero = refl
     lemma1  (suc y) = lemma1 y
 putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
  where
-    lemma1 : (m :  ℕ) -> EQ  ≡ compare2 m m
+    lemma1 : (m :  ℕ) → EQ  ≡ compare2 m m
     lemma1  zero = refl
     lemma1  (suc y) = lemma1 y
 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
  where
-    lemma1 : (m :  ℕ) -> GT  ≡ compare2  (ℕ.suc (m + k))  m
+    lemma1 : (m :  ℕ) → GT  ≡ compare2  (ℕ.suc (m + k))  m
     lemma1  zero = refl
     lemma1  (suc y) = lemma1 y
 
-putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
+putTest1Lemma3 : (k : ℕ)  → compareℕ k k ≡ EQ
 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 
 
-compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
+compareLemma1 : {x  y : ℕ}  → compare2 x y ≡ EQ → x  ≡ y
 compareLemma1 {zero} {zero} refl = refl
 compareLemma1 {zero} {suc _} () 
 compareLemma1 {suc _} {zero} () 
-compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
+compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
    where
       lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
 
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
-         -> (k : ℕ) (x : ℕ) 
-         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True)) 
+         → (k : ℕ) (x : ℕ) 
+         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
+         (λ  t → getRedBlackTree t k (λ  t x1 → check2 x1 x  ≡ True)) 
 putTest1 n k x with n
 ...  | Just n1 = lemma2 ( record { top = Nothing } )
    where
-     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
          GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
      lemma2 s with compare2 k (key n1)
      ... |  EQ = lemma3 {!!}
         where 
-           lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+           lemma3 : compare2 k (key n1) ≡  EQ → getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
-               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
+               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( λ  t x1 → check2 x1 x  ≡ True)
            lemma3 eq with compare2 x x | putTest1Lemma2 x 
            ... | EQ | refl with compare2 k (key n1)  | eq
            ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
@@ -257,7 +266,7 @@
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red 
         } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
-        ( \ t x1 -> check2 x1 x  ≡ True) 
+        ( λ  t x1 → check2 x1 x  ≡ True) 
      lemma1 with compare2 k k | putTest1Lemma2 k
      ... | EQ | refl with compare2 x x | putTest1Lemma2 x
      ...              | EQ | refl = refl