--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/etc/trichotomos-ex.agda	Tue Apr 17 10:14:16 2018 +0900
@@ -0,0 +1,205 @@
+module trichotomos-ex where
+
+open import Level hiding (zero) renaming ( suc to succ )
+open import Data.Empty
+open import Data.Nat
+open import Relation.Nullary
+open import Algebra
+open import Data.Nat.Properties   as NatProp
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Function
+
+data Bool {n : Level } : Set n where
+  True  : Bool
+  False : Bool
+
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    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
+
+data Color {n : Level } : Set n where
+  Red   : Color
+  Black : Color
+
+data CompareResult {n : Level } : Set n where
+  LT : CompareResult
+  GT : CompareResult
+  EQ : CompareResult
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+compareℕ :  ℕ → ℕ → CompareResult {Level.zero}
+compareℕ x y with Data.Nat.compare x y
+... | less _ _ = LT
+... | equal _ = EQ
+... | greater _ _ = GT
+
+compareT :  ℕ → ℕ → CompareResult {Level.zero}
+compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y
+... | tri≈ _ _ _ = EQ
+... | tri< _ _ _ = LT
+... | tri> _ _ _ = GT
+
+
+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
+
+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 _ _  ≤′-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 (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 ( compareTri2 _ _ p )
+... | no p = no ( compareTri6 _ p )
+
+compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
+compareTri20 () 
+
+
+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 zero ( ≤′-step p ) _ =   ≤′-refl
+        compareTri23 zero ≤′-refl _ =   ≤′-refl
+        compareTri23 (suc n1) ( ≤′-step p ) ()
+compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
+compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
+   
+
+compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
+compareTri3 zero    ()
+compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
+
+compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4' m {n} with n ≟ m
+... | yes refl  = λ x y → x refl
+... | no  p  = λ x y → p ( cong pred y )
+
+compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4 m = contraposition ( λ x → cong pred x )
+
+-- 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
+compareTri5  m {n}  = compareTri6 (suc m)
+
+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<  (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
+... | 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 with (key n) ≟ (key n1)
+...  | yes p  = pi1  p
+...  | no ¬p  = pi2 ¬p
+
+
+putTest1Lemma2 : (k : ℕ)  → compare2 k k ≡ EQ
+putTest1Lemma2 zero = refl
+putTest1Lemma2 (suc k) = putTest1Lemma2 k
+
+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  zero = refl
+    lemma1  (suc y) = lemma1 y
+putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
+ where
+    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  zero = refl
+    lemma1  (suc y) = lemma1 y
+
+putTest1Lemma3 : (k : ℕ)  → compareℕ k k ≡ EQ
+putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 
+
+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 ) )
+   where
+      lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
+      lemma2 = refl
+
+
+compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
+compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 
+   where open import  Relation.Binary
+
+checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
+checkT Nothing _ = False
+checkT (Just n) x with compTri (value n)  x
+...  | tri≈ _ _ _ = True
+...  | _ = False
+
+checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (Just n) x ≡ True
+checkEQ x n refl with compTri (value n)  x
+... |  tri≈ _ refl _ = refl
+... |  tri> _ neq gt =  ⊥-elim (neq refl)
+... |  tri< lt neq _ =  ⊥-elim (neq refl)
+
+checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x  ≡ y  ) -> ( x  ≟ y ) ≡ yes eq
+checkEQ' x y refl with  x  ≟ y
+... | yes refl = refl
+... | no neq = ⊥-elim ( neq refl )
+