Mercurial > hg > Members > kono > Proof > automaton

comparison a02/agda/practice-nat.agda @ 406:a60132983557

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 Wed, 08 Nov 2023 21:35:54 +0900
parents b3f05cd08d24
children
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
1 {-# OPTIONS --cubical-compatible --safe #-}
1 module practice-nat where 2 module practice-nat where
2 3
3 open import Data.Nat 4 open import Data.Nat
4 open import Data.Empty 5 open import Data.Empty
5 open import Relation.Nullary 6 open import Relation.Nullary
6 open import Relation.Binary.PropositionalEquality hiding (_⇔_) 7 open import Relation.Binary.PropositionalEquality hiding (_⇔_)
7 open import logic 8 open import logic
8 9
10 -- data _<=_ : ℕ → ℕ → Set where
11 -- z<=n : {x : ℕ} → zero <= x
12 -- s<=s : {x y : ℕ} → x <= y → suc x <= suc y
13
9 -- hint : it has two inputs, use recursion 14 -- hint : it has two inputs, use recursion
10 nat-<> : { x y : ℕ } → x < y → y < x → ⊥ 15 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
11 nat-<> = {!!} 16 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
12 17
13 -- hint : use recursion 18 -- hint : use recursion
14 nat-<≡ : { x : ℕ } → x < x → ⊥ 19 nat-<≡ : { x : ℕ } → x < x → ⊥
15 nat-<≡ = {!!} 20 nat-<≡ (s≤s x<x) = nat-<≡ x<x
16 21
17 -- hint : use refl and recursion 22 -- hint : use refl and recursion
18 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ 23 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
19 nat-≡< = {!!} 24 nat-≡< refl (s≤s x<y) = nat-≡< refl x<y
20 25
21 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ 26 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
22 ¬a≤a = {!!} 27 ¬a≤a (s≤s lt) = ¬a≤a lt
23 28
24 -- hint : make case with la first 29 -- hint : make case with la first
25 a<sa : {la : ℕ} → la < suc la 30 a<sa : {i : ℕ} → i < suc i
26 a<sa = {!!} 31 a<sa {zero} = s≤s z≤n
32 a<sa {suc i} = s≤s a<sa
27 33
28 -- hint : ¬ has an input, use recursion 34 -- hint : ¬ has an input, use recursion
29 =→¬< : {x : ℕ } → ¬ ( x < x ) 35 =→¬< : {x : ℕ } → ¬ ( x < x )
30 =→¬< = {!!} 36 =→¬< = {!!}
31 37