view etc/trichotomos-ex.agda @ 956:bfc7007177d0 default tip

safe and cubical compatible with no warning done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 19 Oct 2024 09:48:48 +0900
parents 0b791ae19543
children
line wrap: on
line source

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 )