Mercurial > hg > Gears > GearsAgda
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 )