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

annotate nat.agda @ 324:fbabb20f222e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 18:18:17 +0900
parents 95a26d1698f4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module nat where
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Empty
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Relation.Nullary
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Relation.Binary.PropositionalEquality
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import logic
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 nat-<> : { x y : Nat } → x < y → y < x → ⊥
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 nat-<≡ : { x : Nat } → x < x → ⊥
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 nat-<≡ (s≤s lt) = nat-<≡ lt
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 nat-≡< refl lt = nat-<≡ lt
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 ¬a≤a (s≤s lt) = ¬a≤a lt
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 a<sa : {la : Nat} → la < Suc la
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 a<sa {Zero} = s≤s z≤n
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 a<sa {Suc la} = s≤s a<sa
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 =→¬< : {x : Nat } → ¬ ( x < x )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 =→¬< {Zero} ()
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 =→¬< {Suc x} (s≤s lt) = =→¬< lt
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 <-∨ {Suc x} {Zero} (s≤s ())
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
41 max : (x y : Nat) → Nat
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
42 max Zero Zero = Zero
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
43 max Zero (Suc x) = (Suc x)
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
44 max (Suc x) Zero = (Suc x)
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
45 max (Suc x) (Suc y) = Suc ( max x y )
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
46