Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison nat.agda @ 213:22d435172d1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate logic and nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2019 12:17:10 +0900
parents
children 95a26d1698f4
comparison
equal deleted inserted replaced
212:0a1804cc9d0a 213:22d435172d1a
1 module nat where
2
3 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
4 open import Data.Empty
5 open import Relation.Nullary
6 open import Relation.Binary.PropositionalEquality
7 open import logic
8
9
10 nat-<> : { x y : Nat } → x < y → y < x → ⊥
11 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
12
13 nat-<≡ : { x : Nat } → x < x → ⊥
14 nat-<≡ (s≤s lt) = nat-<≡ lt
15
16 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
17 nat-≡< refl lt = nat-<≡ lt
18
19 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
20 ¬a≤a (s≤s lt) = ¬a≤a lt
21
22 a<sa : {la : Nat} → la < Suc la
23 a<sa {Zero} = s≤s z≤n
24 a<sa {Suc la} = s≤s a<sa
25
26 =→¬< : {x : Nat } → ¬ ( x < x )
27 =→¬< {Zero} ()
28 =→¬< {Suc x} (s≤s lt) = =→¬< lt
29
30 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
31 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
32
33 <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
34 <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
35 <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
36 <-∨ {Suc x} {Zero} (s≤s ())
37 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
38 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
39 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
40