Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/nat.agda @ 431:a5f8084b8368
reorganiztion for apkg
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 21 Dec 2020 10:23:37 +0900 |
parents | |
children | eb4049abad70 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/nat.agda Mon Dec 21 10:23:37 2020 +0900 @@ -0,0 +1,46 @@ +module nat where + +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +open import logic + + +nat-<> : { x y : Nat } → x < y → y < x → ⊥ +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x + +nat-<≡ : { x : Nat } → x < x → ⊥ +nat-<≡ (s≤s lt) = nat-<≡ lt + +nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + +¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ +¬a≤a (s≤s lt) = ¬a≤a lt + +a<sa : {la : Nat} → la < Suc la +a<sa {Zero} = s≤s z≤n +a<sa {Suc la} = s≤s a<sa + +=→¬< : {x : Nat } → ¬ ( x < x ) +=→¬< {Zero} () +=→¬< {Suc x} (s≤s lt) = =→¬< lt + +>→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) +>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x + +<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl +<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) +<-∨ {Suc x} {Zero} (s≤s ()) +<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt +<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) +<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) + +max : (x y : Nat) → Nat +max Zero Zero = Zero +max Zero (Suc x) = (Suc x) +max (Suc x) Zero = (Suc x) +max (Suc x) (Suc y) = Suc ( max x y ) +