Mercurial > hg > Gears > GearsAgda

changeset 554:988c12d7f887

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use another nat comparator
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Mar 2018 23:22:07 +0900
parents 7d9af1d4b5af
children e8c9a492b578
files redBlackTreeTest.agda stack.agda
diffstat 2 files changed, 22 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Mon Mar 26 17:50:04 2018 +0900
+++ b/redBlackTreeTest.agda	Mon Mar 26 23:22:07 2018 +0900
@@ -2,7 +2,7 @@
 
 open import RedBlackTree
 open import stack
-open import Level hiding (zero)
+open import Level hiding (zero) renaming ( suc to succ )
 
 open import Data.Empty
 
@@ -128,24 +128,27 @@
 -- compare2  zero (suc _) = LT
 -- compare2  (suc x) (suc y) = compare2 x y
 
-compareTri1 : (n : ℕ) -> zero < ℕ.suc n 
-compareTri1 zero = {!!}
-compareTri1 (suc n) = {!!}
+compareTri1 : (n : ℕ) -> zero <′ suc n 
+compareTri1 zero =   ≤′-refl 
+compareTri1 (suc n) =  ≤′-step ( compareTri1 n )
 
-compareTri :  Trichotomous  _≡_ _<_
-compareTri zero zero = tri≈ (\()) refl (\())
-compareTri zero (suc n) = tri< {!!} (\()) (\())
-compareTri (suc n) zero = tri> (\()) (\()) {!!}
+compareTri2 : (n m : ℕ) -> (suc n) ≤′ m -> suc (suc n) ≤′ suc m
+compareTri2 _ _  ≤′-refl = ≤′-refl 
+compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc (suc n) }  ( compareTri2 n m p )
+
+compareTri :  Trichotomous  _≡_ _<′_
+compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
+compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())
+compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
 compareTri (suc n) (suc m) with compareTri n m
-... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!}
-... | tri< p q r = tri<  {!!} {!!} {!!}
-... | tri> p q r = tri> {!!} {!!} {!!}
+... | tri≈ p q r = tri≈ {!!} (cong ( λ x -> suc x) q) {!!}
+... | tri< p q r = tri<  (compareTri2 n m p ) {!!} {!!}
+... | tri> p q r = tri> {!!} {!!}  (compareTri2 m n r )
 
-compareDecTest : (n n1 : Node ℕ ℕ) -> 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 = p
-...  | no ¬p  = {!!}
-
+...  | yes p = pi1 p
+...  | no ¬p  = pi2 ¬p
 
 
 putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
--- a/stack.agda	Mon Mar 26 17:50:04 2018 +0900
+++ b/stack.agda	Mon Mar 26 23:22:07 2018 +0900
@@ -17,6 +17,10 @@
     pi1 : a
     pi2 : b
 
+data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where
+   pi1  : a -> a ∨ b
+   pi2  : b -> a ∨ b
+
 data Maybe {n : Level } (a : Set n) : Set n where
   Nothing : Maybe a
   Just    : a -> Maybe a